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 that ofAdd (-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 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].

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.ofClass v).valueGroup ∧ γ < 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.ofClass v).valueGroup ∧ γ < 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 an element of Γ which 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.ofClass v).valueGroup

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

generator v ∈ (MonoidWithZeroHom.ofClass v).valueGroup

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

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

↥(MonoidWithZeroHom.ofClass v).valueGroup

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

Equations

Valuation.IsRankOneDiscrete.generator' v = ⟨Valuation.IsRankOneDiscrete.generator v, ⋯⟩

Instances For

@[simp]

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

MonoidWithZeroHom.ValueGroup₀.embedding ↑(generator' v) = ↑(generator v)

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

Subgroup.zpowers (generator' 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

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

IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup

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.ofClass v).valueGroup = generator v

theorem Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range {A : Type u_2} [Ring A] {v : Valuation A (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete] (hπ : WithZero.exp (-1) ∈ Set.range ⇑v) :

generator v = Units.mk0 (WithZero.exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

The generator of a discrete valuation in ℤᵐ⁰ that contains exp (-1) in its range is equal to exp (-1).

theorem Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective {A : Type u_2} [Ring A] {v : Valuation A (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete] (hsurj : Function.Surjective ⇑v) :

generator v = Units.mk0 (WithZero.exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

The generator of a surjective discrete valuation in ℤᵐ⁰ is equal to exp (-1).

@[deprecated Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_surjective (since := "2026-04-01")]

theorem Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective {A : Type u_2} [Ring A] {v : Valuation A (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete] (hsurj : Function.Surjective ⇑v) :

generator v = Units.mk0 (WithZero.exp (-1)) generator_eq_exp_neg_one_of_mem_range._proof_1

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.ofClass v).valueGroup = 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_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

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

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

@[implicit_reducible]

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.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup] :

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.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup] :

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

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

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.ofClass v).valueGroup] [IsCyclic ↥(MonoidWithZeroHom.ofClass v).valueGroup] :

¬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.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup] (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.ofClass v).valueGroup] [Nontrivial ↥(MonoidWithZeroHom.ofClass v).valueGroup] :

IsPrincipalIdealRing ↥v.valuationSubring

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

IsDiscreteValuationRing ↥v.valuationSubring

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