The Iwasawa presentation of the tame quotient

Let K be a nonarchimedean local field with residue characteristic p and residue field of order q, and let G_K^t = G_K / P_K be its tame quotient. This file proves Iwasawa's theorem that G_K^t is the profinite group

⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩

with σ an arithmetic Frobenius lift and τ a topological generator of tame inertia, and that the isomorphism is determined by these two values.

The presented group IwasawaGroup K is the quotient of the free profinite group on two generators by the closed normal closure of the relator σ τ σ⁻¹ τ⁻ᵠ. Its coordinate iwasawaCoordinate K : IwasawaGroup K →ₜ* ℤ̂ sends σ to the canonical generator and kills τ, and its kernel is the closed normal closure ⟨⟨τ⟩⟩ of τ. In every finite quotient of the presented group, conjugation by σ raises the image of τ to the q-th power, so the order of that image is prime to q and σ normalizes the cyclic group it generates. Passing to the limit, ⟨⟨τ⟩⟩ is the closed procyclic subgroup generated by τ.

Given a Frobenius lift σ and an element τ of inertia whose tame character generates ℤ̂^{(p')}(1), the Iwasawa relation in G_K^t gives a continuous surjection IwasawaGroup K → G_K^t. It is compatible with the coordinates to ℤ̂, so its kernel lies in ⟨⟨τ⟩⟩ and consists of profinite powers τ ^ a. If such a power dies in G_K^t, the tame character shows that a vanishes modulo every integer prime to p, and since the image of τ in each finite quotient has order prime to q, the power τ ^ a is already trivial. Hence the surjection is an isomorphism.

Main definitions

• TauCeti.iwasawaRelator K: the relator σ τ σ⁻¹ τ⁻ᵠ in the free profinite group on two generators.
• TauCeti.IwasawaGroup K: the profinite group ⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩, with its marked generators TauCeti.iwasawaSigma K and TauCeti.iwasawaTau K.
• TauCeti.iwasawaCoordinate K: the continuous homomorphism IwasawaGroup K →ₜ* ℤ̂ with σ ↦ zHat.gen and τ ↦ 1.
• TauCeti.tameQuotientEquiv hσ τ hτ: for a Frobenius lift σ and a tame inertia generator τ, the topological isomorphism G_K^t ≃ₜ* IwasawaGroup K sending the classes of σ and τ to the marked generators.

Main results

• TauCeti.iwasawaSigma_mul_iwasawaTau_mul_inv: the relation σ τ σ⁻¹ = τ ^ q.
• TauCeti.IwasawaGroup.hom_ext, TauCeti.IwasawaGroup.topologicalClosure_closure_eq_top: the marked generators determine continuous homomorphisms and generate topologically.
• TauCeti.ker_iwasawaCoordinate: the kernel of the coordinate is ⟨⟨τ⟩⟩.
• TauCeti.topologicalClosure_normalClosure_iwasawaTau: ⟨⟨τ⟩⟩ is the closed procyclic subgroup generated by τ.
• TauCeti.tameQuotientEquiv_toTameQuotient_frobenius, TauCeti.tameQuotientEquiv_toTameQuotient_tameGenerator: the marking, which determines the isomorphism (TauCeti.eq_tameQuotientEquiv).
• TauCeti.iwasawaCoordinate_tameQuotientEquiv: the coordinate of the presented group is the unramified coordinate G_K^t → ℤ̂.
• TauCeti.map_tameQuotientEquiv_tameInertia, TauCeti.IsArithFrobeniusLift.inv_iwasawaSigma_mul_tameQuotientEquiv_mem: whatever the marking, tame inertia goes to ⟨⟨τ⟩⟩ and every Frobenius lift to the coset σ ⟨⟨τ⟩⟩.
• TauCeti.nonempty_continuousMulEquiv_iwasawaGroup: G_K^t ≅ ⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (7.5.3).
• K. Iwasawa, On Galois groups of local fields, Trans. Amer. Math. Soc. 80 (1955).

The presented group

noncomputable def TauCeti.iwasawaRelator (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ↑(freeProfiniteGroup (ULift.{u, 0} (Fin 2))).toProfinite.toTop

The Iwasawa relator σ τ σ⁻¹ τ⁻ᵠ in the free profinite group on the two generators σ = of 0 and τ = of 1, where q is the order of the residue field of K. The generators are indexed by ULift (Fin 2) so that the presented group lives in the universe of K.

@[reducible, inline]

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

The Iwasawa group ⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩, with q the order of the residue field of K: the profinite group presented by iwasawaRelator K.

@[reducible, inline]

noncomputable abbrev TauCeti.iwasawaSigma (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IwasawaGroup K

The marked generator σ of the Iwasawa group, the image of an arithmetic Frobenius.

@[reducible, inline]

noncomputable abbrev TauCeti.iwasawaTau (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IwasawaGroup K

The marked generator τ of the Iwasawa group, the image of a tame inertia generator.

theorem TauCeti.iwasawaSigma_mul_iwasawaTau_mul_inv (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : iwasawaSigma K * iwasawaTau K * (iwasawaSigma K)⁻¹ = iwasawaTau K ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The Iwasawa relation σ τ σ⁻¹ = τ ^ q in the Iwasawa group.

theorem TauCeti.IwasawaGroup.hom_ext {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {G : Type u_1} [Group G] [TopologicalSpace G] [T2Space G] {φ ψ : IwasawaGroup K →ₜ* G} (hσ : φ (iwasawaSigma K) = ψ (iwasawaSigma K)) (hτ : φ (iwasawaTau K) = ψ (iwasawaTau K)) : φ = ψ

Two continuous homomorphisms out of the Iwasawa group into a Hausdorff group agree as soon as they agree on the marked generators σ and τ.

theorem TauCeti.IwasawaGroup.topologicalClosure_closure_eq_top (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (Subgroup.closure {iwasawaSigma K, iwasawaTau K}).topologicalClosure = ⊤

The marked generators σ and τ topologically generate the Iwasawa group.

The coordinate to ℤ̂

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

The coordinate IwasawaGroup K →ₜ* ℤ̂ of the Iwasawa group, sending σ to the canonical generator zHat.gen and τ to 1. It is well defined since gen * 1 * gen⁻¹ * (1 ^ q)⁻¹ = 1.

@[simp]

theorem TauCeti.iwasawaCoordinate_iwasawaSigma (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (iwasawaCoordinate K) (iwasawaSigma K) = zHat.gen

The coordinate sends σ to the canonical generator of ℤ̂.

@[simp]

theorem TauCeti.iwasawaCoordinate_iwasawaTau (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (iwasawaCoordinate K) (iwasawaTau K) = 1

The coordinate kills τ.

theorem TauCeti.ker_iwasawaCoordinate (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (iwasawaCoordinate K).ker = (Subgroup.normalClosure {iwasawaTau K}).topologicalClosure

The kernel of the coordinate is the closed normal closure ⟨⟨τ⟩⟩ of τ, so the coordinate identifies IwasawaGroup K ⧸ ⟨⟨τ⟩⟩ with ℤ̂.

⟨⟨τ⟩⟩ is procyclic

theorem TauCeti.topologicalClosure_normalClosure_iwasawaTau (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (Subgroup.normalClosure {iwasawaTau K}).topologicalClosure = closedZpowers (iwasawaTau K)

⟨⟨τ⟩⟩ is procyclic: the closed normal closure of τ in the Iwasawa group is the closed subgroup generated by τ.

The marked isomorphism

noncomputable def TauCeti.tameQuotientEquiv {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 = ⊤) : tameQuotient K ≃ₜ* IwasawaGroup K

The Iwasawa presentation of the tame quotient (Iwasawa). For an arithmetic Frobenius lift σ and an element τ of inertia whose tame character topologically generates ℤ̂^{(p')}(1), the topological isomorphism G_K^t ≃ₜ* ⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩ sending the classes of σ and τ to the marked generators.

@[simp]

theorem TauCeti.tameQuotientEquiv_symm_iwasawaSigma {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : (tameQuotientEquiv hσ τ hτ).symm (iwasawaSigma K) = (toTameQuotient K) σ

The inverse of the marked isomorphism sends σ to the class of the Frobenius lift.

@[simp]

theorem TauCeti.tameQuotientEquiv_symm_iwasawaTau {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : (tameQuotientEquiv hσ τ hτ).symm (iwasawaTau K) = (toTameQuotient K) ↑τ

The inverse of the marked isomorphism sends τ to the class of the tame inertia generator.

@[simp]

theorem TauCeti.tameQuotientEquiv_toTameQuotient_frobenius {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : (tameQuotientEquiv hσ τ hτ) ((toTameQuotient K) σ) = iwasawaSigma K

The marked isomorphism sends the class of the Frobenius lift σ to the generator σ.

@[simp]

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

The marked isomorphism sends the class of the tame inertia generator τ to the generator τ.

theorem TauCeti.eq_tameQuotientEquiv {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) (e : tameQuotient K ≃ₜ* IwasawaGroup K) (he₀ : e ((toTameQuotient K) σ) = iwasawaSigma K) (he₁ : e ((toTameQuotient K) ↑τ) = iwasawaTau K) : e = tameQuotientEquiv hσ τ hτ

The marking determines the isomorphism: a topological isomorphism G_K^t ≃ₜ* IwasawaGroup K sending the classes of σ and τ to the marked generators is tameQuotientEquiv.

@[simp]

theorem TauCeti.iwasawaCoordinate_tameQuotientEquiv {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) (x : tameQuotient K) : (iwasawaCoordinate K) ((tameQuotientEquiv hσ τ hτ) x) = (tameQuotientToZHat K) x

The coordinate is the unramified coordinate: through the marked isomorphism, the coordinate IwasawaGroup K → ℤ̂ is the surjection G_K^t → ℤ̂, that is, restriction to K^{ur} followed by Gal(K^{ur}/K) ≃ ℤ̂.

theorem TauCeti.map_tameQuotientEquiv_tameInertia {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) : Subgroup.map (↑↑(tameQuotientEquiv hσ τ hτ)) (tameInertia K) = (Subgroup.normalClosure {iwasawaTau K}).topologicalClosure

The image of tame inertia under the marked isomorphism is the closed normal closure ⟨⟨τ⟩⟩ of the marked generator τ, whatever the choice of σ and τ.

theorem TauCeti.IsArithFrobeniusLift.inv_iwasawaSigma_mul_tameQuotientEquiv_mem {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} {τ : ↥(inertiaSubgroup K)} (hσ : IsArithFrobeniusLift K σ) (hτ : (Subgroup.zpowers ((inertiaTameCharacter K) τ)).topologicalClosure = ⊤) {φ : Field.absoluteGaloisGroup K} (hφ : IsArithFrobeniusLift K φ) : (iwasawaSigma K)⁻¹ * (tameQuotientEquiv hσ τ hτ) ((toTameQuotient K) φ) ∈ (Subgroup.normalClosure {iwasawaTau K}).topologicalClosure

Frobenius lifts land in σ ⟨⟨τ⟩⟩: whatever the choice of σ and τ, the marked isomorphism sends the class of every arithmetic Frobenius lift φ into the coset of the marked generator σ modulo the closed normal closure of τ.

theorem TauCeti.nonempty_continuousMulEquiv_iwasawaGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Nonempty (tameQuotient K ≃ₜ* IwasawaGroup K)

Iwasawa's theorem: the tame quotient of the absolute Galois group of K is isomorphic, as a topological group, to the profinite group ⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩.