Cohomological dimension read on the explicit cohomology #
The vanishing predicate CohomologicalDimensionLE p G n is stated against Mathlib's continuous
cohomology continuousCohomology i (ofDiscreteModule ℤ G M), while the low-degree theory of
LowDegree.lean works with the explicit cocycle models H¹(G, M) and H²(G, M). This file
transfers the vanishing through the comparison of CohomologyComparison.lean: for a locally
compact group G with cd_p G ≤ 1, the explicit H²(G, A) of every discrete p-primary
G-module A is trivial.
The coefficients live in the universe of G: the continuous-cohomology side needs them in a
universe containing that of G, and the explicit comparison is stated for coefficients in
exactly that universe.
Main results #
TauCeti.CohomologicalDimensionLE.subsingleton_H2:cd_p G ≤ 1kills the explicitH²of every discretep-primaryG-module.
theorem
TauCeti.CohomologicalDimensionLE.subsingleton_H2
{p : ℕ}
{G : Type u}
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
[LocallyCompactSpace G]
(hcd : CohomologicalDimensionLE p G 1)
(A : Type u)
[AddCommGroup A]
[TopologicalSpace A]
[DiscreteTopology A]
[DistribMulAction G A]
[ContinuousSMul G A]
(hA : IsPPrimaryTorsion p A)
:
cd_p G ≤ 1 kills the explicit H² of every discrete p-primary G-module.