The maximal tamely ramified extension and wild inertia

Let K be a nonarchimedean local field with residue field 𝓀[K] of characteristic p and cardinality q, and let Ω be an extension of K. This file defines the maximal tamely ramified extension

TauCeti.maximalTameExtension K Ω,

the intermediate field K^{t} of Ω / K generated by the m-th roots of the nonzero elements of K, for all m prime to p. It contains the maximal unramified extension K^{ur}, whose generators are roots of unity of order prime to p, and it is Galois over K when Ω is separably closed. For any uniformizer π of K it is the familiar

K^{t} = K^{ur}(π^{1/m} : p ∤ m) = ⋃_{p ∤ m} K^{ur}(π^{1/m}),

since for a unit u of K and p ∤ m the roots of X^m − u are unramified: u is a root of unity of order prime to p times a principal unit, and principal units are m-th powers in K.

The wild inertia subgroup P_K = TauCeti.wildInertiaSubgroup K of the absolute Galois group G_K = Field.absoluteGaloisGroup K is the fixing subgroup of K^{t} inside K^{alg}, which IntermediateField.fixingSubgroupEquiv identifies with Gal(K^{alg}/K^{t}). It is a closed normal subgroup of G_K, contained in the inertia subgroup I_K = TauCeti.inertiaSubgroup K.

At finite level, P_K is the inverse limit of the wild inertia groups G_1 of the finite normal subextensions L of K^{alg}/K: an automorphism lies in P_K exactly when each of its restrictions lies in the first lower ramification group G_1 of L/K. As each G_1 is a p-group, P_K is pro-p; conversely every pro-p subgroup of I_K fixes the tame radicals, since I_K acts on them through roots of unity of order prime to p. So P_K is the largest pro-p subgroup of I_K: it is the unique Sylow pro-p subgroup of I_K.

Restriction to a finite Galois subextension L maps I_K onto the inertia group G_0 of L/K, and a continuous surjection carries a Sylow pro-p subgroup onto a Sylow subgroup; since G_1 is the unique Sylow p-subgroup of G_0, the image of P_K is all of G_1. Consequently L lies in K^{t} exactly when G_1 of L/K is trivial, that is, exactly when L/K is tamely ramified.

Being a normal pro-p subgroup, P_K can be discarded when counting topological generators of G_K, up to its commutator subgroup: by the Frattini argument along P_K, a set generating G_K modulo ⁅P_K, P_K⁆ already generates G_K.

Main definitions

• TauCeti.maximalTameExtension K Ω: the maximal tamely ramified extension K^{t} of K in Ω.
• TauCeti.wildInertiaSubgroup K: the wild inertia subgroup P_K of G_K.

Main results

• TauCeti.maximalUnramifiedExtension_le_maximalTameExtension: K^{ur} ≤ K^{t}.
• TauCeti.isGalois_maximalTameExtension: for Ω separably closed, K^{t} is Galois over K.
• TauCeti.maximalTameExtension_eq_sup_adjoin: for Ω separably closed and any uniformizer π, K^{t} = K^{ur}(π^{1/m} : p ∤ m).
• TauCeti.isClosed_wildInertiaSubgroup, TauCeti.wildInertiaSubgroup_normal: P_K is closed and normal in G_K.
• TauCeti.wildInertiaSubgroup_le_inertiaSubgroup: P_K ≤ I_K.
• TauCeti.restrictNormal_mem_lowerRamificationGroup_one: the restriction of an element of P_K to a finite normal subextension L lies in G_1 of L/K.
• TauCeti.mem_wildInertiaSubgroup_iff_forall_restrictNormal_mem: P_K is the inverse limit of the finite-level groups G_1.
• TauCeti.isProP_wildInertiaSubgroup: P_K is pro-p.
• TauCeti.le_wildInertiaSubgroup_of_isProP: every pro-p subgroup of I_K lies in P_K.
• TauCeti.isProPSylow_wildInertiaSubgroup and TauCeti.eq_subgroupOf_wildInertiaSubgroup_of_isProPSylow: P_K is the unique Sylow pro-p subgroup of I_K.
• TauCeti.topologicalClosure_eq_top_of_sup_wildInertiaCommutator: a set topologically generating G_K together with ⁅P_K, P_K⁆ topologically generates G_K.
• TauCeti.map_wildInertiaSubgroup_restrictNormalHom: the image of P_K in the Galois group of a finite Galois subextension L is the first lower ramification group G_1 of L/K.
• TauCeti.le_maximalTameExtension_iff: a finite Galois subextension L lies in K^{t} exactly when L/K is tamely ramified.
• TauCeti.mem_wildInertiaSubgroup_iff_of_isUniformizer: σ ∈ P_K exactly when σ ∈ I_K and σ fixes every m-th root of a given uniformizer, for p ∤ m.

References

• J.-P. Serre, Corps Locaux, Chapter IV, §2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (3.9.1) and Chapter VII, §5.

The maximal tamely ramified extension

def TauCeti.maximalTameExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : IntermediateField K Ω

The maximal tamely ramified extension K^{t} of a nonarchimedean local field K inside an extension Ω: the intermediate field generated by the m-th roots of the nonzero elements of K, for all m not divisible by the residue characteristic p. It contains the maximal unramified extension, and for a uniformizer π of K and Ω separably closed it is K^{ur}(π^{1/m} : p ∤ m) by TauCeti.maximalTameExtension_eq_sup_adjoin.

Equations

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

theorem TauCeti.maximalTameExtension_def (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : maximalTameExtension K Ω = IntermediateField.adjoin K {x : Ω | ∃ (m : ℕ), ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ m ∧ ∃ (a : Kˣ), x ^ m = (algebraMap K Ω) ↑a}

The maximal tamely ramified extension is generated by the m-th roots of the nonzero elements of K, for m prime to the residue characteristic.

theorem TauCeti.mem_maximalTameExtension_of_pow_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {m : ℕ} (hm : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ m) (a : Kˣ) {x : Ω} (hx : x ^ m = (algebraMap K Ω) ↑a) : x ∈ maximalTameExtension K Ω

An m-th root of a nonzero element of K lies in the maximal tamely ramified extension, when the residue characteristic does not divide m.

theorem TauCeti.maximalUnramifiedExtension_le_maximalTameExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : maximalUnramifiedExtension K Ω ≤ maximalTameExtension K Ω

The maximal unramified extension is tamely ramified: K^{ur} ≤ K^{t}, since K^{ur} is generated by roots of unity of order q ^ f − 1, which is prime to the residue characteristic.

instance TauCeti.isGalois_maximalTameExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : IsGalois K ↥(maximalTameExtension K Ω)

The maximal tamely ramified extension is Galois over K, when Ω is separably closed: it is the compositum of the splitting fields of the separable polynomials X^m − a, a ∈ Kˣ, p ∤ m.

theorem TauCeti.maximalTameExtension_eq_sup_adjoin {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {π : Kˣ} (hπ : IsUniformizer K π) : maximalTameExtension K Ω = maximalUnramifiedExtension K Ω ⊔ IntermediateField.adjoin K {x : Ω | ∃ (m : ℕ), ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ m ∧ x ^ m = (algebraMap K Ω) ↑π}

The maximal tamely ramified extension, through a uniformizer. For Ω separably closed and any uniformizer π of K, K^{t} is generated over the maximal unramified extension by the m-th roots of π, for m prime to the residue characteristic: K^{t} = K^{ur}(π^{1/m} : p ∤ m).

The wild inertia subgroup

noncomputable def TauCeti.wildInertiaSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Subgroup (Field.absoluteGaloisGroup K)

The wild inertia subgroup P_K of the absolute Galois group of a nonarchimedean local field K: the automorphisms of the algebraic closure fixing the maximal tamely ramified extension K^{t}. Through IntermediateField.fixingSubgroupEquiv it is Gal(K^{alg}/K^{t}).

Equations

• TauCeti.wildInertiaSubgroup K = (TauCeti.maximalTameExtension K (AlgebraicClosure K)).fixingSubgroup

theorem TauCeti.wildInertiaSubgroup_def (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : wildInertiaSubgroup K = (maximalTameExtension K (AlgebraicClosure K)).fixingSubgroup

The wild inertia subgroup is the fixing subgroup of the maximal tamely ramified extension.

@[simp]

theorem TauCeti.mem_wildInertiaSubgroup_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} : σ ∈ wildInertiaSubgroup K ↔ ∀ x ∈ maximalTameExtension K (AlgebraicClosure K), σ x = x

An automorphism lies in the wild inertia subgroup exactly when it fixes every element of the maximal tamely ramified extension.

theorem TauCeti.mem_wildInertiaSubgroup_iff_pow_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} : σ ∈ wildInertiaSubgroup K ↔ ∀ (m : ℕ), ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ m → ∀ (a : Kˣ) (x : AlgebraicClosure K), x ^ m = (algebraMap K (AlgebraicClosure K)) ↑a → σ x = x

Wild inertia, through radicals. An automorphism of K^{alg} lies in the wild inertia subgroup exactly when it fixes every m-th root of every nonzero element of K, for m prime to the residue characteristic.

theorem TauCeti.isClosed_wildInertiaSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsClosed ↑(wildInertiaSubgroup K)

The wild inertia subgroup is closed in the Krull topology.

instance TauCeti.wildInertiaSubgroup_normal (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (wildInertiaSubgroup K).Normal

The wild inertia subgroup is normal, since K^{t}/K is normal.

theorem TauCeti.wildInertiaSubgroup_le_inertiaSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : wildInertiaSubgroup K ≤ inertiaSubgroup K

Wild inertia lies in inertia: P_K ≤ I_K, since K^{ur} ≤ K^{t}.

theorem TauCeti.mem_wildInertiaSubgroup_iff_of_isUniformizer {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {π : Kˣ} (hπ : IsUniformizer K π) {σ : Field.absoluteGaloisGroup K} : σ ∈ wildInertiaSubgroup K ↔ σ ∈ inertiaSubgroup K ∧ ∀ (m : ℕ), ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ m → ∀ (x : AlgebraicClosure K), x ^ m = (algebraMap K (AlgebraicClosure K)) ↑π → σ x = x

Wild inertia, through a uniformizer. For a uniformizer π of K, an automorphism of K^{alg} lies in the wild inertia subgroup exactly when it lies in the inertia subgroup and fixes every m-th root of π, for m prime to the residue characteristic.

Wild inertia at finite level

theorem TauCeti.restrictNormal_mem_lowerRamificationGroup_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] [FiniteDimensional K ↥L] [Normal K ↥L] {σ : Gal(AlgebraicClosure K/K)} (hσ : σ ∈ wildInertiaSubgroup K) : σ.restrictNormal ↥L ∈ LocalFieldsRamification.lowerRamificationGroup K (↥L) 1

Wild inertia restricts into G_1. The restriction of an element of the wild inertia subgroup P_K to a finite normal subextension L of K^{alg}/K lies in the first ramification group G_1 of L/K.

theorem TauCeti.mem_wildInertiaSubgroup_iff_forall_restrictNormal_mem {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Gal(AlgebraicClosure K/K)} : σ ∈ wildInertiaSubgroup K ↔ ∀ (L : IntermediateField K (AlgebraicClosure K)) [inst : ValuativeRel ↥L] [inst_1 : TopologicalSpace ↥L] [inst_2 : IsNonarchimedeanLocalField ↥L] [inst_3 : ValuativeExtension K ↥L] [inst_4 : FiniteDimensional K ↥L] [inst_5 : Normal K ↥L], σ.restrictNormal ↥L ∈ LocalFieldsRamification.lowerRamificationGroup K (↥L) 1

Wild inertia is the inverse limit of the finite-level G_1. An automorphism σ of K^{alg} lies in the wild inertia subgroup P_K exactly when, for every finite normal subextension L of K^{alg}/K, its restriction to L lies in the first ramification group G_1 of L/K.

Wild inertia is the pro-p Sylow subgroup of inertia

theorem TauCeti.isProP_wildInertiaSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] : IsProP p ↥(wildInertiaSubgroup K)

Wild inertia is pro-p, for p the residue characteristic.

theorem TauCeti.le_wildInertiaSubgroup_of_isProP {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] {R : Subgroup (Field.absoluteGaloisGroup K)} (hR : IsProP p ↥R) (hRI : R ≤ inertiaSubgroup K) : R ≤ wildInertiaSubgroup K

Wild inertia is the largest pro-p subgroup of inertia: every pro-p subgroup of G_K contained in the inertia subgroup I_K is contained in P_K.

theorem TauCeti.isProPSylow_wildInertiaSubgroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] : IsProPSylow p ((wildInertiaSubgroup K).subgroupOf (inertiaSubgroup K))

Wild inertia is the pro-p Sylow subgroup of inertia: P_K, viewed as a subgroup of the inertia subgroup I_K, is a Sylow pro-p subgroup of I_K, for p the residue characteristic.

theorem TauCeti.eq_subgroupOf_wildInertiaSubgroup_of_isProPSylow (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] {Q : Subgroup ↥(inertiaSubgroup K)} (hQ : IsProPSylow p Q) : Q = (wildInertiaSubgroup K).subgroupOf (inertiaSubgroup K)

Uniqueness of the Sylow subgroup: P_K is the only Sylow pro-p subgroup of the inertia subgroup I_K, for p the residue characteristic, since it is normal.

The Frattini argument along wild inertia

theorem TauCeti.topologicalClosure_eq_top_of_sup_wildInertiaCommutator {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {s : Set (Field.absoluteGaloisGroup K)} (hs : (Subgroup.closure s ⊔ ⁅wildInertiaSubgroup K, wildInertiaSubgroup K⁆).topologicalClosure = ⊤) : (Subgroup.closure s).topologicalClosure = ⊤

Relative Frattini reduction along wild inertia (NSW (3.9.1)). A set which topologically generates G_K together with the commutator subgroup ⁅P_K, P_K⁆ of wild inertia already topologically generates G_K.

The image of wild inertia at finite level

@[simp]

theorem TauCeti.map_wildInertiaSubgroup_restrictNormalHom {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] : Subgroup.map (AlgEquiv.restrictNormalHom ↥L) (wildInertiaSubgroup K) = LocalFieldsRamification.lowerRamificationGroup K (↥L) 1

Wild inertia maps onto finite wild inertia. For every compatible local-field structure on a finite Galois subextension L/K, the image of P_K under restriction is G_1(L/K).

theorem TauCeti.exists_mem_wildInertiaSubgroup_restrictNormal_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] {τ : Gal(↥L/K)} (hτ : τ ∈ LocalFieldsRamification.lowerRamificationGroup K (↥L) 1) : ∃ σ ∈ wildInertiaSubgroup K, AlgEquiv.restrictNormal σ ↥L = τ

Every element of finite wild inertia lifts to an element of absolute wild inertia.

theorem TauCeti.le_maximalTameExtension_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (AlgebraicClosure K)) [Module.Finite K ↥L] [IsGalois K ↥L] [ValuativeRel ↥L] [TopologicalSpace ↥L] [IsNonarchimedeanLocalField ↥L] [ValuativeExtension K ↥L] : L ≤ maximalTameExtension K (AlgebraicClosure K) ↔ IsTamelyRamified K ↥L

The tame criterion at finite level. A finite Galois subextension L of K^{alg}/K lies in the maximal tamely ramified extension K^{t} exactly when L/K is tamely ramified.