The cohomology class of the pro-p class-module extension

For an open normal subgroup V of a profinite group G, the bundled extension 1 → Vᵃᵇ(p) → G / ker(V → Vᵃᵇ(p)) → G/V → 1 has class abelianizationProPClass. This identifies the class used in extension lifting with the explicit cocycle built from quotient representatives. In particular, generation results about the explicit class apply to the actual profinite extension.

The quotient representatives need not send 1 to 1. Their section still gives the explicit cocycle, and comparison with a normalized continuous section changes it by a continuous coboundary.

References

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

@[simp]

theorem TauCeti.abelianizationProPProfiniteExtension_contCohomologyClass (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (V : Subgroup G) [V.Normal] [CompactSpace G] [TotallyDisconnectedSpace G] (hV : IsOpen ↑V) : (abelianizationProPProfiniteExtension p G V).contCohomologyClass = abelianizationProPClass p G V hV

The continuous cohomology class of the bundled pro-p class-module extension is the explicit class u_{G/V}(p) defined by quotient representatives.