Tamely ramified extensions of local fields

Let L/K be an extension of nonarchimedean local fields which is tamely ramified, so that the residue characteristic p does not divide e = e(L/K).

When L/K is Galois, tameness is read off the lower ramification filtration: the wild inertia group G_1 is the Sylow p-subgroup of the inertia group G_0, whose order is e, so G_1 is trivial exactly when L/K is tamely ramified.

When L/K is moreover totally ramified, e(L/K) = [L : K], this file proves the structure theorem for such extensions: L is obtained from K by adjoining an e-th root of a uniformizer of K,

L = K(α) with α ^ e = π for a uniformizer π of K,

and the root α is then a uniformizer of L. Tameness cannot be dropped: ℚ₂(√-1)/ℚ₂ is totally ramified of degree 2, but contains no square root of a uniformizer of ℚ₂, since -1 has even valuation and lies in a different square class from every uniformizer.

Main results

• TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroup_one: for L/K Galois, the order of G_1 is the residue-characteristic part of the ramification index.
• TauCeti.LocalFieldsRamification.lowerRamificationGroup_one_eq_bot_iff_isTamelyRamified: for L/K Galois, G_1 = 1 if and only if L/K is tamely ramified.
• TauCeti.IsTamelyRamified.ramificationIndex_dvd_card_residueField_sub_one: for L/K Galois and tamely ramified, e(L/K) divides #𝓀[L] - 1.
• TauCeti.IsTotallyRamified.exists_pow_eq_uniformizer_of_isTamelyRamified: a totally and tamely ramified extension of degree e is generated by an e-th root of a uniformizer of K, and that root is a uniformizer of L.

References

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

theorem TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroup_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] [Module.Finite K L] [IsGalois K L] : Nat.card ↥(lowerRamificationGroup K L 1) = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ (ramificationIndex K L).factorization (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer))

The order of wild inertia is the residue-characteristic part of the ramification index: #G_1(L/K) = p ^ (v_p e(L/K)).

@[simp]

theorem TauCeti.LocalFieldsRamification.lowerRamificationGroup_one_eq_bot_iff_isTamelyRamified (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] [Module.Finite K L] [IsGalois K L] : lowerRamificationGroup K L 1 = ⊥ ↔ IsTamelyRamified K L

Wild inertia is trivial exactly in the tame case. For a finite Galois extension L/K of nonarchimedean local fields, the first lower ramification group G_1 is trivial if and only if L/K is tamely ramified: G_1 is the Sylow p-subgroup of the inertia group G_0, which has order e(L/K).

theorem TauCeti.IsTamelyRamified.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] [Module.Finite K L] [IsGalois K L] (ht : IsTamelyRamified K L) : ramificationIndex K L ∣ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation L).integer) - 1

The tame ramification index divides q - 1. For a tamely ramified finite Galois extension L/K of nonarchimedean local fields, e(L/K) divides #𝓀[L] - 1: the inertia group G_0, of order e(L/K), meets the wild inertia group G_1 trivially, and G_0 / G_1 embeds into 𝓀[L]ˣ through the tame character.

theorem TauCeti.IsTotallyRamified.exists_pow_eq_uniformizer_of_isTamelyRamified {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) : ∃ (π : Kˣ) (α : Lˣ), IsUniformizer K π ∧ IsUniformizer L α ∧ ↑α ^ ramificationIndex K L = (algebraMap K L) ↑π ∧ K⟮↑α⟯ = ⊤

Totally and tamely ramified extensions are radical. If L/K is a totally and tamely ramified extension of nonarchimedean local fields, of degree e = e(L/K), then there are a uniformizer π of K and a uniformizer α of L with α ^ e = π and L = K(α).