Degree zero with trivial mod-two coefficients

The invariant-vector interpretation of degree zero identifies cohomF2 G 0 with ZMod 2. Unlike cohomFp, the coefficient representation here is over ℤ; its canonical mod-two scalar structure is recovered from its additive group. The equivalence sends the cup-product unit to 1.

noncomputable def TauCeti.cohomF2ZeroLinearEquiv (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : cohomF2 G 0 ≃ₗ[ZMod 2] ZMod 2

Zeroth continuous cohomology with the integral trivial mod-two coefficient representation is canonically ZMod 2.

theorem TauCeti.cohomF2ZeroLinearEquiv_apply (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (x : cohomF2 G 0) : (cohomF2ZeroLinearEquiv G) x = (trivialF2Equiv G) ↑((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.zeroIso (trivialF2 G)).hom) x)

The identification reads the value of the invariant representing the degree-zero class.

@[simp]

theorem TauCeti.cohomF2ZeroLinearEquiv_one (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (cohomF2ZeroLinearEquiv G) 1 = 1

The cup-product unit has coefficient value one.

theorem TauCeti.trivialF2ResMap_zero_surjective (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (S : Subgroup G) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (trivialF2ResMap G S 0))

Restriction on degree-zero mod-two cohomology is surjective: every invariant coefficient on the subgroup is already invariant on the whole group.