The cubical cross product as a chain map

The cross product of normalized cubical chains (TauCeti.NormalizedCubicalChain.crossProduct) is bilinear and satisfies the Leibniz rule, so it assembles into a chain map out of the tensor product of the normalized cubical chain complexes, N(X) ⊗ N(Y) ⟶ N(X × Y), natural in both spaces.

The tensor product of chain complexes is Mathlib's, with the differential d (a ⊗ b) = d a ⊗ b + (-1) ^ p • (a ⊗ d b) on a summand of bidegree (p, q). The cross product is a map on each summand, followed by the reindexing p + q = n.

Main definitions and results

• TauCeti.cubicalCrossProduct R X Y: the cross product as a chain map N(X) ⊗ N(Y) ⟶ N(X ⊗ Y).
• TauCeti.cubicalCrossProduct_naturality: naturality in both spaces.

noncomputable def TauCeti.cubicalCrossProductSummand (R : Type u) [CommRing R] (X Y : TopCat) (p q n : ℕ) (h : p + q = n) : CategoryTheory.MonoidalCategoryStruct.tensorObj ↧(NormalizedCubicalChain (↑X) R p) ↧(NormalizedCubicalChain (↑Y) R q) ⟶ ↧(NormalizedCubicalChain (↑X × ↑Y) R n)

The cross product of normalized chains of degrees p and q, as a map out of the tensor product of modules to the chains of degree n = p + q of the product space.

@[simp]

theorem TauCeti.cubicalCrossProductSummand_apply (R : Type u) [CommRing R] (X Y : TopCat) (p q n : ℕ) (h : p + q = n) (a : NormalizedCubicalChain (↑X) R p) (b : NormalizedCubicalChain (↑Y) R q) : (ModuleCat.Hom.hom (cubicalCrossProductSummand R X Y p q n h)) (a ⊗ₜ[R] b) = (NormalizedCubicalChain.cast R h) (((NormalizedCubicalChain.crossProduct (↑X) (↑Y) R p q) a) b)

The cross product map of a summand, evaluated on a pure tensor a ⊗ b of normalized chains of degrees p and q, is their cross product reindexed along p + q = n.

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

The cross product of normalized cubical chains as a chain map N(X) ⊗ N(Y) ⟶ N(X ⊗ Y), with the Koszul sign on the tensor product of complexes: it sends a ⊗ b of bidegree (p, q) to a × b, and the Leibniz rule says it commutes with the differentials. It is the cubical counterpart of the shuffle map TopCat.shuffle.

@[simp]

theorem TauCeti.ι_cubicalCrossProduct_f {R : Type u} [CommRing R] {X Y : TopCat} {p q n : ℕ} (h : p + q = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex R).obj X) ((normalizedCubicalChainComplex R).obj Y) p q n h) ((cubicalCrossProduct R X Y).f n) = cubicalCrossProductSummand R X Y p q n h

On a summand of bidegree (p, q), the cross product chain map is the cross product of normalized chains followed by the reindexing p + q = n.

@[simp]

theorem TauCeti.ι_cubicalCrossProduct_f_assoc {R : Type u} [CommRing R] {X Y : TopCat} {p q n : ℕ} (h : p + q = n) {Z : ModuleCat R} (h✝ : ((normalizedCubicalChainComplex R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((normalizedCubicalChainComplex R).obj X) ((normalizedCubicalChainComplex R).obj Y) p q n h) (CategoryTheory.CategoryStruct.comp ((cubicalCrossProduct R X Y).f n) h✝) = CategoryTheory.CategoryStruct.comp (cubicalCrossProductSummand R X Y p q n h) h✝

On a summand of bidegree (p, q), the cross product chain map is the cross product of normalized chains followed by the reindexing p + q = n.

theorem TauCeti.cubicalCrossProduct_naturality {R : Type u} [CommRing R] {X X' Y Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((normalizedCubicalChainComplex R).map f) ((normalizedCubicalChainComplex R).map g)) (cubicalCrossProduct R X' Y') = CategoryTheory.CategoryStruct.comp (cubicalCrossProduct R X Y) ((normalizedCubicalChainComplex R).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))

Naturality of the cross product chain map in both spaces.

theorem TauCeti.cubicalCrossProduct_naturality_assoc {R : Type u} [CommRing R] {X X' Y Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') {Z : ChainComplex (ModuleCat R) ℕ} (h : (normalizedCubicalChainComplex R).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X' Y') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((normalizedCubicalChainComplex R).map f) ((normalizedCubicalChainComplex R).map g)) (CategoryTheory.CategoryStruct.comp (cubicalCrossProduct R X' Y') h) = CategoryTheory.CategoryStruct.comp (cubicalCrossProduct R X Y) (CategoryTheory.CategoryStruct.comp ((normalizedCubicalChainComplex R).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)) h)

Naturality of the cross product chain map in both spaces.