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,

TODO

• Define (pre)uniformizers for nontrivial discrete valuations.
• 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 Γ) : Prop

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

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

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_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)