Inertia and Frobenius along a finite extension of local fields

Let L/K be a finite extension of nonarchimedean local fields with residue degree f = f(L/K), embedded in a separable closure of K by ι, and let absoluteGaloisGroupExtend K L ι : G_L →* G_K be the resulting embedding of absolute Galois groups. If q is the cardinality of the residue field of K, that of L is q^f, so the generators of the maximal unramified extensions, the roots of the polynomials X^{q^g} − X and X^{q^{fg}} − X, correspond under the identification of separable closures. Consequently an element τ ∈ G_L acts on L^{ur} as the n-th power of the arithmetic Frobenius of L exactly when its image acts on K^{ur} as the f n-th power of the arithmetic Frobenius of K. In particular:

• the inertia subgroup of L is the preimage of that of K;
• an arithmetic Frobenius lift of L acts on K^{ur} as the f-th power of Frobenius;
• if the image of τ acts on K^{ur} as an integral power m of Frobenius, then f ∣ m: the element fixes L, and hence its Teichmüller representatives, whose residues generate the degree-f extension of the residue field of K.

These are the inputs of the functoriality of the local Weil group under finite extensions.

They also determine how inertia sits along the extension. Since Frobenius generates Gal(K^{ur}/K) topologically, the image of G_L there is the open subgroup of index f, so G_L · I_K has index f in G_K. As G_L has index [L : K] = e f in G_K, the image I_L = G_L ∩ I_K of the inertia subgroup of L has index e = e(L/K) in that of K.

The description of inertia through the roots of X^{q^g} − X needs no chosen embedding: under any ring isomorphism L^{alg} ≃ K^{alg}, elements of G_L and G_K that correspond lie in the inertia subgroups together. This identifies the inertia subgroup of a finite extension M of K inside K^{alg} with the elements of I_K fixing M, once K^{alg} is read as an algebraic closure of M.

Main results

• RingEquiv.mem_inertiaSubgroup_iff_of_semiconj: if φ ∘ τ = σ ∘ φ for a ring isomorphism φ : L^{alg} ≃ K^{alg}, then σ ∈ I_K exactly when τ ∈ I_L.
• TauCeti.restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend_eq_zpow_iff: the image of τ ∈ G_L acts on K^{ur} as Frob_K ^ (f n) exactly when τ acts on L^{ur} as Frob_L ^ n, for every integer n.
• TauCeti.absoluteGaloisGroupExtend_mem_inertiaSubgroup_iff: I_L is the preimage of I_K.
• TauCeti.IsArithFrobeniusLift.restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend: an arithmetic Frobenius lift of L acts on K^{ur} as Frob_K ^ f.
• TauCeti.inertiaDegree_dvd_of_restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend_eq_zpow: an element of G_L acting on K^{ur} as Frob_K ^ m has f ∣ m.
• TauCeti.comap_absoluteGaloisGroupExtend_inertiaSubgroup, TauCeti.map_absoluteGaloisGroupExtend_inertiaSubgroup: I_L is the preimage of I_K, and its image is I_K ∩ G_L.
• TauCeti.index_map_restrictMaximalUnramifiedHom_range_absoluteGaloisGroupExtend, TauCeti.index_range_absoluteGaloisGroupExtend_sup_inertiaSubgroup: the image of G_L in Gal(K^{ur}/K) has index f, and so does G_L · I_K in G_K.
• TauCeti.relIndex_map_absoluteGaloisGroupExtend_inertiaSubgroup: the image of I_L has index e(L/K) in I_K.

References

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

theorem RingEquiv.mem_inertiaSubgroup_iff_of_semiconj {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] (φ : AlgebraicClosure L ≃+* AlgebraicClosure K) {τ : Gal(AlgebraicClosure L/L)} {σ : Gal(AlgebraicClosure K/K)} (h : Function.Semiconj ⇑φ ⇑τ ⇑σ) : σ ∈ TauCeti.inertiaSubgroup K ↔ τ ∈ TauCeti.inertiaSubgroup L

Inertia along an identification of algebraic closures. Let L/K be an extension of nonarchimedean local fields and φ : L^{alg} ≃ K^{alg} a ring isomorphism, and let τ ∈ G_L and σ ∈ G_K correspond under φ, that is φ ∘ τ = σ ∘ φ. Then σ lies in the inertia subgroup of K exactly when τ lies in that of L. No compatibility of φ with L or K is needed: both inertia subgroups are cut out by the roots of the polynomials X^{q^g} − X, which every ring isomorphism preserves.

theorem TauCeti.restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend_eq_pow_iff {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) (τ : Field.absoluteGaloisGroup L) (n : ℕ) : (restrictMaximalUnramifiedHom K) ((absoluteGaloisGroupExtend K L ι) τ) = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ (inertiaDegree K L * n) ↔ (restrictMaximalUnramifiedHom L) τ = maximalUnramifiedFrobenius L (AlgebraicClosure L) ^ n

Frobenius along a finite extension. For n : ℕ, the image of τ ∈ G_L in G_K acts on K^{ur} as the f n-th power of the arithmetic Frobenius of K, where f = f(L/K), exactly when τ acts on L^{ur} as the n-th power of the arithmetic Frobenius of L.

theorem TauCeti.restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend_eq_zpow_iff {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) (τ : Field.absoluteGaloisGroup L) (n : ℤ) : (restrictMaximalUnramifiedHom K) ((absoluteGaloisGroupExtend K L ι) τ) = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ (↑(inertiaDegree K L) * n) ↔ (restrictMaximalUnramifiedHom L) τ = maximalUnramifiedFrobenius L (AlgebraicClosure L) ^ n

Frobenius along a finite extension, integral powers. For n : ℤ, the image of τ ∈ G_L in G_K acts on K^{ur} as the f n-th power of the arithmetic Frobenius of K, where f = f(L/K), exactly when τ acts on L^{ur} as the n-th power of the arithmetic Frobenius of L.

theorem TauCeti.absoluteGaloisGroupExtend_mem_inertiaSubgroup_iff {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) {τ : Field.absoluteGaloisGroup L} : (absoluteGaloisGroupExtend K L ι) τ ∈ inertiaSubgroup K ↔ τ ∈ inertiaSubgroup L

Inertia along a finite extension. An element of G_L lies in the inertia subgroup of L exactly when its image in G_K lies in the inertia subgroup of K: I_L is the preimage of I_K.

theorem TauCeti.IsArithFrobeniusLift.restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) {τ : Field.absoluteGaloisGroup L} (hτ : IsArithFrobeniusLift L τ) : (restrictMaximalUnramifiedHom K) ((absoluteGaloisGroupExtend K L ι) τ) = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ inertiaDegree K L

Frobenius lifts along a finite extension. An arithmetic Frobenius lift of L acts on K^{ur} as the f-th power of the arithmetic Frobenius of K, where f = f(L/K).

theorem TauCeti.inertiaDegree_dvd_of_restrictMaximalUnramifiedHom_absoluteGaloisGroupExtend_eq_zpow {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) {τ : Field.absoluteGaloisGroup L} {m : ℤ} (h : (restrictMaximalUnramifiedHom K) ((absoluteGaloisGroupExtend K L ι) τ) = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ m) : ↑(inertiaDegree K L) ∣ m

Divisibility by the residue degree. If the image of τ ∈ G_L in G_K acts on K^{ur} as the m-th power of the arithmetic Frobenius of K, then the residue degree f(L/K) divides m: the q^m-th power map fixes the residue field of L, of degree f(L/K) over that of K.

Inertia and its index along a finite extension

@[simp]

theorem TauCeti.comap_absoluteGaloisGroupExtend_inertiaSubgroup {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) : Subgroup.comap (absoluteGaloisGroupExtend K L ι) (inertiaSubgroup K) = inertiaSubgroup L

Inertia along a finite extension, as a preimage. The inertia subgroup of L is the preimage of that of K under the embedding G_L → G_K.

@[simp]

theorem TauCeti.map_absoluteGaloisGroupExtend_inertiaSubgroup {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) : Subgroup.map (absoluteGaloisGroupExtend K L ι) (inertiaSubgroup L) = inertiaSubgroup K ⊓ (absoluteGaloisGroupExtend K L ι).range

Inertia along a finite extension, as an image. The image of the inertia subgroup of L in G_K is the part of the inertia subgroup of K lying in the image of G_L.

theorem TauCeti.index_map_restrictMaximalUnramifiedHom_range_absoluteGaloisGroupExtend {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) : (Subgroup.map (restrictMaximalUnramifiedHom K) (absoluteGaloisGroupExtend K L ι).range).index = inertiaDegree K L

The image of G_L in Gal(K^{ur}/K) has index f(L/K): the elements of G_L act on K^{ur} through an open subgroup of index the residue degree.

theorem TauCeti.index_range_absoluteGaloisGroupExtend_sup_inertiaSubgroup {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) : ((absoluteGaloisGroupExtend K L ι).range ⊔ inertiaSubgroup K).index = inertiaDegree K L

G_L · I_K has index f(L/K) in G_K.

theorem TauCeti.relIndex_map_absoluteGaloisGroupExtend_inertiaSubgroup {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] [FiniteDimensional K L] (ι : L →ₐ[K] SeparableClosure K) : (Subgroup.map (absoluteGaloisGroupExtend K L ι) (inertiaSubgroup L)).relIndex (inertiaSubgroup K) = ramificationIndex K L

The inertia subgroup of L has index e(L/K) in that of K: the image of I_L in G_K is a subgroup of I_K of index the ramification index of L/K.