Additivity and linearity of continuous cohomology

This file proves that the compatible-pair map on continuous cohomology is additive in its coefficient morphism. Over a commutative coefficient ring it also commutes with scalar multiplication. Consequently Hⁿ(G, -), packaged as TauCeti.ContinuousCohomology.continuousCohomologyFunctor, is an additive and linear functor.

The proof follows the construction through Mathlib's coinduced resolution: resolutionMap, cochainsMap, cocyclesMap, and finally the induced map on homology. The cochain- and cocycle-level statements are public because later constructions, in particular connecting maps and cup products, need linearity before passing to cohomology.

Main results

• TauCeti.ContinuousCohomology.map_add and TauCeti.ContinuousCohomology.map_smul give additivity and linearity of the map associated to a compatible pair.
• TauCeti.ContinuousCohomology.mapAddHom and TauCeti.ContinuousCohomology.mapLinearMap bundle that dependence as an additive homomorphism and a linear map.
• TauCeti.ContinuousCohomology.continuousCochainsFunctor is the additive functor of homogeneous cochain complexes, with continuousCochainsFunctorCompHomologyIso; its action on maps of discrete modules is cochainsMap_ofDiscreteModulePair_id.
• TauCeti.ContinuousCohomology.continuousCohomologyFunctor_additive and TauCeti.ContinuousCohomology.continuousCohomologyFunctor_linear install the corresponding functor instances.
• TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_subsingleton: continuous cohomology vanishes on subsingleton coefficients, a consequence of additivity.
• TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_ofDiscreteModule_of_subsingleton: the same for the discrete module attached to a subsingleton carrier.
• TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_iso: continuous cohomology vanishes on coefficients isomorphic to ones on which it vanishes.
• subsingleton_continuousCohomology_ofDiscreteModule_of_continuousMulEquiv: the same along a topological group isomorphism and an equivariant isomorphism of discrete modules.

@[simp]

theorem TauCeti.ContinuousCohomology.cochainsMap_zero {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) : ContinuousCohomology.cochainsMap φ 0 = 0

The compatible-pair cochain map induced by the zero coefficient morphism is zero.

@[simp]

theorem TauCeti.ContinuousCohomology.cochainsMap_add {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f g : TopRep.res (↑φ) X ⟶ Y) : ContinuousCohomology.cochainsMap φ (f + g) = ContinuousCohomology.cochainsMap φ f + ContinuousCohomology.cochainsMap φ g

Compatible-pair cochain maps are additive in the coefficient morphism.

@[simp]

theorem TauCeti.ContinuousCohomology.cocyclesMap_zero {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (n : ℕ) : ContinuousCohomology.cocyclesMap φ 0 n = 0

The map on continuous cocycles induced by the zero coefficient morphism is zero.

@[simp]

theorem TauCeti.ContinuousCohomology.cocyclesMap_add {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f g : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : ContinuousCohomology.cocyclesMap φ (f + g) n = ContinuousCohomology.cocyclesMap φ f n + ContinuousCohomology.cocyclesMap φ g n

Maps on continuous cocycles are additive in the coefficient morphism.

@[simp]

theorem TauCeti.ContinuousCohomology.map_zero {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (n : ℕ) : ContinuousCohomology.map φ 0 n = 0

The map on continuous cohomology induced by the zero coefficient morphism is zero.

@[simp]

theorem TauCeti.ContinuousCohomology.map_add {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f g : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : ContinuousCohomology.map φ (f + g) n = ContinuousCohomology.map φ f n + ContinuousCohomology.map φ g n

Maps on continuous cohomology are additive in the coefficient morphism.

noncomputable def TauCeti.ContinuousCohomology.mapAddHom {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (φ : H →ₜ* G) (X : TopRep R G) (Y : TopRep R H) (n : ℕ) : (TopRep.res (↑φ) X ⟶ Y) →+ (continuousCohomology n X ⟶ continuousCohomology n Y)

The map on continuous cohomology induced by a fixed group homomorphism, bundled as an additive homomorphism in the coefficient morphism.

Equations

• TauCeti.ContinuousCohomology.mapAddHom φ X Y n = { toFun := fun (f : TopRep.res (↑φ) X ⟶ Y) => ContinuousCohomology.map φ f n, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.ContinuousCohomology.mapAddHom_apply {R : Type u} {G H : Type v} [Ring R] [TopologicalSpace R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : (mapAddHom φ X Y n) f = ContinuousCohomology.map φ f n

@[simp]

theorem TauCeti.ContinuousCohomology.cochainsMap_smul {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {R : Type u} [CommRing R] [TopologicalSpace R] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (r : R) (f : TopRep.res (↑φ) X ⟶ Y) : ContinuousCohomology.cochainsMap φ (r • f) = r • ContinuousCohomology.cochainsMap φ f

Compatible-pair cochain maps commute with scalar multiplication of the coefficient morphism.

@[simp]

theorem TauCeti.ContinuousCohomology.cocyclesMap_smul {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {R : Type u} [CommRing R] [TopologicalSpace R] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (r : R) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : ContinuousCohomology.cocyclesMap φ (r • f) n = r • ContinuousCohomology.cocyclesMap φ f n

Maps on continuous cocycles commute with scalar multiplication of the coefficient morphism.

@[simp]

theorem TauCeti.ContinuousCohomology.map_smul {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {R : Type u} [CommRing R] [TopologicalSpace R] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (r : R) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : ContinuousCohomology.map φ (r • f) n = r • ContinuousCohomology.map φ f n

Maps on continuous cohomology commute with scalar multiplication of the coefficient morphism.

noncomputable def TauCeti.ContinuousCohomology.mapLinearMap {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {R : Type u} [CommRing R] [TopologicalSpace R] (φ : H →ₜ* G) (X : TopRep R G) (Y : TopRep R H) (n : ℕ) : (TopRep.res (↑φ) X ⟶ Y) →ₗ[R] continuousCohomology n X ⟶ continuousCohomology n Y

The map on continuous cohomology induced by a fixed group homomorphism, bundled as a linear map in the coefficient morphism.

Equations

• TauCeti.ContinuousCohomology.mapLinearMap φ X Y n = { toFun := (↑(TauCeti.ContinuousCohomology.mapAddHom φ X Y n)).toFun, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ContinuousCohomology.mapLinearMap_apply {G H : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {R : Type u} [CommRing R] [TopologicalSpace R] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : (mapLinearMap φ X Y n) f = ContinuousCohomology.map φ f n

instance TauCeti.ContinuousCohomology.continuousCohomologyFunctor_additive (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : (continuousCohomologyFunctor R G n).Additive

Continuous cohomology in a fixed degree is additive in the coefficient representation.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_subsingleton {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [Subsingleton ↑X] (n : ℕ) : Subsingleton ↑(continuousCohomology n X).toModuleCat

Continuous cohomology vanishes on a coefficient representation whose carrier is a subsingleton: the identity of such a representation is the zero morphism, and the additive functor continuousCohomologyFunctor sends it to the zero endomorphism of the cohomology.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_ofDiscreteModule_of_subsingleton {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (M : Type (max v w)) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] [Subsingleton M] (n : ℕ) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule R G M)).toModuleCat

Continuous cohomology vanishes on a discrete module with subsingleton carrier: the carrier of ofDiscreteModule R G M is M itself, so the representation is a subsingleton and subsingleton_continuousCohomology_of_subsingleton applies.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_of_iso {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (e : X ≅ Y) (n : ℕ) [Subsingleton ↑(continuousCohomology n Y).toModuleCat] : Subsingleton ↑(continuousCohomology n X).toModuleCat

Continuous cohomology vanishes on a coefficient representation isomorphic to one on which it vanishes: the coefficient map of the isomorphism is a bijection of the cohomology modules.

theorem TauCeti.ContinuousCohomology.subsingleton_continuousCohomology_ofDiscreteModule_of_continuousMulEquiv {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] (e : H ≃ₜ* G) {M N : Type (max v w)} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [SMulCommClass H R N] [ContinuousSMul R N] (f : M ≃ₗ[R] N) (hf : ∀ (h : H) (m : M), f (e h • m) = h • f m) (n : ℕ) [Subsingleton ↑(continuousCohomology n (ofDiscreteModule R G M)).toModuleCat] : Subsingleton ↑(continuousCohomology n (ofDiscreteModule R H N)).toModuleCat

Continuous cohomology vanishes on a discrete module carried along a topological group isomorphism from one on which it vanishes: for e : H ≃ₜ* G and an R-linear isomorphism f : M ≃ₗ[R] N with f (e h • m) = h • f m, the map along e and f has a right inverse, the map along e⁻¹ and f⁻¹.

instance TauCeti.ContinuousCohomology.continuousCohomologyFunctor_linear (R : Type u) [CommRing R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : CategoryTheory.Functor.Linear R (continuousCohomologyFunctor R G n)

Continuous cohomology in a fixed degree is linear in the coefficient representation.

The cochain functor

noncomputable def TauCeti.ContinuousCohomology.continuousCochainsFunctor (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor (TopRep R G) (CochainComplex (TopModuleCat R) ℕ)

Mathlib's homogeneous cochain complex TopRep.homogeneousCochains as a functor in the coefficients. Its action on morphisms is the compatible-pair cochain map at φ = id, the cochain-level counterpart of TauCeti.ContinuousCohomology.coeffMap.

Equations

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

@[simp]

theorem TauCeti.ContinuousCohomology.continuousCochainsFunctor_map (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X✝ Y✝ : TopRep R G} (f : X✝ ⟶ Y✝) : (continuousCochainsFunctor R G).map f = ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) f

@[simp]

theorem TauCeti.ContinuousCohomology.continuousCochainsFunctor_obj (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : (continuousCochainsFunctor R G).obj X = X.homogeneousCochains

instance TauCeti.ContinuousCohomology.continuousCochainsFunctor_additive (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (continuousCochainsFunctor R G).Additive

The cochain functor is additive in the coefficient representation.

noncomputable def TauCeti.ContinuousCohomology.continuousCochainsFunctorCompHomologyIso (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (n : ℕ) : (continuousCochainsFunctor R G).comp (HomologicalComplex.homologyFunctor (TopModuleCat R) (ComplexShape.up ℕ) n) ≅ continuousCohomologyFunctor R G n

The homology of the cochain functor in degree n is continuous cohomology continuousCohomologyFunctor R G n; the two functors agree on objects and morphisms by definition.

Equations

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

theorem TauCeti.ContinuousCohomology.cochainsMap_ofDiscreteModulePair_id {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {M N : Type v} [AddCommGroup M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [AddCommGroup N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] {f : M →+ N} (hf : ∀ (g : G) (m : M), f (g • m) = g • f m) : ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) (ofDiscreteModulePair (↑(ContinuousMonoidHom.id G)) f.toIntLinearMap hf) = (continuousCochainsFunctor ℤ G).map (ofDiscreteModuleMap f.toIntLinearMap hf)

The cochain map of an equivariant map of discrete modules agrees with the cochain functor applied to the corresponding map of topological representations.

theorem TauCeti.ContinuousCohomology.forget₂_map_map {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).map (ContinuousCohomology.map φ f n) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.sc X.homogeneousCochains n).mapHomologyIso (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (((CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).mapHomologicalComplex (ComplexShape.up ℕ)).map (ContinuousCohomology.cochainsMap φ f)) n) ((HomologicalComplex.sc Y.homogeneousCochains n).mapHomologyIso (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))).hom)

After forgetting topologies, the map Hⁿ(G, X) ⟶ Hⁿ(H, Y) of a compatible pair is the map induced on the homology of the forgotten homogeneous-cochain complexes by cochainsMap φ f, conjugated by the identifications CategoryTheory.ShortComplex.mapHomologyIso of that homology with the underlying modules of continuous cohomology.

theorem TauCeti.ContinuousCohomology.forget₂_map_coeffMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep R G} (f : X ⟶ Y) (n : ℕ) : (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).map (coeffMap f n) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.sc X.homogeneousCochains n).mapHomologyIso (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))).inv (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (((CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).mapHomologicalComplex (ComplexShape.up ℕ)).map ((continuousCochainsFunctor R G).map f)) n) ((HomologicalComplex.sc Y.homogeneousCochains n).mapHomologyIso (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R))).hom)

After forgetting topologies, the coefficient map Hⁿ(G, X) ⟶ Hⁿ(G, Y) is the map induced on the homology of the forgotten homogeneous-cochain complexes, conjugated by the identifications CategoryTheory.ShortComplex.mapHomologyIso of that homology with the underlying modules of continuous cohomology. This is forget₂_map_map at φ = id.