Discrete Valuations

A valuation v : A → ℤₘ₀ on a ring A is said to be a (normalized) discrete valuation if ofAdd (-1 : ℤ) belongs to the image of v. Note that valuations in Mathlib are multiplicative; if a : A → ℤ ∪ {infty} is the additive valuation associated to v, this is equivalent to asking that 1 : ℤ belongs to the image of a.

Main Definitions

• IsDiscrete: We define a valuation to be discrete if it is ℤₘ₀-valued and ofAdd (-1 : ℤ) belongs to the image.

TODO

• Define (pre)uniformizers for nontrivial ℤₘ₀-valued valuations.
• Relate discrete valuations and discrete valuation rings.

class Valuation.IsDiscrete {A : Type u_1} [Ring A] (v : Valuation A (WithZero (Multiplicative ℤ))) : Prop

A valuation v on a ring A is (normalized) discrete if it is ℤₘ₀-valued and ofAdd (-1 : ℤ) belongs to the image. Note that the latter is equivalent to asking that 1 : ℤ belongs to the image of the corresponding additive valuation.

• one_mem_range : ↑(Multiplicative.ofAdd (-1)) ∈ Set.range ⇑v

theorem Valuation.IsDiscrete.surj {K : Type u_2} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) [hv : v.IsDiscrete] : Function.Surjective ⇑v

A discrete valuation on a field K is surjective.

theorem Valuation.isDiscrete_iff_surjective {K : Type u_2} [Field K] (v : Valuation K (WithZero (Multiplicative ℤ))) : v.IsDiscrete ↔ Function.Surjective ⇑v

A ℤₘ₀-valued valuation on a field K is discrete if and only if it is surjective.