Low degree continuous cohomology

In this file we show that the zeroth continuous cohomology is isomorphic to the invariants of the representation.

theorem ContinuousCohomology.cocycles₀IsoAux {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (σ : ↑(X.homogeneousCochains.X 0).toModuleCat) (hσ : σ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker) : ↑σ 1 ∈ X.ρ.invariants

theorem ContinuousCohomology.mem_const_resol₀ {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (x : ↑X) (hx : x ∈ X.ρ.invariants) : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants

theorem ContinuousCohomology.cocycles₀IsoAux' {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (x : ↑X) (h : ContinuousMap.const G x ∈ (X.resolution'.X 0).ρ.invariants) : ⟨ContinuousMap.const G x, h⟩ ∈ (↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker

@[reducible, inline]

noncomputable abbrev ContinuousCohomology.cocycles₀Iso {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : cocycles X 0 ≅ TopModuleCat.of k ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker

The isomorphism between the zeroth cocycles and the kernel of the zeroth differential.

Equations

• One or more equations did not get rendered due to their size.

def ContinuousCohomology.d₀kerIso {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : ↥(↑(TopModuleCat.Hom.hom (X.homogeneousCochains.d 0 1))).ker ≃L[k] ↥X.ρ.invariants

The isomorphism between the kernel of the zeroth differential and the invariants of a representation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ContinuousCohomology.zeroIso {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (A : TopRep k G) : continuousCohomology 0 A ≅ TopModuleCat.of k ↥A.ρ.invariants

The isomorphism between the zeroth continuous cohomology group and the invariants of a representation.

Equations

• ContinuousCohomology.zeroIso A = A.homogeneousCochains.isoHomologyπ₀.symm ≪≫ ContinuousCohomology.cocycles₀Iso A ≪≫ TopModuleCat.ofIso (ContinuousCohomology.d₀kerIso A)