Continuous cohomology of a finite discrete group in every degree

Let G be a finite group with the discrete topology and M a discrete G-module. In every degree n the canonical continuous cohomology Hⁿ(G, M) is isomorphic to Mathlib's discrete group cohomology of the representation Rep.ofDistribMulAction ℤ G M (TauCeti.ContCohomology.nonempty_continuousCohomology_addEquiv_groupCohomology).

In degrees 0 and 1 this is the composite of the explicit low-degree comparisons on both sides. The higher degrees follow by dimension shifting, run in parallel in the two theories along the same short exact sequence

0 → M → Coind_1^G M → Coind_1^G M ⧸ M → 0.

Its middle term is acyclic in positive degrees for continuous cohomology (TauCeti.ContCohomology.dimensionShiftIso) and, being the representation coindBot ℤ G M coinduced from the trivial subgroup, for group cohomology (groupCohomology.isZero_coindBot_succ). So the two connecting maps identify Hⁿ⁺²(G, M) with Hⁿ⁺¹(G, Coind_1^G M ⧸ M) in both theories, and induction on the degree, over all coefficient modules at once, finishes.

This is what lets a vanishing statement about the cohomology of the finite layers of a profinite group, proved in Mathlib's groupCohomology (for instance by Tate's theorem), be read in the finite-quotient colimit description of continuous cohomology.

Main results

• TauCeti.ContCohomology.nonempty_continuousCohomology_addEquiv_groupCohomology: an additive equivalence Hⁿ(G, M) ≃+ groupCohomology (Rep.ofDistribMulAction ℤ G M) n exists for every n.

Implementation notes

The isomorphism is assembled from the connecting maps of the two long exact sequences and from the low-degree comparisons; its naturality is not proved here, so it is stated as the existence of an additive equivalence, which is the form vanishing and finiteness statements consume. Finiteness of G enters only through the acyclicity of Coind_1^G M in continuous cohomology, which is proved for compact groups.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §2.2.
• K. S. Brown, Cohomology of Groups, Chapter III, §7 (dimension shifting).

The dimension-shifting sequence in Rep ℤ G

The comparison in every degree

theorem TauCeti.ContCohomology.nonempty_continuousCohomology_addEquiv_groupCohomology (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] (M : Type) [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [Finite G] (n : ℕ) : Nonempty (↑(continuousCohomology n (ofDiscreteModule ℤ G M)).toModuleCat ≃+ ↑(groupCohomology (Rep.ofDistribMulAction ℤ G M) n))

The continuous cohomology of a finite discrete group is its group cohomology, in every degree: for a finite group G with the discrete topology and a discrete G-module M, Hⁿ(G, M) is additively isomorphic to Mathlib's groupCohomology of Rep.ofDistribMulAction ℤ G M.