The cross product in singular homology #

For topological spaces X and Y and coefficient objects R and S, the homology cross product is the morphism

Hₚ(X; R) ⊗ H_q(Y; S) ⟶ Hₙ(X × Y; R ⊗ S), for p + q = n.

It is the cross product HomologicalComplex.homologyCross of the singular chain complexes, Hₚ(C(X; R)) ⊗ H_q(C(Y; S)) ⟶ Hₙ(C(X; R) ⊗ C(Y; S)), followed by the map on homology induced by the Eilenberg–Mac Lane shuffle map C(X; R) ⊗ C(Y; S) ⟶ C(X × Y; R ⊗ S). On classes of cycles a and b it is the class of the shuffle product a × b. It is natural in both spaces and in both coefficient objects. As for HomologicalComplex.homologyCross, each declaration only assumes that tensoring preserves cokernels for the three objects the construction uses: tensorLeft of Hₚ(C(X; R)), and tensorRight of the cycles Z_q(C(Y; S)) and of the chains C_{q+1}(Y; S). For ModuleCat these are found by instance search.

By the Eilenberg–Zilber theorem the shuffle map is a chain homotopy equivalence with homotopy inverse the Alexander–Whitney map, so the map induced by Alexander–Whitney on homology recovers the algebraic cross product (TopCat.singularHomologyCross_comp_homologyMap_alexanderWhitney). So the Künneth theorem over a field, that the direct sum over all p + q = n of the homology cross products Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₙ(X × Y; k) is an isomorphism, reduces to the corresponding statement for the direct sum of the algebraic cross products of the singular chain complexes.

Main definitions and results #

TopCat.singularHomologyCross: the homology cross product.
TopCat.homologyπ_tensorHom_singularHomologyCross: its value on classes of cycles.
TopCat.singularHomologyCross_naturality and TopCat.singularHomologyCross_coefficient_naturality: naturality in the spaces and in the coefficients.
TopCat.singularHomologyCross_comp_homologyMap_alexanderWhitney: under the Eilenberg–Zilber isomorphism, the homology cross product is the cross product of the singular chain complexes.

References #

A. Hatcher, Algebraic Topology, Section 3.B, the cross product in homology.
S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953).

source

noncomputable def TopCat.singularHomologyCross {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) (p q n : ℕ) (h : p + q = n) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology ((toSSet.obj X).chainComplex R) p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles ((toSSet.obj Y).chainComplex S) q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (((toSSet.obj Y).chainComplex S).X ((ComplexShape.down ℕ).prev q)))] :

CategoryTheory.MonoidalCategoryStruct.tensorObj (((AlgebraicTopology.singularHomologyFunctor C p).obj R).obj X) (((AlgebraicTopology.singularHomologyFunctor C q).obj S).obj Y) ⟶ ((AlgebraicTopology.singularHomologyFunctor C n).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The homology cross product Hₚ(X; R) ⊗ H_q(Y; S) ⟶ Hₙ(X × Y; R ⊗ S) for p + q = n: the cross product of the singular chain complexes followed by the shuffle map.

Equations

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

Instances For

source

theorem TopCat.singularHomologyCross_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) (p q n : ℕ) (h : p + q = n) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology ((toSSet.obj X).chainComplex R) p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles ((toSSet.obj Y).chainComplex S) q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (((toSSet.obj Y).chainComplex S).X ((ComplexShape.down ℕ).prev q)))] :

X.singularHomologyCross Y R S p q n h = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyCross ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h) (HomologicalComplex.homologyMap (X.shuffle Y R S) n)

The homology cross product is the cross product of the singular chain complexes followed by the map induced by the shuffle map.

source

@[simp]

theorem TopCat.homologyπ_tensorHom_singularHomologyCross {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) (p q n : ℕ) (h : p + q = n) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology ((toSSet.obj X).chainComplex R) p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles ((toSSet.obj Y).chainComplex S) q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (((toSSet.obj Y).chainComplex S).X ((ComplexShape.down ℕ).prev q)))] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex R) p) (HomologicalComplex.homologyπ ((toSSet.obj Y).chainComplex S) q)) (X.singularHomologyCross Y R S p q n h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesCross ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (X.shuffle Y R S) n) (HomologicalComplex.homologyπ ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) n))

The cross product of the classes of two singular cycles is the class of their shuffle product.

source

CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.homologyπ ((toSSet.obj X).chainComplex R) p) (HomologicalComplex.homologyπ ((toSSet.obj Y).chainComplex S) q)) (X.singularHomologyCross Y R S p q n h)) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesCross ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (X.shuffle Y R S) n) (HomologicalComplex.homologyπ ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) n))) h✝

The cross product of the classes of two singular cycles is the class of their shuffle product.

source

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((AlgebraicTopology.singularHomologyFunctor C p).obj R).map f) (((AlgebraicTopology.singularHomologyFunctor C q).obj S).map g)) (X'.singularHomologyCross Y' R S p q n h) = CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R S p q n h) (((AlgebraicTopology.singularHomologyFunctor C n).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))

Naturality of the homology cross product in both spaces: f_* a × g_* b = (f × g)_* (a × b).

source

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((AlgebraicTopology.singularHomologyFunctor C p).obj R).map f) (((AlgebraicTopology.singularHomologyFunctor C q).obj S).map g)) (CategoryTheory.CategoryStruct.comp (X'.singularHomologyCross Y' R S p q n h) h✝) = CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R S p q n h) (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C n).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) h✝)

Naturality of the homology cross product in both spaces: f_* a × g_* b = (f × g)_* (a × b).

source

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((AlgebraicTopology.singularHomologyFunctor C p).map φ).app X) (((AlgebraicTopology.singularHomologyFunctor C q).map ψ).app Y)) (X.singularHomologyCross Y R' S' p q n h) = CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R S p q n h) (((AlgebraicTopology.singularHomologyFunctor C n).map (CategoryTheory.MonoidalCategoryStruct.tensorHom φ ψ)).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

Naturality of the homology cross product in both coefficient objects.

source

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (((AlgebraicTopology.singularHomologyFunctor C p).map φ).app X) (((AlgebraicTopology.singularHomologyFunctor C q).map ψ).app Y)) (CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R' S' p q n h) h✝) = CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R S p q n h) (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor C n).map (CategoryTheory.MonoidalCategoryStruct.tensorHom φ ψ)).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) h✝)

Naturality of the homology cross product in both coefficient objects.

source

@[simp]

theorem TopCat.singularHomologyCross_comp_homologyMap_alexanderWhitney {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) (p q n : ℕ) (h : p + q = n) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology ((toSSet.obj X).chainComplex R) p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles ((toSSet.obj Y).chainComplex S) q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (((toSSet.obj Y).chainComplex S).X ((ComplexShape.down ℕ).prev q)))] :

CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R S p q n h) (HomologicalComplex.homologyMap (X.alexanderWhitney Y R S) n) = HomologicalComplex.homologyCross ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h

The homology cross product under Eilenberg–Zilber: following the homology cross product by the map induced by the Alexander–Whitney map gives the cross product of the singular chain complexes. Since the Alexander–Whitney map is a chain homotopy equivalence, this identifies the homology cross product with the algebraic one.

source

theorem TopCat.singularHomologyCross_comp_homologyMap_alexanderWhitney_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.CategoryWithHomology C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft T)] [∀ (T : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight T)] (X Y : TopCat) (R S : C) (p q n : ℕ) (h : p + q = n) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft (HomologicalComplex.homology ((toSSet.obj X).chainComplex R) p))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (HomologicalComplex.cycles ((toSSet.obj Y).chainComplex S) q))] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight (((toSSet.obj Y).chainComplex S).X ((ComplexShape.down ℕ).prev q)))] {Z : C} (h✝ : HomologicalComplex.homology (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S)) n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (X.singularHomologyCross Y R S p q n h) (HomologicalComplex.homologyMap (X.alexanderWhitney Y R S) n)) h✝ = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyCross ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S) p q n h) h✝

Documentation

TauCeti.AlgebraicTopology.Singular.CrossProduct

The cross product in singular homology #

Main definitions and results #

References #