Functoriality of continuous cohomology

Given topological groups G and H, a continuous group homomorphism φ : H →ₜ* G, a topological representation X of G, a topological representation Y of H, and a morphism of topological H-representations f : res φ X ⟶ Y, we construct a cochain map homogeneousCochains X ⟶ homogeneousCochains Y and hence maps on continuous cohomology Hⁿ(G, X) ⟶ Hⁿ(H, Y).

Main definitions

• ContinuousCohomology.cochainsMap φ f : the cochain map homogeneousCochains X ⟶ homogeneousCochains Y induced by φ : H →ₜ* G and f : res φ X ⟶ Y, sending an invariant function σ : C(G, C(G, ⋯)) to f ∘ σ ∘ φ.
• ContinuousCohomology.map φ f n : the induced map Hⁿ(G, X) ⟶ Hⁿ(H, Y) on continuous cohomology.

def ContinuousCohomology.resolutionMap {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ) : TopRep.res (↑φ) (X.resolutionX i) ⟶ Y.resolutionX i

The morphisms between the levels of the standard resolutions of X and Y induced by a continuous group homomorphism φ : H →ₜ* G and a morphism f : res φ X ⟶ Y, given by F ↦ f ∘ F ∘ φ.

Equations

• ContinuousCohomology.resolutionMap φ f 0 = f
• ContinuousCohomology.resolutionMap φ f i.succ = TopRep.ofHom (ContRepresentation.coind₁ResMap φ (TopRep.Hom.hom (ContinuousCohomology.resolutionMap φ f i)))

@[simp]

theorem ContinuousCohomology.resolutionMap_zero {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) : resolutionMap φ f 0 = f

theorem ContinuousCohomology.resolutionMap_succ {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ) : resolutionMap φ f (i + 1) = TopRep.ofHom (ContRepresentation.coind₁ResMap φ (TopRep.Hom.hom (resolutionMap φ f i)))

@[simp]

theorem ContinuousCohomology.resolutionMap_id {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (i : ℕ) : resolutionMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) i = CategoryTheory.CategoryStruct.id (X.resolutionX i)

theorem ContinuousCohomology.resolutionMap_comp {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) (i : ℕ) : resolutionMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) i = CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map (resolutionMap φ f i)) (resolutionMap ψ g i)

theorem ContinuousCohomology.resolutionMap_comp_d {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ) : CategoryTheory.CategoryStruct.comp (resolutionMap φ f i) (Y.d i) = CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑φ).map (X.d i)) (resolutionMap φ f (i + 1))

The maps resolutionMap φ f commute with the differentials of the resolutions.

def ContinuousCohomology.cochainsMap {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) : X.homogeneousCochains ⟶ Y.homogeneousCochains

The cochain map homogeneousCochains X ⟶ homogeneousCochains Y induced by a continuous group homomorphism φ : H →ₜ* G and a morphism of topological H-representations f : res φ X ⟶ Y, sending an invariant function σ : C(G, C(G, ⋯)) to f ∘ σ ∘ φ.

Equations

• ContinuousCohomology.cochainsMap φ f = { f := fun (i : ℕ) => TopRep.invariantsResMap (↑φ) (ContinuousCohomology.resolutionMap φ f (i + 1)), comm' := ⋯ }

theorem ContinuousCohomology.cochainsMap_f {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ) : (cochainsMap φ f).f i = TopRep.invariantsResMap (↑φ) (resolutionMap φ f (i + 1))

theorem ContinuousCohomology.cochainsMap_f_hom {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ) : TopModuleCat.Hom.hom ((cochainsMap φ f).f i) = ContIntertwiningMap.mapInvariantsOfRes (↑φ) (TopRep.Hom.hom (resolutionMap φ f (i + 1)))

@[simp]

theorem ContinuousCohomology.cochainsMap_id {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : cochainsMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.homogeneousCochains

theorem ContinuousCohomology.cochainsMap_comp {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) : cochainsMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) = CategoryTheory.CategoryStruct.comp (cochainsMap φ f) (cochainsMap ψ g)

theorem ContinuousCohomology.cochainsMap_comp_assoc {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) {Z✝ : CochainComplex (TopModuleCat k) ℕ} (h : Z.homogeneousCochains ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (cochainsMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑ψ) (TopRep.Hom.hom f))) g)) h = CategoryTheory.CategoryStruct.comp (cochainsMap φ f) (CategoryTheory.CategoryStruct.comp (cochainsMap ψ g) h)

@[reducible, inline]

noncomputable abbrev ContinuousCohomology.cocyclesMap {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : cocycles X n ⟶ cocycles Y n

The map Zⁿ(G, X) ⟶ Zⁿ(H, Y) on cocycles induced by a continuous group homomorphism φ : H →ₜ* G and a morphism of topological H-representations f : res φ X ⟶ Y.

Equations

• ContinuousCohomology.cocyclesMap φ f n = HomologicalComplex.cyclesMap (ContinuousCohomology.cochainsMap φ f) n

@[simp]

theorem ContinuousCohomology.cocyclesMap_id {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : cocyclesMap (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) n = CategoryTheory.CategoryStruct.id (cocycles X n)

theorem ContinuousCohomology.cocyclesMap_comp {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ) : cocyclesMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) n = CategoryTheory.CategoryStruct.comp (cocyclesMap φ f n) (cocyclesMap ψ g n)

theorem ContinuousCohomology.cocyclesMap_comp_assoc {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ) {Z✝ : TopModuleCat k} (h : cocycles Z n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (cocyclesMap (φ.comp ψ) (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑ψ) (TopRep.Hom.hom f))) g) n) h = CategoryTheory.CategoryStruct.comp (cocyclesMap φ f n) (CategoryTheory.CategoryStruct.comp (cocyclesMap ψ g n) h)

@[reducible, inline]

noncomputable abbrev ContinuousCohomology.map {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : continuousCohomology n X ⟶ continuousCohomology n Y

The map Hⁿ(G, X) ⟶ Hⁿ(H, Y) on continuous cohomology induced by a continuous group homomorphism φ : H →ₜ* G and a morphism of topological H-representations f : res φ X ⟶ Y.

Equations

• ContinuousCohomology.map φ f n = HomologicalComplex.homologyMap (ContinuousCohomology.cochainsMap φ f) n

theorem ContinuousCohomology.π_map {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (π X n) (map φ f n) = CategoryTheory.CategoryStruct.comp (cocyclesMap φ f n) (π Y n)

theorem ContinuousCohomology.π_map_assoc {k : Type u} {G H : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (n : ℕ) {Z : TopModuleCat k} (h : continuousCohomology n Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (π X n) (CategoryTheory.CategoryStruct.comp (map φ f n) h) = CategoryTheory.CategoryStruct.comp (cocyclesMap φ f n) (CategoryTheory.CategoryStruct.comp (π Y n) h)

@[simp]

theorem ContinuousCohomology.map_id {k : Type u} {G : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : map (ContinuousMonoidHom.id G) (CategoryTheory.CategoryStruct.id X) n = CategoryTheory.CategoryStruct.id (continuousCohomology n X)

theorem ContinuousCohomology.map_comp {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ) : map (φ.comp ψ) (CategoryTheory.CategoryStruct.comp ((TopRep.resFunctor ↑ψ).map f) g) n = CategoryTheory.CategoryStruct.comp (map φ f n) (map ψ g n)

theorem ContinuousCohomology.map_comp_assoc {k : Type u} {G H K : Type v} [Ring k] [TopologicalSpace k] [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [Group K] [TopologicalSpace K] [IsTopologicalGroup K] {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y) (g : TopRep.res (↑ψ) Y ⟶ Z) (n : ℕ) {Z✝ : TopModuleCat k} (h : continuousCohomology n Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (map (φ.comp ψ) (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑ψ) (TopRep.Hom.hom f))) g) n) h = CategoryTheory.CategoryStruct.comp (map φ f n) (CategoryTheory.CategoryStruct.comp (map ψ g n) h)