Continuous cohomology

We define continuous cohomology as the homology of homogeneous cochains.

Implementation details

We define homogenous 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 Action (TopModuleCat R) 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 ContinuousCohomology.MultiInd.d.

Main definition

• ContinuousCohomology.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 homology.

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 induces long exact sequences in certain scenarios.

@[reducible, inline]

abbrev ContinuousCohomology.Iobj {R : Type u_1} {G : Type u_2} [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) : Action (TopModuleCat R) G

The G representation C(G, rep) given a representation rep. The G action is defined by g • f := x ↦ g • f (g⁻¹ * x).

Equations

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

theorem ContinuousCohomology.Iobj_ρ_apply (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) (g : G) (f : ↑(Iobj rep).V.toModuleCat) (x : G) : ((TopModuleCat.Hom.hom ((Iobj rep).ρ g)) f) x = (TopModuleCat.Hom.hom (rep.ρ g)) (f (g⁻¹ * x))

def ContinuousCohomology.I (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor (Action (TopModuleCat R) G) (Action (TopModuleCat R) G)

The functor taking a representation rep to the representation C(G, rep).

Equations

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

@[simp]

theorem ContinuousCohomology.I_obj_V_topologicalSpace (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) : ((I R G).obj rep).V.topologicalSpace = ContinuousMap.compactOpen

@[simp]

theorem ContinuousCohomology.I_obj_V_isModule (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) : ((I R G).obj rep).V.isModule = ContinuousMap.module

@[simp]

theorem ContinuousCohomology.I_obj_V_isAddCommGroup (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) : ((I R G).obj rep).V.isAddCommGroup = ContinuousMap.instAddCommGroupContinuousMap

@[simp]

theorem ContinuousCohomology.I_obj_V_carrier (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) : ↑((I R G).obj rep).V.toModuleCat = C(G, ↑rep.V.toModuleCat)

@[simp]

theorem ContinuousCohomology.I_obj_ρ_apply (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (rep : Action (TopModuleCat R) G) (g : G) : ((I R G).obj rep).ρ g = TopModuleCat.ofHom { toFun := fun (f : C(G, ↑rep.V.toModuleCat)) => (↑(TopModuleCat.Hom.hom (rep.ρ g))).comp (f.comp ↑(Homeomorph.mulLeft g⁻¹)), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousCohomology.I_map_hom (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] {M N : Action (TopModuleCat R) G} (φ : M ⟶ N) : ((I R G).map φ).hom = TopModuleCat.ofHom (ContinuousLinearMap.compLeftContinuous R G (TopModuleCat.Hom.hom φ.hom))

instance ContinuousCohomology.instAdditiveActionTopModuleCatI (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : (I R G).Additive

instance ContinuousCohomology.instLinearActionTopModuleCatI (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor.Linear R (I R G)

def ContinuousCohomology.const (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor.id (Action (TopModuleCat R) G) ⟶ I R G

The constant function rep ⟶ C(G, rep) as a natural transformation.

Equations

• ContinuousCohomology.const R G = { app := fun (x : Action (TopModuleCat R) G) => { hom := TopModuleCat.ofHom (ContinuousLinearMap.const R G), comm := ⋯ }, naturality := ⋯ }

@[simp]

theorem ContinuousCohomology.const_app_hom (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (x✝ : Action (TopModuleCat R) G) : ((const R G).app x✝).hom = TopModuleCat.ofHom (ContinuousLinearMap.const R G)

def ContinuousCohomology.MultiInd.functor (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ → CategoryTheory.Functor (Action (TopModuleCat R) G) (Action (TopModuleCat R) G)

The n-th functor taking M to C(G, C(G,...,C(G, M))) (with n Gs). These functors form a complex, see MultiInd.complex.

Equations

• ContinuousCohomology.MultiInd.functor R G 0 = CategoryTheory.Functor.id (Action (TopModuleCat R) G)
• ContinuousCohomology.MultiInd.functor R G n.succ = (ContinuousCohomology.MultiInd.functor R G n).comp (ContinuousCohomology.I R G)

def ContinuousCohomology.MultiInd.d (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : functor R G n ⟶ functor R G (n + 1)

The differential map in MultiInd.complex.

Equations

• One or more equations did not get rendered due to their size.
• ContinuousCohomology.MultiInd.d R G 0 = ContinuousCohomology.const R G

theorem ContinuousCohomology.MultiInd.d_zero (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : d R G 0 = const R G

theorem ContinuousCohomology.MultiInd.d_succ (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : d R G (n + 1) = CategoryTheory.whiskerLeft (functor R G (n + 1)) (const R G) - CategoryTheory.whiskerRight (d R G n) (I R G)

@[simp]

theorem ContinuousCohomology.MultiInd.d_comp_d (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : CategoryTheory.CategoryStruct.comp (d R G n) (d R G (n + 1)) = 0

@[simp]

theorem ContinuousCohomology.MultiInd.d_comp_d_assoc (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) {Z : CategoryTheory.Functor (Action (TopModuleCat R) G) (Action (TopModuleCat R) G)} (h : functor R G (n + 1 + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (d R G n) (CategoryTheory.CategoryStruct.comp (d R G (n + 1)) h) = CategoryTheory.CategoryStruct.comp 0 h

def ContinuousCohomology.MultiInd.complex (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : CochainComplex (CategoryTheory.Functor (Action (TopModuleCat R) G) (Action (TopModuleCat R) 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

• ContinuousCohomology.MultiInd.complex R G = CochainComplex.of (ContinuousCohomology.MultiInd.functor R G) (ContinuousCohomology.MultiInd.d R G) ⋯

def ContinuousCohomology.invariants (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] : CategoryTheory.Functor (Action (TopModuleCat R) G) (TopModuleCat R)

The functor taking an R-linear G-representation to its G-invariant submodule.

Equations

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

instance ContinuousCohomology.instLinearActionTopModuleCatInvariants (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] : CategoryTheory.Functor.Linear R (invariants R G)

instance ContinuousCohomology.instAdditiveActionTopModuleCatInvariants (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] : (invariants R G).Additive

def ContinuousCohomology.homogeneousCochains (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor (Action (TopModuleCat R) G) (CochainComplex (TopModuleCat R) ℕ)

homogeneousCochains R G is the functor taking an R-linear G-representation to the complex of homogeneous cochains.

Equations

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

noncomputable def continuousCohomology (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : CategoryTheory.Functor (Action (TopModuleCat R) G) (TopModuleCat R)

continuousCohomology R G n is the functor taking an R-linear G-representation to its n-th continuous homology.

Equations

• continuousCohomology R G n = (ContinuousCohomology.homogeneousCochains R G).comp (HomologicalComplex.homologyFunctor (TopModuleCat R) (ComplexShape.up ℕ) n)

def ContinuousCohomology.kerHomogeneousCochainsZeroEquiv (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] (X : Action (TopModuleCat R) G) (n : ℕ) (hn : n = 1) : ↥(LinearMap.ker (TopModuleCat.Hom.hom (((homogeneousCochains R G).obj X).d 0 n))) ≃L[R] ↑((invariants R G).obj X).toModuleCat

The 0-homogeneous cochains are isomorphic to Xᴳ.

Equations

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

noncomputable def ContinuousCohomology.continuousCohomologyZeroIso (R : Type u_1) (G : Type u_2) [CommRing R] [Group G] [TopologicalSpace R] [TopologicalSpace G] [IsTopologicalGroup G] : continuousCohomology R G 0 ≅ invariants R G

H⁰_cont(G, X) ≅ Xᴳ.

Equations

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