Finite local Galois generators from the tame layer's class module

Let K be a perfect nonarchimedean local field whose residue prime p is invertible in K. Let U be an open normal subgroup of G_K containing the commutator of wild inertia, and let L be the fixed field of P_K U. A generating tuple of Gal(L/K) lifts to a generating tuple of G_K/U whenever its pro-p relation group maps continuously and equivariantly onto the arithmetic class module, inducing a bijection on explicit continuous second cohomology.

The arithmetic coefficients use the separable closure and the canonical embedding of the tame layer. The conclusion uses the algebraic-closure model of G_K, retaining the prescribed generators under the canonical quotient identification. Thus an arithmetic relation-module calculation can be used directly without changing coefficient actions or transporting its second-cohomology hypothesis to a different quotient model.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).

theorem TauCeti.exists_generating_tuple_quotient_of_galoisClassModuleMap {p : ℕ} [Fact (Nat.Prime p)] (K : Type) [Field K] [PerfectField K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (hp : IsUnit ↑p) (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (hU : ⁅wildInertiaSubgroup K, wildInertiaSubgroup K⁆ ≤ ↑U.toOpenSubgroup) {n : ℕ} (g : Fin n → Gal(↥(tameLayer K U)/K)) (hg : Subgroup.closure (Set.range g) = ⊤) : have j := tameLayerEmbedding K U; ∀ (f : abelianizationProP p (↑(freeProfiniteGroup (Fin n)).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker →*[Gal(↥(tameLayer K U)/K)] abelianizationProP p (AbsoluteGaloisGroup K) ↑(galoisSubgroup K (↥(tameLayer K U)) j)) (hf : Continuous ⇑f), Function.Surjective ⇑f → Function.Bijective ⇑(ContCohomology.explicitCoeff2 Gal(↥(tameLayer K U)/K) (Additive (abelianizationProP p (↑(freeProfiniteGroup (Fin n)).toProfinite.toTop) (↑(freeProfiniteGroup.lift g)).ker)) f.toAdditive ⋯) → ∃ (t : Fin n → Field.absoluteGaloisGroup K ⧸ ↑U.toOpenSubgroup), Subgroup.closure (Set.range t) = ⊤ ∧ ∀ (i : Fin n), (quotientTameLayerEquiv K U) ((QuotientGroup.mapOfLE ⋯) (t i)) = g i

A cohomologically bijective surjection onto the arithmetic class module of the tame layer lifts its Galois generators to generators of the original finite quotient. The tuple's images in the tame quotient are retained through quotientTameLayerEquiv.