Finite local Galois quotients through the arithmetic class-module extension #
Let P_K be wild inertia and U an open normal subgroup of the absolute Galois group
G_K. If ⁅P_K, P_K⁆ ≤ U, the image of V = P_K U in G_K/U is an abelian
p-group, for p the residue characteristic. Consequently G_K/U is a quotient of
G_K / ker(V → Vᵃᵇ(p)).
This is the last quotient in the integral generator argument: a surjection from a free
profinite group onto the arithmetic class-module extension supplies a generating tuple
in G_K/U by composition with QuotientGroup.mapOfLE.
References #
- J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.4.1).
theorem
TauCeti.abelianizationProPExtensionKernel_le_of_commutator_wildInertiaSubgroup_le
(K : Type u_1)
[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, wildInertiaSubgroup K⁆ ≤ ↑U.toOpenSubgroup)
:
If a finite local Galois quotient kills the commutator of wild inertia, it is a
quotient of the arithmetic pro-p class-module extension at P_K U.