Generators of finite quotients of a local absolute Galois group

Let K be a finite extension of ℚ_p and N = [K : ℚ_p]. Every finite quotient G_K ⧸ U of the absolute Galois group through which the commutator ⁅P_K, P_K⁆ of wild inertia dies is generated by an (N + 2)-tuple. This is the finite level of the generator theorem for G_K, from which topological generation of G_K itself follows by compactness.

The proof is that of NSW (7.4.1). Let L be the tame layer of U, the fixed field of P_K U. Its Galois group is generated by a tame frame σ, τ (TauCeti.exists_tameFrame_tameLayer), so padding the frame to an (N + 2)-tuple g, the relation module of g surjects onto the completed multiplicative group A(L) with kernel free of rank one (TauCeti.exists_relationModule_surjective_of_tameFrame). Read through Lyndon's isomorphism and local reciprocity, this is a continuous equivariant surjection of pro-p relation groups which is bijective on second cohomology, because its kernel is projective (TauCeti.bijective_explicitCoeff2_relationModuleToAbelianizationProPEquivariant). The extension dictionary then lifts g to generators of G_K ⧸ U (TauCeti.exists_generating_tuple_quotient_of_galoisClassModuleMap).

Main results

• TauCeti.exists_generating_tuple_quotient: every finite quotient of G_K killing ⁅P_K, P_K⁆ is generated by [K : ℚ_p] + 2 elements, given as a tuple.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).
• Tau Ceti lookahead branch lookahead/LocalGaloisGroups/exists-generating-tuple-quotient, split 5: source of the final proof structure and of the helper lemmas Subgroup.exists_closure_range_eq_top_of_closure_pair_eq_top and TauCeti.charP_residueField.

theorem TauCeti.exists_generating_tuple_quotient (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K)) (hU : ⁅wildInertiaSubgroup K, wildInertiaSubgroup K⁆ ≤ ↑U.toOpenSubgroup) : ∃ (x : Fin (Module.finrank ℚ_[p] K + 2) → Field.absoluteGaloisGroup K ⧸ ↑U.toOpenSubgroup), Subgroup.closure (Set.range x) = ⊤

The finite level of the generator theorem (NSW, proof of (7.4.1)). For a finite extension K of ℚ_p, every finite quotient of G_K through which the commutator subgroup of wild inertia dies is generated by [K : ℚ_p] + 2 elements. The generators form a tuple, in which repetitions are allowed: the quotient may have fewer than [K : ℚ_p] + 2 elements.