The pro-p class module for a p-group quotient

Let G be a profinite group with scd_p G ≤ 2 and let V be an open normal subgroup such that G ⧸ V is a p-group. Then H¹(G ⧸ V, V^ab(p)) = 0, and H²(G ⧸ V, V^ab(p)) is cyclic of order #(G ⧸ V), generated by the class u_{G/V}(p) (TauCeti.abelianizationProPClass). This is NSW (3.6.4), (ii) ⇒ (iii), for p-group quotients; the Sylow argument of (3.6.3) passes from these to arbitrary finite quotients.

Main results

• TauCeti.subsingleton_h1_abelianizationProP_of_isPGroup: H¹(G ⧸ V, V^ab(p)) = 0 for a p-group quotient G ⧸ V.
• TauCeti.abelianizationProPClass_generates_of_isPGroup: for a p-group quotient G ⧸ V, u_{G/V}(p) generates H²(G ⧸ V, V^ab(p)), a group of order #(G ⧸ V).

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., the proofs of (3.6.3) and of (3.6.4), (ii) ⇒ (iii).

theorem TauCeti.abelianizationProPClass_generates_of_isPGroup {p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {V : Subgroup G} [V.Normal] (hp : Nat.Prime p) (h : strictCohomologicalDimensionAt p G ≤ 2) (hV : IsOpen ↑V) (hpV : IsPGroup p (G ⧸ V)) : AddSubgroup.zmultiples (abelianizationProPClass p G V hV) = ⊤ ∧ Nat.card (ContCohomology.H2 (G ⧸ V) (Additive (abelianizationProP p G V))) = Nat.card (G ⧸ V)

For a profinite group G with scd_p G ≤ 2 and an open normal subgroup V whose quotient G ⧸ V is a p-group, u_{G/V}(p) generates H²(G ⧸ V, V^ab(p)), a group of order #(G ⧸ V).