Finite unramified extensions and residue fields

Reduction identifies finite unramified extensions of a nonarchimedean local field K with finite extensions of its residue field. The fully faithful part is TauCeti.IsUnramified.residueFieldHomEquiv: reduction gives an equivalence between embeddings of an unramified extension and embeddings of residue fields.

This file proves essential surjectivity. Given a finite extension k/𝓀[K], the canonical unramified extension of K whose degree is [k : 𝓀[K]] has residue field isomorphic to k over 𝓀[K]. Thus every finite residue-field extension occurs, while the chosen residue isomorphism records the noncanonical data needed to compare abstract extensions.

Main result

• TauCeti.nonempty_residueFieldAlgEquiv_unramifiedExtension: every finite extension of the residue field is the residue field of the canonical unramified extension of the same degree.

References

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

theorem TauCeti.nonempty_residueFieldAlgEquiv_unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (k : Type u_3) [Field k] [Algebra (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) k] [Module.Finite (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) k] : have f := Module.finrank (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) k; let L := unramifiedExtension K Ω f; Nonempty (IsLocalRing.ResidueField ↥(ValuativeRel.valuation ↥L).integer ≃ₐ[IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer] k)

Every finite residue-field extension has an unramified lift. Let k/𝓀[K] be finite and put f = [k : 𝓀[K]]. With the canonical local-field structure on unramifiedExtension K Ω f, its residue field is isomorphic to k over 𝓀[K].

Together with IsUnramified.residueFieldHomEquiv, this is the object-existence half of the equivalence between finite unramified extensions of K and finite extensions of 𝓀[K].