Galois totally and tamely ramified extensions

A totally and tamely ramified extension of nonarchimedean local fields, with ramification index e, is Galois exactly when the base field contains a primitive e-th root of unity, or equivalently when e divides the size of its residue field minus one. In that case a radical uniformizer identifies the Galois group with the e-th roots of unity in the base field by σ ↦ σ(α) / α.

The radical presentation comes from TamelyRamified.Basic; the splitting-field and automorphism constructions reuse Mathlib's FieldTheory.KummerExtension.

References

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

theorem TauCeti.IsTotallyRamified.isGalois_iff_ramificationIndex_dvd_card_residueField_sub_one {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) (ht : IsTamelyRamified K L) : IsGalois K L ↔ ramificationIndex K L ∣ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) - 1

A totally and tamely ramified extension is Galois exactly when its ramification index divides the size of the base residue field minus one.

theorem TauCeti.IsTotallyRamified.isGalois_iff_exists_isPrimitiveRoot {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) (ht : IsTamelyRamified K L) : IsGalois K L ↔ ∃ (ζ : K), IsPrimitiveRoot ζ (ramificationIndex K L)

A totally and tamely ramified extension with ramification index e is Galois exactly when the base field contains a primitive e-th root of unity.

theorem TauCeti.IsTotallyRamified.exists_pow_eq_uniformizer_and_autEquivRootsOfUnity {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] [IsGalois K L] (h : IsTotallyRamified K L) (ht : IsTamelyRamified K L) : ∃ (π : Kˣ) (α : Lˣ), IsUniformizer K π ∧ IsUniformizer L α ∧ ↑α ^ ramificationIndex K L = (algebraMap K L) ↑π ∧ K⟮↑α⟯ = ⊤ ∧ ∃ (Φ : Gal(L/K) ≃* ↥(rootsOfUnity (ramificationIndex K L) K)), ∀ (σ : Gal(L/K)), (algebraMap K L) ↑↑(Φ σ) = σ ↑α / ↑α

In a totally and tamely ramified Galois extension, a radical uniformizer identifies the Galois group with the roots of unity in the base field by σ ↦ σ(α) / α.