Module

ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.lean

Nyll.AlgebraicCurves.Valuations.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal

10 declarations indexed from sourceView source ↗

Module documentation

Valuation Subring exists dvd pow of mem maximal Ideal

Imports12

Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Order.GroupWithZero.Basic
Mathlib.Data.Finset.Max
Mathlib.Data.Nat.Factorization.Basic
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
Mathlib.RingTheory.Algebraic.Basic
Mathlib.RingTheory.Coprime.Lemmas
Mathlib.RingTheory.Valuation.Basic
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Tactic.ByContra
Mathlib.Tactic.Push
Mathlib.Tactic.WLOG

Imported by1

Nyll.AlgebraicCurves.Valuations.All

theorem

exists_ne_val_eq_of_sum_eq_zero

L43 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.exists_ne_val_eq_of_sum_eq_zero

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)

Lean source · statement

theorem exists_ne_val_eq_of_sum_eq_zero {ι : Type*} (s : Finset ι) (t : ι → K)
    (hsum : ∑ i ∈ s, t i = 0) {i₁ : ι} (hi₁ : i₁ ∈ s) (ht₁ : t i₁ ≠ 0) :
    ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ t i ≠ 0 ∧ t j ≠ 0 ∧ v (t i) = v (t j)

theorem

valuation_natCast_eq_one_of_not_dvd

L68 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.valuation_natCast_eq_one_of_not_dvd

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem valuation_natCast_eq_one_of_not_dvd (hqA : (q : K) ∈ A.nonunits) {n : ℕ} (hn : ¬ q ∣ n) :
    w (n : K) = 1

theorem

exists_valuation_natCast_eq

L92 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.exists_valuation_natCast_eq

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem exists_valuation_natCast_eq (hqA : (q : K) ∈ A.nonunits) {n : ℕ} (hn : n ≠ 0) :
    ∃ e : ℕ, w (n : K) = w (q : K) ^ e

theorem

exists_valuation_ratCast_eq

L99 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.exists_valuation_ratCast_eq

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem exists_valuation_ratCast_eq (hqA : (q : K) ∈ A.nonunits) [CharZero K] {r : ℚ} (hr : r ≠ 0) :
    ∃ a b : ℕ, w (r : K) * w (q : K) ^ a = w (q : K) ^ b

theorem

exists_pow_valuation_eq

L116 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.exists_pow_valuation_eq

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem exists_pow_valuation_eq [CharZero K] [Algebra ℚ K] (hqA : (q : K) ∈ A.nonunits) {x : K}
    (hx : IsAlgebraic ℚ x) (hx0 : x ≠ 0) :
    ∃ k : ℕ, 0 < k ∧ ∃ a b : ℕ, w x ^ k * w (q : K) ^ a = w (q : K) ^ b

theorem

exists_pow_eq_mul_of_mem_maximalIdeal

L151 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.exists_pow_eq_mul_of_mem_maximalIdeal

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem exists_pow_eq_mul_of_mem_maximalIdeal [CharZero K] [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (hqA : (q : K) ∈ A.nonunits) (c : A) (hc0 : c ≠ 0) (c' : A)
    (hc' : c' ∈ IsLocalRing.maximalIdeal A) (hc'0 : c' ≠ 0) :
    ∃ M : ℕ, ∃ a : A, (c' : K) ^ M = c * a

theorem

map_eq_zero_of_mem_maximalIdeal

L197 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.map_eq_zero_of_mem_maximalIdeal

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem map_eq_zero_of_mem_maximalIdeal [CharZero K] [Algebra ℚ K] [Algebra.IsAlgebraic ℚ K]
    (hqA : (q : K) ∈ A.nonunits) {k : Type*} [Field k] [CharP k q] (red : A →+* k)
    (a : A) (ha : a ∈ IsLocalRing.maximalIdeal A) : red a = 0

theorem

exists_pow_eq_mul_of_mem_maximalIdeal_algebraicClosure

L219 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.exists_pow_eq_mul_of_mem_maximalIdeal_algebraicClosure

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem exists_pow_eq_mul_of_mem_maximalIdeal_algebraicClosure
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hqA : (q : AlgebraicClosure ℚ) ∈ A.nonunits)
    (c : A) (hc0 : c ≠ 0) (c' : A) (hc' : c' ∈ IsLocalRing.maximalIdeal A) (hc'0 : c' ≠ 0) :
    ∃ M : ℕ, ∃ a : A, (c' : AlgebraicClosure ℚ) ^ M = c * a

theorem

map_eq_zero_of_mem_maximalIdeal_algebraicClosure

L226 ↗

AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal.Ws25.Archimedean.map_eq_zero_of_mem_maximalIdeal_algebraicClosure

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal
namespace Ws25
namespace Archimedean
section Archimedean
open Polynomial
variable {K : Type*} [Field K] {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ)
variable (A : ValuationSubring K) {q : ℕ} [hq : Fact q.Prime]
local notation "w" => ValuationSubring.valuation A

Lean source · statement

theorem map_eq_zero_of_mem_maximalIdeal_algebraicClosure
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hqA : (q : AlgebraicClosure ℚ) ∈ A.nonunits)
    {k : Type*} [Field k] [CharP k q] (red : A →+* k)
    (a : A) (ha : a ∈ IsLocalRing.maximalIdeal A) : red a = 0

theorem

exists_dvd_pow_of_mem_maximalIdeal

L237 ↗

ValuationSubring.exists_dvd_pow_of_mem_maximalIdeal

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Valuations.Proofs.ValuationSubring_exists_dvd_pow_of_mem_maximalIdeal

Lean source · statement

theorem _root_.ValuationSubring.exists_dvd_pow_of_mem_maximalIdeal
    (A : ValuationSubring (AlgebraicClosure ℚ)) {q : ℕ} [Fact q.Prime]
    (hq : ((q : ℕ) : AlgebraicClosure ℚ) ∈ A.nonunits)
    (c : A) (hc : c ≠ 0) (c' : A) (hc' : c' ∈ IsLocalRing.maximalIdeal A) (hc'0 : c' ≠ 0) :
    ∃ M : ℕ, c ∣ c' ^ M

Module documentation

Valuation Subring exists dvd pow of mem maximal Ideal

Declarations