Uniformizers of a nonarchimedean local field

This file records the uniformizer predicate for a nonarchimedean local field. It is formulated on Kˣ, where the normalized valuation is defined. The characterization below connects it with the irreducible elements of the ring of integers, the convention used by the local-fields infrastructure.

def TauCeti.IsUniformizer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (π : Kˣ) : Prop

A uniformizer is a nonzero field element whose normalized valuation is one.

Equations

• TauCeti.IsUniformizer K π = ((TauCeti.normalizedValuation K) π = Multiplicative.ofAdd 1)

@[simp]

theorem TauCeti.isUniformizer_def {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (π : Kˣ) : IsUniformizer K π ↔ (normalizedValuation K) π = Multiplicative.ofAdd 1

theorem TauCeti.isUniformizer_iff_exists_irreducible (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (π : Kˣ) : IsUniformizer K π ↔ ∃ (ϖ : ↥(ValuativeRel.valuation K).integer), Irreducible ϖ ∧ ↑ϖ = ↑π

A field unit is a uniformizer iff its underlying element is the image of an irreducible element of the ring of integers.

theorem TauCeti.exists_isUniformizer (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ∃ (π : Kˣ), IsUniformizer K π

Uniformizers exist in every nonarchimedean local field.