The cubical cross product and the simplicial cross product

For a commutative ring k and spaces X and Y, there are two natural chain maps N(X; k) ⊗ N(Y; k) ⟶ C(X × Y; k) from the tensor product of the normalized cubical chains to the simplicial singular chains of the product:

• the cubical cross product TauCeti.cubicalCrossProduct followed by the comparison map TauCeti.cubicalToSingular;
• the tensor product of two comparison maps followed by the simplicial cross product, the shuffle map of Eilenberg and Mac Lane (TopCat.shuffle) with the coefficients k ⊗ k identified with k by the unitor (TauCeti.singularCrossProduct).

They agree on the augmentation in degree zero, and the singular chains of the product are acyclic on the models of the tensor product (TauCeti.cubicalTensorModelPresentation), so by the method of acyclic models they are naturally chain homotopic (TauCeti.cubicalSingularCrossProductHomotopy), and equal on homology.

Main definitions and results

• TauCeti.cubicalCrossProductToSingular, TauCeti.singularCrossProductOfCubical: the two natural chain maps, on pairs of spaces.
• TauCeti.cubicalSingularCrossProductHomotopy: the chain homotopy between them, natural in both spaces (TauCeti.cubicalSingularCrossProductHomotopy_hom_naturality).
• TauCeti.homologyMap_cubicalCrossProductToSingularApp_eq_singularCrossProductOfCubicalApp: they have the same map on homology.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter VII, for the cubical cross product and the comparison of the cubical and simplicial chains by acyclic models.
• S. Eilenberg and S. Mac Lane, Acyclic models, Amer. J. Math. 75 (1953).
• S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953), for the shuffle map.

noncomputable def TauCeti.cubicalCrossProductToSingularApp (k : Type u) [CommRing k] (X Y : TopCat) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((normalizedCubicalChainComplex k).obj X) ((normalizedCubicalChainComplex k).obj Y) ⟶ (singularChains k).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The cubical cross product followed by the comparison map to simplicial chains.

noncomputable def TauCeti.singularCrossProductOfCubicalApp (k : Type u) [CommRing k] (X Y : TopCat) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((normalizedCubicalChainComplex k).obj X) ((normalizedCubicalChainComplex k).obj Y) ⟶ (singularChains k).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The tensor product of the two comparison maps followed by the simplicial cross product.

theorem TauCeti.cubicalCrossProductToSingularApp_def (k : Type u) [CommRing k] (X Y : TopCat) : cubicalCrossProductToSingularApp k X Y = CategoryTheory.CategoryStruct.comp (cubicalCrossProduct k X Y) ((cubicalToSingular k).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The cubical cross product followed by the comparison map is a composite.

theorem TauCeti.singularCrossProductOfCubicalApp_def (k : Type u) [CommRing k] (X Y : TopCat) : singularCrossProductOfCubicalApp k X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((cubicalToSingular k).app X) ((cubicalToSingular k).app Y)) (singularCrossProduct k X Y)

The tensor product of the comparison maps followed by the simplicial cross product is a composite.

noncomputable def TauCeti.cubicalCrossProductToSingular (k : Type u) [CommRing k] : cubicalTensor k ⟶ singularChainsProduct k

The cubical cross product followed by the comparison map to simplicial chains, as a natural transformation of functors on pairs of spaces.

@[simp]

theorem TauCeti.cubicalCrossProductToSingular_app (k : Type u) [CommRing k] (X Y : TopCat) : (cubicalCrossProductToSingular k).app (X, Y) = cubicalCrossProductToSingularApp k X Y

The component of cubicalCrossProductToSingular at a pair of spaces.

noncomputable def TauCeti.singularCrossProductOfCubical (k : Type u) [CommRing k] : cubicalTensor k ⟶ singularChainsProduct k

The tensor product of the two comparison maps followed by the simplicial cross product, as a natural transformation of functors on pairs of spaces.

@[simp]

theorem TauCeti.singularCrossProductOfCubical_app (k : Type u) [CommRing k] (X Y : TopCat) : (singularCrossProductOfCubical k).app (X, Y) = singularCrossProductOfCubicalApp k X Y

The component of singularCrossProductOfCubical at a pair of spaces.

theorem TauCeti.singularAugment_cubicalCrossProductToSingular_eq_singularCrossProductOfCubical (k : Type u) [CommRing k] (X : TopCat × TopCat) (x : ↑(((cubicalTensor k).obj X).X 0)) : (singularAugment k (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2)) ((CategoryTheory.ConcreteCategory.hom (((cubicalCrossProductToSingular k).app X).f 0)) x) = (singularAugment k (CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 X.2)) ((CategoryTheory.ConcreteCategory.hom (((singularCrossProductOfCubical k).app X).f 0)) x)

The two natural chain maps from the tensor product of the cubical chains to the singular chains of the product agree after augmentation in degree zero.

noncomputable def TauCeti.cubicalSingularCrossProductHomotopy (k : Type u) [CommRing k] (X Y : TopCat) : Homotopy (cubicalCrossProductToSingularApp k X Y) (singularCrossProductOfCubicalApp k X Y)

The cubical and the simplicial cross product are naturally chain homotopic: the cubical cross product followed by the comparison map and the tensor product of the two comparison maps followed by the simplicial cross product, N(X; k) ⊗ N(Y; k) ⟶ C(X × Y; k), are chain homotopic. The homotopy is natural in both spaces.

theorem TauCeti.cubicalSingularCrossProductHomotopy_hom_naturality (k : Type u) [CommRing k] {X X' Y Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((HomologicalComplex.tensorHom ((normalizedCubicalChainComplex k).map f) ((normalizedCubicalChainComplex k).map g)).f i) ((cubicalSingularCrossProductHomotopy k X' Y').hom i j) = CategoryTheory.CategoryStruct.comp ((cubicalSingularCrossProductHomotopy k X Y).hom i j) (((singularChains k).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)).f j)

The homotopy between the two cross products is natural in both spaces.

theorem TauCeti.homologyMap_cubicalCrossProductToSingularApp_eq_singularCrossProductOfCubicalApp (k : Type u) [CommRing k] (X Y : TopCat) (n : ℕ) : HomologicalComplex.homologyMap (cubicalCrossProductToSingularApp k X Y) n = HomologicalComplex.homologyMap (singularCrossProductOfCubicalApp k X Y) n

The cubical cross product is the simplicial cross product on homology: the cubical cross product followed by the comparison map and the tensor product of the two comparison maps followed by the simplicial cross product induce the same map on homology.