Zeroth continuous cohomology with trivial ZMod p coefficients #
The canonical identification cohomFpZeroLinearEquiv sends zeroth continuous cohomology to
the underlying coefficient value in ZMod p. In particular, the cohomology module is finite
over ZMod p; when p is prime, it is a finite-dimensional vector space over 𝔽_p.
This identification specializes Mathlib's ContinuousCohomology.zeroIso, composed with
LinearEquiv.ofTop for the trivial action and trivialFpEquiv for the coefficient value.
noncomputable def
TauCeti.cohomFpZeroLinearEquiv
(p : ℕ)
(G : Type u)
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
:
Zeroth continuous cohomology with trivial coefficients is canonically ZMod p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.cohomFpZeroLinearEquiv_apply
(p : ℕ)
(G : Type u)
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
(x : ↑(cohomFp p G 0).toModuleCat)
:
(cohomFpZeroLinearEquiv p G) x = (trivialFpEquiv p G) ↑((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso (trivialFp p G)).hom) x)
The canonical identification reads the coefficient value of the invariant representing the cohomology class.
instance
TauCeti.instFiniteZModCarrierCohomFpOfNatNat
(p : ℕ)
(G : Type u)
[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]
:
Module.Finite (ZMod p) ↑(cohomFp p G 0).toModuleCat
Zeroth continuous cohomology with trivial coefficients is finite as a ZMod p-module.