Integral generators of finite local-field extensions

The integer ring of a finite extension of nonarchimedean local fields is generated by one integral element over the base integer ring. An integral power basis can be chosen whose generator also generates the field extension and whose length is the field degree. These results let ramification and different computations use a generator without imposing a separate monogenicity hypothesis. When the extension is totally ramified, every uniformizer ϖ of L is such a generator, so 1, ϖ, …, ϖ^{e - 1} is a basis of 𝒪[L] over 𝒪[K], with e = [L : K]. In that basis the additive valuation of an element of 𝒪[L] is read off from its coordinates.

Main results

• TauCeti.exists_integerRing_adjoin_eq_top: 𝒪[L] is monogenic over 𝒪[K].
• TauCeti.IsTotallyRamified.integralPowerBasis: the power basis of 𝒪[L] over 𝒪[K] generated by a uniformizer of a totally ramified extension, of length e(L/K).
• TauCeti.IsTotallyRamified.addVal_eq_iInf_integralPowerBasis_repr: the additive valuation of x ∈ 𝒪[L] is the least of e(L/K) · v_K(a_i) + i over the coordinates a_i of x in that basis.

References

• J.-P. Serre, Corps Locaux, Chapter I, §6, Proposition 18.
• J.-P. Serre, Corps Locaux, Chapter III, §6, Proposition 12.

theorem TauCeti.exists_integerRing_adjoin_eq_top (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ∃ (x : ↥(ValuativeRel.valuation L).integer), (↥(ValuativeRel.valuation K).integer)[x] = ⊤

The integer ring of a finite extension of nonarchimedean local fields is generated as an algebra over the base integer ring by one element.

theorem TauCeti.exists_integerRing_powerBasis_intermediateField_adjoin_eq_top_and_dim_eq_finrank (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : ∃ (pb : PowerBasis ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer), K⟮↑pb.gen⟯ = ⊤ ∧ pb.dim = Module.finrank K L

The integer ring of a finite local-field extension has an integral power basis whose generator also generates the field extension. Its length is [L : K].

theorem TauCeti.IsTotallyRamified.adjoin_eq_top_of_irreducible {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) : (↥(ValuativeRel.valuation K).integer)[ϖ] = ⊤

In a totally ramified extension of nonarchimedean local fields, every uniformizer of L generates 𝒪[L] as an 𝒪[K]-algebra.

noncomputable def TauCeti.IsTotallyRamified.integralPowerBasis {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) : PowerBasis ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

The integral power basis of a totally ramified extension. In a totally ramified extension L/K of nonarchimedean local fields, the powers 1, ϖ, …, ϖ^{e - 1} of a uniformizer ϖ of L form a basis of 𝒪[L] over 𝒪[K], where e = e(L/K) = [L : K].

Equations

• h.integralPowerBasis hϖ = PowerBasis.ofAdjoinEqTop' ⋯ ⋯

@[simp]

theorem TauCeti.IsTotallyRamified.integralPowerBasis_gen {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) : (h.integralPowerBasis hϖ).gen = ϖ

The integral power basis of a totally ramified extension is generated by the chosen uniformizer.

@[simp]

theorem TauCeti.IsTotallyRamified.integralPowerBasis_dim {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) : (h.integralPowerBasis hϖ).dim = ramificationIndex K L

The integral power basis of a totally ramified extension has length e(L/K).

theorem TauCeti.IsTotallyRamified.addVal_eq_iInf_integralPowerBasis_repr {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (h : IsTotallyRamified K L) {ϖ : ↥(ValuativeRel.valuation L).integer} (hϖ : Irreducible ϖ) (x : ↥(ValuativeRel.valuation L).integer) : (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation L).integer) x = ⨅ (i : Fin (h.integralPowerBasis hϖ).dim), ramificationIndex K L • (IsDiscreteValuationRing.addVal ↥(ValuativeRel.valuation K).integer) (((h.integralPowerBasis hϖ).basis.repr x) i) + ↑↑i

Valuations in the integral power basis. In a totally ramified extension L/K with uniformizer ϖ, the additive valuation of x ∈ 𝒪[L] is the least of e(L/K) · v_K(a_i) + i, where x = ∑ a_i ϖ^i is the expansion of x in the integral power basis.