Documentation

Mathlib.RingTheory.Valuation.Discrete.Basic

Discrete Valuations #

Given a linearly ordered commutative group with zero Γ, a valuation v : A → Γ on a ring A is discrete, if there is an element γ : Γˣ that is < 1 and generated the range of v, implemented as MonoidWithZeroHom.valueGroup v. When Γ := ℤₘ₀ (defined in Multiplicative.termℤₘ₀), γ = ofAdd (-1)and the condition of being discrete is equivalent to asking thatofAdd (-1 : ℤ)belongs to the image, in turn equivalent to asking that `1 : ℤ` belongs to the image of the corresponding additive valuation.

Note that this definition of discrete implies that the valuation is nontrivial and of rank one, as is commonly assumed in number theory. To avoid potential confusion with other definitions of discrete, we use the name IsRankOneDiscrete to refer to discrete valuations in this setting.

Main Definitions #

Valuation.IsRankOneDiscrete: We define a Γ-valued valuation v to be discrete if if there is an element γ : Γˣ that is < 1 and generates the range of v.
Valuation.IsUniformizer: Given a Γ-valued valuation v on a ring R, an element π : R is a uniformizer if v π is a generator of the value group that is <1.
Valuation.Uniformizer: A structure bundling an element of a ring and a proof that it is a uniformizer.

Main Results #

Valuation.IsUniformizer.of_associated: An element associated to a uniformizer is itself a uniformizer.
Valuation.associated_of_isUniformizer: If two elements are uniformizers, they are associated.
Valuation.IsUniformizer.is_generator A generator of the maximal ideal is a uniformizer when the valuation is discrete.
Valuation.IsRankOneDiscrete.mk': if the valueGroup of the valuation v is cyclic and nontrivial, then v is discrete.
Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial: If v is a valuation on a field K whose value group is cyclic and nontrivial, then there exists a uniformizer for v.
Valuation.isUniformizer_of_maximalIdeal_eq_span: Given a discrete valuation v on a field K, a generator of the maximal ideal of v.valuationSubring is a uniformizer for v.
Valuation.valuationSubring_isDiscreteValuationRing : If v is a valuation on a field K whose value group is cyclic and nontrivial, then v.valuationSubring is a discrete valuation ring. This instance is the formalization of Chapter I, Section 1, Proposition 1 in [Ser68].
IsDiscreteValuationRing.isRankOneDiscrete: Given a DVR A and a field K satisfying IsFractionRing A K, the valuation induced on K is discrete.
IsDiscreteValuationRing.equivValuationSubring The ring isomorphism between a DVR and the unit ball in its field of fractions endowed with the adic valuation of the maximal ideal.

TODO #

Relate discrete valuations and discrete valuation rings (contained in the project https://github.com/mariainesdff/LocalClassFieldTheory)

class Valuation.IsRankOneDiscrete {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) :

Given a linearly ordered commutative group with zero Γ such that Γˣ is nontrivial cyclic, a valuation v : A → Γ on a ring A is discrete, if genLTOne Γˣ belongs to the image. Note that the latter is equivalent to asking that 1 : ℤ belongs to the image of the corresponding additive valuation.

exists_generator_lt_one' : ∃ (γ : Γˣ), Subgroup.zpowers γ = MonoidWithZeroHom.valueGroup v ∧ γ < 1

Instances

theorem Valuation.IsRankOneDiscrete.exists_generator_lt_one {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

∃ (γ : Γˣ), Subgroup.zpowers γ = MonoidWithZeroHom.valueGroup v ∧ γ < 1

noncomputable def Valuation.IsRankOneDiscrete.generator {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

Γˣ

Given a discrete valuation v, Valuation.IsRankOneDiscrete.generator is a generator of the value group that is < 1.

Equations

Valuation.IsRankOneDiscrete.generator v = ⋯.choose

Instances For

theorem Valuation.IsRankOneDiscrete.generator_zpowers_eq_valueGroup {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

Subgroup.zpowers (generator v) = MonoidWithZeroHom.valueGroup v

theorem Valuation.IsRankOneDiscrete.generator_mem_valueGroup {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

generator v ∈ MonoidWithZeroHom.valueGroup v

theorem Valuation.IsRankOneDiscrete.generator_lt_one {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

generator v < 1

theorem Valuation.IsRankOneDiscrete.generator_ne_one {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

generator v ≠ 1

theorem Valuation.IsRankOneDiscrete.generator_zpowers_eq_range {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (K : Type u_3) [Field K] (w : Valuation K Γ) [w.IsRankOneDiscrete] :

Units.val '' ↑(Subgroup.zpowers (generator w)) = Set.range ⇑w \ {0}

theorem Valuation.IsRankOneDiscrete.generator_mem_range {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] (K : Type u_3) [Field K] (w : Valuation K Γ) [w.IsRankOneDiscrete] :

↑(generator w) ∈ Set.range ⇑w

theorem Valuation.IsRankOneDiscrete.generator_ne_zero {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

↑(generator v) ≠ 0

instance Valuation.IsRankOneDiscrete.instIsCyclicSubtypeUnitsMemSubgroupValueGroup {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

IsCyclic ↥(MonoidWithZeroHom.valueGroup v)

instance Valuation.IsRankOneDiscrete.instNontrivialSubtypeUnitsMemSubgroupValueGroup {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

Nontrivial ↥(MonoidWithZeroHom.valueGroup v)

instance Valuation.IsRankOneDiscrete.instNontrivialSubtypeUnitsMemSubmonoidValueMonoid {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

Nontrivial ↥(MonoidWithZeroHom.valueMonoid v)

instance Valuation.IsRankOneDiscrete.instIsNontrivial {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

theorem Valuation.IsRankOneDiscrete.valueGroup_genLTOne_eq_generator {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [v.IsRankOneDiscrete] :

LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.valueGroup v) = generator v

def Valuation.IsUniformizer {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [hv : v.IsRankOneDiscrete] (π : A) :

An element π : A is a uniformizer if v π is a generator of the value group that is < 1.

Equations

v.IsUniformizer π = (v π = ↑(Valuation.IsRankOneDiscrete.generator v))

Instances For

theorem Valuation.IsUniformizer.iff {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} :

v.IsUniformizer π ↔ v π = ↑(IsRankOneDiscrete.generator v)

theorem Valuation.IsUniformizer.ne_zero {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) :

π ≠ 0

@[simp]

theorem Valuation.IsUniformizer.val {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) :

v π = ↑(IsRankOneDiscrete.generator v)

theorem Valuation.IsUniformizer.val_lt_one {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) :

v π < 1

theorem Valuation.IsUniformizer.val_ne_zero {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) :

v π ≠ 0

theorem Valuation.IsUniformizer.val_pos {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) :

0 < v π

theorem Valuation.IsUniformizer.zpowers_eq_valueGroup {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {π : A} (hπ : v.IsUniformizer π) :

MonoidWithZeroHom.valueGroup v = Subgroup.zpowers (Units.mk0 (v π) ⋯)

structure Valuation.Uniformizer {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] (v : Valuation A Γ) [hv : v.IsRankOneDiscrete] :

Type u_2

The structure Uniformizer bundles together the term in the ring and a proof that it is a uniformizer.

val : ↥v.integer
The integer underlying a Uniformizer
valuation_gt_one : v.IsUniformizer ↑self.val

Instances For

theorem Valuation.Uniformizer.ext {Γ : Type u_1} {inst✝ : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst✝¹ : Ring A} {v : Valuation A Γ} {hv : v.IsRankOneDiscrete} {x y : v.Uniformizer} (val : x.val = y.val) :

x = y

theorem Valuation.Uniformizer.ext_iff {Γ : Type u_1} {inst✝ : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst✝¹ : Ring A} {v : Valuation A Γ} {hv : v.IsRankOneDiscrete} {x y : v.Uniformizer} :

x = y ↔ x.val = y.val

def Valuation.Uniformizer.mk' {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] {x : A} (hx : v.IsUniformizer x) :

A constructor for Uniformizer.

Equations

Valuation.Uniformizer.mk' hx = { val := ⟨x, ⋯⟩, valuation_gt_one := hx }

Instances For

instance Valuation.Uniformizer.instCoeSubtypeMemSubringInteger {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] :

Coe v.Uniformizer ↥v.integer

Equations

Valuation.Uniformizer.instCoeSubtypeMemSubringInteger = { coe := fun (π : v.Uniformizer) => π.val }

theorem Valuation.Uniformizer.ne_zero {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [Ring A] {v : Valuation A Γ} [hv : v.IsRankOneDiscrete] (π : v.Uniformizer) :

↑π.val ≠ 0

theorem Valuation.IsUniformizer.not_isUnit {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [CommRing R] {v : Valuation R Γ} [hv : v.IsRankOneDiscrete] {π : ↥v.integer} (hπ : v.IsUniformizer ↑π) :

instance Valuation.IsRankOneDiscrete.mk' {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {R : Type u_2} [Ring R] (v : Valuation R Γ) [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] :

v.IsRankOneDiscrete

theorem Valuation.exists_isUniformizer_of_isCyclic_of_nontrivial {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] :

∃ (π : ↥v.valuationSubring), v.IsUniformizer ↑π

instance Valuation.instNonemptyUniformizer {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] :

Nonempty v.Uniformizer

theorem Valuation.IsUniformizer.of_associated {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] {v : Valuation K Γ} [hv : v.IsRankOneDiscrete] {π₁ π₂ : ↥v.valuationSubring} (h1 : v.IsUniformizer ↑π₁) (H : Associated π₁ π₂) :

v.IsUniformizer ↑π₂

An element associated to a uniformizer is itself a uniformizer.

theorem Valuation.associated_of_isUniformizer {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] {v : Valuation K Γ} [hv : v.IsRankOneDiscrete] {π₁ π₂ : ↥v.valuationSubring} (h1 : v.IsUniformizer ↑π₁) (h2 : v.IsUniformizer ↑π₂) :

Associated π₁ π₂

If two elements of K₀ are uniformizers, then they are associated.

theorem Valuation.exists_pow_Uniformizer {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] {v : Valuation K Γ} [hv : v.IsRankOneDiscrete] {r : ↥v.valuationSubring} (hr : r ≠ 0) (π : v.Uniformizer) :

∃ (n : ℕ) (u : (↥v.valuationSubring)ˣ), ↑r = ↑(π.val ^ n) * ↑↑u

theorem Valuation.Uniformizer.is_generator {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] {v : Valuation K Γ} [hv : v.IsRankOneDiscrete] (π : v.Uniformizer) :

IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {π.val}

theorem Valuation.IsUniformizer.is_generator {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] {v : Valuation K Γ} [hv : v.IsRankOneDiscrete] {π : ↥v.valuationSubring} (hπ : v.IsUniformizer ↑π) :

IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {π}

theorem Valuation.pow_Uniformizer_is_pow_generator {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] {v : Valuation K Γ} [hv : v.IsRankOneDiscrete] (π : v.Uniformizer) (n : ℕ) :

IsLocalRing.maximalIdeal ↥v.valuationSubring ^ n = Ideal.span {π.val ^ n}

theorem Valuation.valuationSubring_not_isField {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] :

¬IsField ↥v.valuationSubring

theorem Valuation.isUniformizer_of_maximalIdeal_eq_span {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [v.IsRankOneDiscrete] {r : ↥v.valuationSubring} (hr : IsLocalRing.maximalIdeal ↥v.valuationSubring = Ideal.span {r}) :

v.IsUniformizer ↑r

theorem Valuation.ideal_isPrincipal {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] (I : Ideal ↥v.valuationSubring) :

Submodule.IsPrincipal I

theorem Valuation.valuationSubring_isPrincipalIdealRing {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] :

IsPrincipalIdealRing ↥v.valuationSubring

instance Valuation.valuationSubring_isDiscreteValuationRing {Γ : Type u_1} [LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [Field K] (v : Valuation K Γ) [IsCyclic ↥(MonoidWithZeroHom.valueGroup v)] [Nontrivial ↥(MonoidWithZeroHom.valueGroup v)] :

IsDiscreteValuationRing ↥v.valuationSubring

This is Chapter I, Section 1, Proposition 1 in Serre's Local Fields

def IsDiscreteValuationRing.maximalIdeal (A : Type u_1) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] :

IsDedekindDomain.HeightOneSpectrum A

The maximal ideal of a discrete valuation ring.

Equations

IsDiscreteValuationRing.maximalIdeal A = { asIdeal := IsLocalRing.maximalIdeal A, isPrime := ⋯, ne_bot := ⋯ }

Instances For

instance IsDiscreteValuationRing.isRankOneDiscrete (A : Type u_1) (K : Type u_2) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] :

(IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)).IsRankOneDiscrete

theorem IsDiscreteValuationRing.exists_lift_of_le_one {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] {x : K} (H : (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)) x ≤ 1) :

∃ (a : A), (algebraMap A K) a = x

theorem IsDiscreteValuationRing.map_algebraMap_eq_valuationSubring {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] :

Subring.map (algebraMap A K) ⊤ = (IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)).valuationSubring.toSubring

noncomputable def IsDiscreteValuationRing.equivValuationSubring {A : Type u_1} {K : Type u_2} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] [Field K] [Algebra A K] [IsFractionRing A K] :

A ≃+* ↥(IsDedekindDomain.HeightOneSpectrum.valuation K (maximalIdeal A)).valuationSubring

The ring isomorphism between a DVR A and the valuation subring of a field of fractions of A endowed with the adic valuation of the maximal ideal.

Equations

IsDiscreteValuationRing.equivValuationSubring = (Subring.topEquiv.symm.trans (⊤.equivMapOfInjective (algebraMap A K) ⋯)).trans (RingEquiv.subringCongr ⋯)

Instances For