The inertia subgroup of the Galois group of the separable closure

Let K be a nonarchimedean local field. Its inertia subgroup TauCeti.inertiaSubgroup K is a subgroup of Gal(K^{alg}/K), the automorphisms of the algebraic closure fixing the maximal unramified extension K^{ur} inside it. Galois cohomology is stated at the Galois group TauCeti.AbsoluteGaloisGroup K = Gal(Kˢ/K) of the separable closure instead, and the two groups are compared by restriction, TauCeti.absoluteGaloisGroupRestrictEquiv K.

This file identifies the image of inertia under that comparison: it is the subgroup of Gal(Kˢ/K) fixing the maximal unramified extension of K inside Kˢ. Both subgroups are cut out by the roots of the polynomials X^{q^f} − X, and these roots are separable over K, so they lie in Kˢ. By infinite Galois theory, a finite subextension E of Kˢ/K is therefore unramified exactly when inertia fixes it. This is the form in which unramifiedness of a field cut out by a Galois module over Kˢ, such as the field of m-torsion points of an elliptic curve, is read off the action of inertia on that module.

For an extension L/K of nonarchimedean local fields, a K-embedding τ : Kˢ → Lˢ of separable closures induces TauCeti.absoluteGaloisGroupMap τ : Gal(Lˢ/L) → Gal(Kˢ/K), and this map sends inertia into inertia: τ carries K^{ur} into L^{ur}, so an automorphism of Lˢ fixing L^{ur} induces one of Kˢ fixing K^{ur}. This is what makes a Galois cohomology class of K vanishing on inertia restrict to a class of L vanishing on inertia.

Main results

• TauCeti.map_inertiaSubgroup_absoluteGaloisGroupRestrictEquiv: the image of I_K in Gal(Kˢ/K) is the fixing subgroup of the maximal unramified extension of K inside Kˢ.
• TauCeti.map_inertiaSubgroup_le_fixingSubgroup_iff: a finite subextension of Kˢ/K is unramified exactly when the image of I_K fixes it.
• AlgHom.map_absoluteGaloisGroupMap_inertiaSubgroup_le: for an extension L/K of local fields, the map Gal(Lˢ/L) → Gal(Kˢ/K) along an embedding of separable closures sends the inertia subgroup of L into that of K.

References

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

theorem TauCeti.map_inertiaSubgroup_absoluteGaloisGroupRestrictEquiv (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Subgroup.map (absoluteGaloisGroupRestrictEquiv K).toMonoidHom (inertiaSubgroup K) = (maximalUnramifiedExtension K (SeparableClosure K)).fixingSubgroup

Inertia in the Galois group of the separable closure. The image of the inertia subgroup I_K ≤ Gal(K^{alg}/K) under restriction to the separable closure is the subgroup of Gal(Kˢ/K) fixing the maximal unramified extension of K inside Kˢ.

theorem TauCeti.map_inertiaSubgroup_le_fixingSubgroup_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (E : IntermediateField K (SeparableClosure K)) [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] : Subgroup.map (absoluteGaloisGroupRestrictEquiv K).toMonoidHom (inertiaSubgroup K) ≤ E.fixingSubgroup ↔ IsUnramified K ↥E

Unramified subextensions of the separable closure are those fixed by inertia. A subextension E of Kˢ/K, with a structure of nonarchimedean local field compatible with K, is unramified over K exactly when the image of the inertia subgroup in Gal(Kˢ/K) fixes it.

theorem AlgHom.map_absoluteGaloisGroupMap_inertiaSubgroup_le {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type u_2} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (τ : SeparableClosure K →ₐ[K] SeparableClosure L) : Subgroup.map (↑(TauCeti.absoluteGaloisGroupMap τ)) (Subgroup.map (TauCeti.absoluteGaloisGroupRestrictEquiv L).toMonoidHom (TauCeti.inertiaSubgroup L)) ≤ Subgroup.map (TauCeti.absoluteGaloisGroupRestrictEquiv K).toMonoidHom (TauCeti.inertiaSubgroup K)

Inertia along an extension of local fields. For an extension L/K of nonarchimedean local fields and a K-embedding τ : Kˢ → Lˢ of separable closures, the induced map Gal(Lˢ/L) → Gal(Kˢ/K) sends the inertia subgroup of L into that of K.