Quotients of a pro-p class-module extension

Let V be a subgroup of a topological group G. A continuous homomorphism from G to a profinite group kills the kernel of V → Vᵃᵇ(p) as soon as it maps V into a closed abelian pro-p subgroup (TauCeti.abelianizationProPExtensionKernel_le_ker). When V is normal, the homomorphism therefore factors through the class-module extension G / ker(V → Vᵃᵇ(p)).

The two instances used are a profinite extension whose kernel is an abelian pro-p group, into which a free presentation maps its relation subgroup, and a finite quotient G/U in which the image of V is an abelian p-group (TauCeti.abelianizationProPExtensionKernel_le_of_isPGroup_map). The latter permits a generating family of the class-module extension to be read in the finite quotient.

References

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

theorem TauCeti.abelianizationProPExtensionKernel_le_ker {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p : ℕ) (V : Subgroup G) {E : Type u_2} [Group E] [TopologicalSpace E] [IsTopologicalGroup E] [CompactSpace E] [TotallyDisconnectedSpace E] (φ : G →ₜ* E) (A : Subgroup E) [IsMulCommutative ↥A] (hA : IsClosed ↑A) (hpro : IsProP p ↥A) (hVA : V ≤ Subgroup.comap (↑φ) A) : abelianizationProPExtensionKernel p G V ≤ (↑φ).ker

A continuous homomorphism to a profinite group which maps V into a closed abelian pro-p subgroup A kills the kernel of V → Vᵃᵇ(p).

theorem TauCeti.abelianizationProPExtensionKernel_le_of_isPGroup_map {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (p : ℕ) (V : Subgroup G) (U : OpenNormalSubgroup G) [(↑U.toOpenSubgroup).FiniteIndex] (hpro : IsPGroup p ↥(Subgroup.map (QuotientGroup.mk' ↑U.toOpenSubgroup) V)) (hcomm : ⁅V, V⁆ ≤ ↑U.toOpenSubgroup) : abelianizationProPExtensionKernel p G V ≤ ↑U.toOpenSubgroup

A finite quotient in which the image of V is an abelian p-group kills the kernel of V → Vᵃᵇ(p). For normal V, this is the inclusion needed by QuotientGroup.mapOfLE to factor the quotient through the pro-p class-module extension.