Continuous cohomology

We define continuous cohomology as the homology of the homogeneous cochain complex.

Implementation details

We define homogeneous cochains as g-invariant continuous function in C(G, C(G,...,C(G, M))) instead of the usual C(Gⁿ, M) to allow more general topological groups other than locally compact ones. For this to work, we also work in TopRep k G, where the G action on M is only continuous on M, and not necessarily continuous in both variables, because the G action on C(G, M) might not be continuous on both variables even if it is on M.

For the differential map, instead of a finite sum we use the inductive definition d₋₁ : M → C(G, M) := const : m ↦ g ↦ m and dₙ₊₁ : C(G, _) → C(G, C(G, _)) := const - C(G, dₙ) : f ↦ g ↦ f - dₙ (f (g)) See TopRep.d.

Main definition

• TopRep.homogeneousCochains: The functor taking an R-linear G-representation to the complex of homogeneous cochains.
• continuousCohomology: The functor taking an R-linear G-representation to its n-th continuous cohomology.

TODO

• Show that it coincides with groupCohomology for discrete groups.
• Give the usual description of cochains in terms of n-ary functions for locally compact groups.
• Show that short exact sequences induce long exact sequences in certain scenarios.

@[reducible, inline]

abbrev TopRep.resolutionX {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : ℕ → TopRep k G

The n-th term in the resolution of a topological representation induced by TopRep.coind₁.

Equations

• X.resolutionX 0 = X
• X.resolutionX n.succ = (X.resolutionX n).coind₁

def TopRep.d {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : X.resolutionX n ⟶ X.resolutionX (n + 1)

The boundary map in the resolution of a topological representation induced by TopRep.coind₁Functor.

Equations

• X.d 0 = TopRep.ofHom X.ρ.coind₁ι
• X.d n.succ = TopRep.ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (TopRep.coind₁Functor k G).map (X.d n)

theorem TopRep.d_zero {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : X.d 0 = ofHom X.ρ.coind₁ι

theorem TopRep.d_succ {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : X.d (n + 1) = ofHom (X.resolutionX (n + 1)).ρ.coind₁ι - (coind₁Functor k G).map (X.d n)

theorem TopRep.hom_d_succ {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : Hom.hom (X.d (n + 1)) = (X.resolutionX (n + 1)).ρ.coind₁ι - ContRepresentation.coind₁Map (Hom.hom (X.d n))

@[simp]

theorem TopRep.d_comp_d {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (X.d n) (X.d (n + 1)) = 0

@[simp]

theorem TopRep.d_comp_d_assoc {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) {Z : TopRep k G} (h : X.resolutionX (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.d n) (CategoryTheory.CategoryStruct.comp (X.d (n + 1)) h) = CategoryTheory.CategoryStruct.comp 0 h

@[reducible, inline]

abbrev TopRep.resolution {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : CochainComplex (TopRep k G) ℕ

The complex of functors whose behaviour pointwise takes an R-linear G-representation M to the complex M → C(G, M) → ⋯ → C(G, C(G,...,C(G, M))) → ⋯ The G-invariant submodules of it is the homogeneous cochains (shifted by one).

Equations

• X.resolution = CochainComplex.of X.resolutionX X.d ⋯

@[reducible, inline]

abbrev TopRep.resolution'X {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : TopRep k G

The shifted object in resolution by 1 degree.

Equations

• X.resolution'X n = X.resolutionX (n + 1)

@[implicit_reducible]

def TopRep.resolution'd {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : X.resolution'X n ⟶ X.resolution'X (n + 1)

The shifted boundary map of the resolution.

Equations

• X.resolution'd n = X.d (n + 1)

theorem TopRep.resolution'd_eq {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : X.resolution'd n = X.d (n + 1)

@[reducible, inline]

abbrev TopRep.resolution' {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : CochainComplex (TopRep k G) ℕ

The shifted resolution of a topological representation by 1 degree.

Equations

• X.resolution' = CochainComplex.of X.resolution'X X.resolution'd ⋯

@[reducible, inline]

abbrev TopRep.homogeneousCochains {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : CochainComplex (TopModuleCat k) ℕ

The homogeneous cochains of a topological representation.

Equations

• X.homogeneousCochains = ((TopRep.invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).obj X.resolution'

theorem TopRep.homogeneousCochains.d_eq {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (i : ℕ) : X.homogeneousCochains.d i (i + 1) = (invariantsFunctor k G).map (X.d (i + 1))

theorem TopRep.homogeneousCochains.d_apply {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (i : ℕ) (σ : ↑(X.homogeneousCochains.X i).toModuleCat) : ↑((TopModuleCat.Hom.hom (X.homogeneousCochains.d i (i + 1))) σ) = (Hom.hom (X.d (i + 1))) ↑σ

@[reducible, inline]

noncomputable abbrev continuousCohomology {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) (A : TopRep k G) : TopModuleCat k

The continuous cohomology of a continuous representation defined by taking homology of the homogeneous cochains.

Equations

• continuousCohomology n A = HomologicalComplex.homology A.homogeneousCochains n

@[reducible, inline]

noncomputable abbrev ContinuousCohomology.cocycles {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (A : TopRep k G) (n : ℕ) : TopModuleCat k

The n-cocycles Zⁿ(G, A) of a k-linear G-representation A, i.e. the kernel of the nth differential in the complex of homogeneous cochains.

Equations

• ContinuousCohomology.cocycles A n = HomologicalComplex.cycles A.homogeneousCochains n

@[reducible, inline]

noncomputable abbrev ContinuousCohomology.π {k : Type u_1} {G : Type u_2} [Ring k] [Group G] [TopologicalSpace k] [TopologicalSpace G] [IsTopologicalGroup G] (A : TopRep k G) (n : ℕ) : HomologicalComplex.cycles A.homogeneousCochains n ⟶ HomologicalComplex.homology A.homogeneousCochains n

The natural map from n-cocycles to nth continuous cohomology for a k-linear G-representation A.

Equations

• ContinuousCohomology.π A n = HomologicalComplex.homologyπ A.homogeneousCochains n