The tame quotient of the absolute Galois group

Let K be a nonarchimedean local field with residue characteristic p and residue field of order q, let G_K = Gal(K^{alg}/K), and let P_K ≤ I_K ≤ G_K be the wild inertia and inertia subgroups. This file studies the tame quotient

G_K^t = G_K / P_K,

a profinite group. It proves that G_K^t is topologically generated by two elements, and that it sits in a split exact sequence of profinite groups

1 → ℤ̂^{(p')}(1) → G_K^t → ℤ̂ → 1

whose conjugation action is the Iwasawa relation σ τ σ⁻¹ = τ ^ q.

Generation

• The tame character identifies I_K / P_K with the prime-to-p Tate module ℤ̂^{(p')}(1), which is procyclic: a compactness argument on I_K produces τ ∈ I_K whose tame character has a primitive m-th root of unity as its level-m component for every m prime to p, and such a point generates a dense subgroup of the Tate module. Hence τ and P_K topologically generate I_K.
• A Frobenius lift and I_K topologically generate G_K, so σ, τ and P_K do. Thus G_K^t is topologically generated by the images of σ and τ, and its topological generator rank is at most 2.
• The same pair generates every finite quotient G_K / U through which wild inertia dies, and there the image of τ has order prime to p: since P_K is the Sylow pro-p subgroup of I_K, the image of I_K in G_K / U has order prime to p.

The finite form is the input to the count of generators of the absolute Galois group of a p-adic field.

The exact sequence

• the first map TauCeti.tameInertiaHom K is the inverse of the tame character I_K / P_K ≃ₜ* ℤ̂^{(p')}(1) followed by the inclusion I_K / P_K ↪ G_K / P_K, so its image is the tame inertia group I_K / P_K;
• the second map TauCeti.tameQuotientToZHat K is restriction to the maximal unramified extension followed by Gal(K^{ur}/K) ≃ₜ* ℤ̂, whose kernel is therefore the image of I_K;
• the image of an arithmetic Frobenius lift σ generates the quotient ℤ̂, so ℤ̂ → G_K^t, 1 ↦ σ, splits the sequence;
• conjugation by g ∈ G_K acts on ℤ̂^{(p')}(1) through the action of g on the roots of unity, by the equivariance of the tame character; a Frobenius lift raises every root of unity of order prime to p to the q-th power, so conjugation by σ is x ↦ x ^ q.

Main definitions

• TauCeti.tameQuotient K: the tame quotient G_K / P_K, a profinite group.
• TauCeti.toTameQuotient K: the quotient map G_K →ₜ* G_K^t.
• TauCeti.tameInertiaHom K: the inclusion ℤ̂^{(p')}(1) →ₜ* G_K^t of tame inertia.
• TauCeti.tameQuotientToZHat K: the surjection G_K^t →ₜ* ℤ̂.

Main results

• TauCeti.exists_topologicalClosure_zpowers_inertiaTameCharacter_eq_top: some element of inertia has a tame character that topologically generates ℤ̂^{(p')}(1).
• TauCeti.topologicalClosure_zpowers_sup_wildInertiaSubgroup: such an element and wild inertia topologically generate inertia.
• TauCeti.IsArithFrobeniusLift.topologicalClosure_closure_sup_wildInertiaSubgroup, TauCeti.IsArithFrobeniusLift.topologicalClosure_closure_tameQuotient_eq_top: together with a Frobenius lift, it generates G_K modulo wild inertia.
• TauCeti.isTopologicallyFinitelyGenerated_tameQuotient, TauCeti.topologicalGeneratorRankNat_tameQuotient_le_two: the tame quotient is topologically generated by two elements.
• TauCeti.tameInertiaHom_injective, TauCeti.ker_tameQuotientToZHat, TauCeti.tameQuotientToZHat_surjective: the sequence 1 → ℤ̂^{(p')}(1) → G_K^t → ℤ̂ → 1 is exact.
• TauCeti.range_tameInertiaHom: the image of ℤ̂^{(p')}(1) is the image of inertia.
• TauCeti.IsArithFrobeniusLift.tameQuotientToZHat_comp_lift: the continuous homomorphism ℤ̂ → G_K^t sending 1 to the image of a Frobenius lift splits the sequence.
• TauCeti.tameInertiaHom_smul: conjugation in G_K^t acts on ℤ̂^{(p')}(1) through the Galois action on the roots of unity.
• TauCeti.IsArithFrobeniusLift.smul_eq_pow: a Frobenius lift acts on ℤ̂^{(p')}(1) as x ↦ x ^ q.
• TauCeti.IsArithFrobeniusLift.toTameQuotient_mul_tameInertiaHom_mul_inv, TauCeti.IsArithFrobeniusLift.toTameQuotient_mul_toTameQuotient_mul_inv: the Iwasawa relation σ τ σ⁻¹ = τ ^ q in G_K^t, for a Frobenius lift σ and τ in tame inertia.
• TauCeti.not_dvd_orderOf_mk_of_mem_inertiaSubgroup: in a finite quotient of G_K through which wild inertia dies, elements of inertia have order prime to p.
• TauCeti.exists_tameFrame_quotient: a Frobenius lift σ and an element τ of inertia whose images generate every finite quotient of G_K through which wild inertia dies, with the image of τ of order prime to p.

References

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

The tame quotient

@[reducible, inline]

abbrev TauCeti.tameQuotient (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Type u

The tame quotient G_K^t = G_K / P_K of the absolute Galois group of K: the quotient by the wild inertia subgroup, which fixes the maximal tamely ramified extension of K.

Equations

• TauCeti.tameQuotient K = (Field.absoluteGaloisGroup K ⧸ TauCeti.wildInertiaSubgroup K)

instance TauCeti.instT2SpaceTameQuotient (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : T2Space (tameQuotient K)

The tame quotient is Hausdorff, since wild inertia is closed.

instance TauCeti.instTotallyDisconnectedSpaceTameQuotient (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TotallyDisconnectedSpace (tameQuotient K)

The tame quotient is totally disconnected, since wild inertia is closed; with compactness, it is a profinite group.

noncomputable def TauCeti.toTameQuotient (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Field.absoluteGaloisGroup K →ₜ* tameQuotient K

The quotient map G_K →ₜ* G_K^t onto the tame quotient.

Equations

• TauCeti.toTameQuotient K = TauCeti.ContinuousMonoidHom.quotientMk (TauCeti.wildInertiaSubgroup K)

theorem TauCeti.toTameQuotient_apply {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : Field.absoluteGaloisGroup K) : (toTameQuotient K) σ = ↑σ

The quotient map onto the tame quotient sends σ to its class modulo wild inertia.

@[simp]

theorem TauCeti.toTameQuotient_eq_one_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} : (toTameQuotient K) σ = 1 ↔ σ ∈ wildInertiaSubgroup K

An element of G_K has trivial image in the tame quotient exactly when it is wild.

theorem TauCeti.toTameQuotient_surjective (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective ⇑(toTameQuotient K)

The quotient map onto the tame quotient is surjective.

A topological generator of tame inertia

theorem TauCeti.exists_topologicalClosure_zpowers_inertiaTameCharacter_eq_top (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ∃ (τ : ↥(inertiaSubgroup K)), (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤

Tame inertia is procyclic: some element τ of the inertia subgroup has a tame character that topologically generates ℤ̂^{(p')}(1).

theorem TauCeti.topologicalClosure_zpowers_sup_wildInertiaSubgroup {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {τ : ↥(inertiaSubgroup K)} (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : (Subgroup.zpowers ↑τ ⊔ wildInertiaSubgroup K).topologicalClosure = inertiaSubgroup K

A tame inertia generator and wild inertia generate inertia. If the tame character of τ ∈ I_K topologically generates ℤ̂^{(p')}(1), then the closed subgroup generated by τ and P_K is I_K.

theorem TauCeti.IsArithFrobeniusLift.topologicalClosure_closure_sup_wildInertiaSubgroup {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) {τ : ↥(inertiaSubgroup K)} (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : (Subgroup.closure {σ, ↑τ} ⊔ wildInertiaSubgroup K).topologicalClosure = ⊤

The tame frame generates G_K modulo wild inertia. An arithmetic Frobenius lift σ, an element τ ∈ I_K whose tame character topologically generates ℤ̂^{(p')}(1), and the wild inertia subgroup P_K together topologically generate the absolute Galois group.

theorem TauCeti.IsArithFrobeniusLift.topologicalClosure_closure_tameQuotient_eq_top {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) {τ : ↥(inertiaSubgroup K)} (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : (Subgroup.closure {↑σ, ↑↑τ}).topologicalClosure = ⊤

The tame frame generates the tame quotient. The images in G_K / P_K of an arithmetic Frobenius lift σ and of an element τ ∈ I_K whose tame character topologically generates ℤ̂^{(p')}(1) topologically generate the tame quotient.

Generation of the tame quotient

theorem TauCeti.isTopologicallyFinitelyGenerated_tameQuotient (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsTopologicallyFinitelyGenerated (tameQuotient K)

The tame quotient is topologically finitely generated, by the images of a Frobenius lift and of a tame inertia generator.

theorem TauCeti.topologicalGeneratorRankNat_tameQuotient_le_two (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : topologicalGeneratorRankNat (tameQuotient K) ⋯ ≤ 2

The tame quotient is topologically generated by two elements.

Tame inertia inside the tame quotient

noncomputable def TauCeti.tameInertiaHom (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : PrimeToPTateModule (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (AlgebraicClosure K) →ₜ* tameQuotient K

The inclusion of tame inertia ℤ̂^{(p')}(1) →ₜ* G_K^t: the inverse of the isomorphism I_K / P_K ≃ₜ* ℤ̂^{(p')}(1) given by the tame character, followed by the map I_K / P_K → G_K / P_K induced by the inclusion of inertia.

Equations

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

@[simp]

theorem TauCeti.tameInertiaHom_inertiaTameCharacter {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (τ : ↥(inertiaSubgroup K)) : (tameInertiaHom K) ((inertiaTameCharacter K) τ) = (toTameQuotient K) ↑τ

The inclusion of tame inertia sends the tame character of τ ∈ I_K to the image of τ in the tame quotient.

theorem TauCeti.tameInertiaHom_injective (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Injective ⇑(tameInertiaHom K)

The inclusion of tame inertia is injective: an element of I_K whose image in G_K / P_K is trivial lies in P_K, so its tame character is trivial.

theorem TauCeti.range_tameInertiaHom (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (tameInertiaHom K).range = Subgroup.map (toTameQuotient K).toMonoidHom (inertiaSubgroup K)

The image of the inclusion of tame inertia is the image I_K / P_K of the inertia subgroup in the tame quotient.

The unramified quotient ℤ̂

noncomputable def TauCeti.tameQuotientToZHat (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : tameQuotient K →ₜ* ↑zHat.toProfinite.toTop

The surjection G_K^t →ₜ* ℤ̂: restriction to the maximal unramified extension, followed by the identification Gal(K^{ur}/K) ≃ₜ* ℤ̂ carrying arithmetic Frobenius to 1. It is well defined on the tame quotient because wild inertia fixes K^{ur}.

Equations

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

@[simp]

theorem TauCeti.tameQuotientToZHat_toTameQuotient {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : Field.absoluteGaloisGroup K) : (tameQuotientToZHat K) ((toTameQuotient K) σ) = (maximalUnramifiedGaloisGroupEquivZHat K (AlgebraicClosure K)) ((restrictMaximalUnramifiedHom K) σ)

The image in ℤ̂ of the class of σ is the image of the restriction of σ to K^{ur}.

theorem TauCeti.ker_tameQuotientToZHat (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (tameQuotientToZHat K).ker = (tameInertiaHom K).range

Exactness in the middle: the kernel of G_K^t → ℤ̂ is the image of ℤ̂^{(p')}(1), since both are the image of the inertia subgroup.

@[simp]

theorem TauCeti.tameQuotientToZHat_tameInertiaHom {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : PrimeToPTateModule (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (AlgebraicClosure K)) : (tameQuotientToZHat K) ((tameInertiaHom K) x) = 1

The map G_K^t → ℤ̂ kills tame inertia: the elementwise form of ker_tameQuotientToZHat.

The conjugation action

theorem TauCeti.tameInertiaHom_smul {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (g : Gal(AlgebraicClosure K/K)) (x : PrimeToPTateModule (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (AlgebraicClosure K)) : (tameInertiaHom K) (g • x) = (toTameQuotient K) g * (tameInertiaHom K) x * ((toTameQuotient K) g)⁻¹

Conjugation acts on tame inertia through the roots of unity: conjugating the image of x ∈ ℤ̂^{(p')}(1) by the image of g ∈ G_K gives the image of g • x. This is the equivariance of the tame character, TauCeti.inertiaTameCharacter_conj.

theorem TauCeti.IsArithFrobeniusLift.smul_eq_pow {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Gal(AlgebraicClosure K/K)} (hσ : IsArithFrobeniusLift K σ) (x : PrimeToPTateModule (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (AlgebraicClosure K)) : σ • x = x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

A Frobenius lift acts on ℤ̂^{(p')}(1) as x ↦ x ^ q, since it raises every root of unity of order prime to p to the q-th power (TauCeti.IsArithFrobeniusLift.apply_of_pow_eq_one).

theorem TauCeti.IsArithFrobeniusLift.toTameQuotient_mul_tameInertiaHom_mul_inv {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) (x : PrimeToPTateModule (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (AlgebraicClosure K)) : (toTameQuotient K) σ * (tameInertiaHom K) x * ((toTameQuotient K) σ)⁻¹ = (tameInertiaHom K) x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The Iwasawa relation on tame inertia: conjugation by the image of an arithmetic Frobenius lift σ raises the image of every x ∈ ℤ̂^{(p')}(1) in the tame quotient to the q-th power.

theorem TauCeti.IsArithFrobeniusLift.toTameQuotient_mul_toTameQuotient_mul_inv {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) {τ : Field.absoluteGaloisGroup K} (hτ : τ ∈ inertiaSubgroup K) : (toTameQuotient K) σ * (toTameQuotient K) τ * ((toTameQuotient K) σ)⁻¹ = (toTameQuotient K) τ ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The Iwasawa relation σ τ σ⁻¹ = τ ^ q in the tame quotient, for an arithmetic Frobenius lift σ and an element τ of the inertia subgroup.

theorem TauCeti.IsArithFrobeniusLift.tameQuotientToZHat_eq_gen {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) : (tameQuotientToZHat K) ((toTameQuotient K) σ) = zHat.gen

The image of an arithmetic Frobenius lift in ℤ̂ is the canonical generator.

theorem TauCeti.IsArithFrobeniusLift.tameQuotientToZHat_comp_lift {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) : (tameQuotientToZHat K).comp (zHat.lift ((toTameQuotient K) σ)) = ContinuousMonoidHom.id ↑zHat.toProfinite.toTop

The splitting by a Frobenius lift: the continuous homomorphism ℤ̂ → G_K^t sending 1 to the image of an arithmetic Frobenius lift is a section of G_K^t → ℤ̂.

theorem TauCeti.IsArithFrobeniusLift.tameQuotientToZHat_lift {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) (x : ↑zHat.toProfinite.toTop) : (tameQuotientToZHat K) ((zHat.lift ((toTameQuotient K) σ)) x) = x

The splitting by a Frobenius lift, pointwise: G_K^t → ℤ̂ sends the image of x ∈ ℤ̂ under the section ℤ̂ → G_K^t determined by an arithmetic Frobenius lift back to x.

theorem TauCeti.tameQuotientToZHat_surjective (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective ⇑(tameQuotientToZHat K)

The map G_K^t → ℤ̂ is surjective, being split by any Frobenius lift.

The tame frame on finite quotients

theorem TauCeti.not_dvd_orderOf_mk_of_mem_inertiaSubgroup {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (hU : wildInertiaSubgroup K ≤ ↑U.toOpenSubgroup) {τ : Field.absoluteGaloisGroup K} (hτ : τ ∈ inertiaSubgroup K) : ¬p ∣ orderOf ↑τ

Inertia has order prime to p on a finite tame layer. In a finite quotient G_K / U through which wild inertia dies, the image of every element of inertia has order prime to the residue characteristic p.

theorem TauCeti.exists_tameFrame_quotient (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] : ∃ (σ : Field.absoluteGaloisGroup K) (τ : Field.absoluteGaloisGroup K), IsArithFrobeniusLift K σ ∧ τ ∈ inertiaSubgroup K ∧ ∀ (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)), wildInertiaSubgroup K ≤ ↑U.toOpenSubgroup → Subgroup.closure {↑σ, ↑τ} = ⊤ ∧ ¬p ∣ orderOf ↑τ

The tame frame on the finite tame layers. There are an arithmetic Frobenius lift σ and an element τ of inertia such that for every open normal subgroup U of G_K containing wild inertia, the images of σ and τ generate the finite group G_K / U and the image of τ has order prime to the residue characteristic p.