The zero-preserving Teichmüller lift of a nonarchimedean local field

For a nonarchimedean local field K, TauCeti.teichmuller 𝒪[K] is the canonical multiplicative section 𝓀[K]ˣ →* 𝒪[K]ˣ. This file adds its zero-preserving extension teichmullerLift K : 𝓀[K] →*₀ 𝒪[K], obtained from Mathlib's Perfection.teichmuller₀, and proves that the two constructions agree on units. It also records that, for q = #𝓀[K] and f ≠ 0, q ^ f - 1 is a unit in 𝒪[K], and that an exponent prime to the residue characteristic p is nonzero.

Main definitions

• TauCeti.teichmullerLift: the zero-preserving Teichmüller lift 𝓀[K] →*₀ 𝒪[K].

Main results

• TauCeti.residue_teichmullerLift: the lift is a section of reduction.
• TauCeti.isUnit_natCast_natCard_pow_sub_one: for f ≠ 0, q ^ f - 1 is a unit in 𝒪[K].
• TauCeti.ne_zero_of_coprime_ringChar: an exponent m prime to p is nonzero.
• TauCeti.exists_isPrimitiveRoot_natCard_residueField_sub_one: K contains a primitive (q - 1)-st root of unity.
• TauCeti.eq_teichmullerLift_iff: an element of 𝒪[K] is teichmullerLift K a exactly when it reduces to a and is fixed by the q-th power map.
• TauCeti.teichmullerLift_unique: it is the unique zero-preserving multiplicative section of reduction.
• AlgEquiv.smul_teichmullerLift: local-field automorphisms commute with the Teichmüller lift through their residue-field action.

References

• J.-P. Serre, Corps Locaux, II §4.
• J. Neukirch, Algebraic Number Theory, II §5.

noncomputable def TauCeti.teichmullerLift (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer →*₀ ↥(ValuativeRel.valuation K).integer

The zero-preserving Teichmüller lift 𝓀[K] →*₀ 𝒪[K].

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.residue_teichmullerLift (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) : (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) ((teichmullerLift K) a) = a

The zero-preserving Teichmüller lift is a section of reduction.

theorem TauCeti.teichmullerLift_pow_natCard (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) : (teichmullerLift K) a ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) = (teichmullerLift K) a

Each Teichmüller representative is fixed by the q-th power map.

@[simp]

theorem TauCeti.teichmullerLift_pow_fintype_card (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) : (teichmullerLift K) a ^ Fintype.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) = (teichmullerLift K) a

The simplifier-normalized form of the Frobenius equation for the zero-preserving lift.

theorem TauCeti.isUnit_natCast_natCard_pow_sub_one (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {f : ℕ} (hf : f ≠ 0) : IsUnit ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - 1)

For f ≠ 0, q ^ f - 1 is prime to the residue characteristic, so it is a unit in 𝒪[K]; here q is the cardinality of 𝓀[K].

theorem TauCeti.ne_zero_of_coprime_ringChar {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {m : ℕ} (hm : m.Coprime (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))) : m ≠ 0

An exponent prime to the residue characteristic is nonzero.

theorem TauCeti.exists_isPrimitiveRoot_natCard_residueField_sub_one (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ∃ (ζ : K), IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1)

A nonarchimedean local field contains a primitive (q - 1)-st root of unity, where q is the cardinality of its residue field: the Teichmüller lifts of the units of 𝓀[K] are the (q - 1)-st roots of unity of K, and 𝓀[K]ˣ is cyclic.

@[simp]

theorem TauCeti.coe_teichmuller_apply (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (a : (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)ˣ) : ↑((teichmuller ↥(ValuativeRel.valuation K).integer) a) = (teichmullerLift K) ↑a

On units, the zero-preserving lift is the Henselian-local-ring Teichmüller lift.

theorem TauCeti.eq_teichmullerLift_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer} {x : ↥(ValuativeRel.valuation K).integer} : x = (teichmullerLift K) a ↔ (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) x = a ∧ x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) = x

An element of 𝒪[K] is teichmullerLift K a exactly when it reduces to a and is fixed by the q-th power map.

theorem TauCeti.teichmullerLift_unique (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (f : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer →*₀ ↥(ValuativeRel.valuation K).integer) (hsection : ∀ (a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer), (IsLocalRing.residue ↥(ValuativeRel.valuation K).integer) (f a) = a) : f = teichmullerLift K

The zero-preserving Teichmüller lift is the unique multiplicative section of reduction.

@[simp]

theorem AlgEquiv.smul_teichmullerLift {K : Type u_2} {L : Type u_3} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] (σ : Gal(L/K)) (a : IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) : σ • (TauCeti.teichmullerLift L) a = (TauCeti.teichmullerLift L) (σ • a)

An automorphism of a finite local-field extension carries each Teichmüller representative to the representative of its residue-field image.