Descent of continuous two-cocycles to finite quotients

For a profinite group G and a discrete continuous G-module M, every continuous 2-cocycle on G is inflated from a finite quotient. The descent is strict: no coboundary is subtracted from the cocycle.

Strict descent supplies the representative-level surjectivity needed to describe continuous degree-two cohomology as a colimit of cohomology groups over finite quotients.

Main statement

• TauCeti.ContCohomology.exists_openNormalSubgroup_descendZ2: every continuous 2-cocycle itself descends to a finite quotient, with equality on representatives.
• TauCeti.ContCohomology.exists_explicitInfl2_eq: consequently every class in H²(G, M) is in the image of a finite-level inflation map.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (1.2.5).
• L. Ribes and P. Zalesskii, Profinite Groups, Cor. 6.5.6(a).

theorem TauCeti.ContCohomology.exists_openNormalSubgroup_descendZ2 {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] [DiscreteTopology M] (z : ↥(Z2 G M)) : ∃ (U : OpenNormalSubgroup G) (c : ↥(Z2 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M))), ∀ (g h : G), ↑(↑c (↑g, ↑h)) = ↑z (g, h)

Strict finite-level descent in degree two. Every continuous 2-cocycle on a profinite group with discrete coefficients is itself the pullback of a 2-cocycle on G ⧸ U with values in M ^ U, for some open normal subgroup U. The equality is on cochain representatives, not only on their classes.

theorem TauCeti.ContCohomology.exists_explicitInfl2_eq {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [CompactSpace G] [TotallyDisconnectedSpace G] [DiscreteTopology M] (x : H2 G M) : ∃ (U : OpenNormalSubgroup G) (y : H2 (G ⧸ ↑U.toOpenSubgroup) ↥(FixedPoints.addSubgroup (↥↑U.toOpenSubgroup) M)), (explicitInfl2 G M ↑U.toOpenSubgroup) y = x

Surjectivity of the degree-two finite-quotient comparison maps. Every class in H²(G, M) is inflated from H²(G ⧸ U, M ^ U) for some open normal subgroup U.