The simplicial cross product of singular chains with coefficients in a ring

For a commutative ring k, the shuffle map of Eilenberg and Mac Lane (TopCat.shuffle) with coefficients k and k lands in the singular chains with coefficients in k ⊗ k. Composing with the coefficient change along the unitor k ⊗ k ≅ k gives the simplicial cross product C(X; k) ⊗ C(Y; k) ⟶ C(X × Y; k) of singular chains with coefficients in k.

Main definitions and results

• TauCeti.singularCrossProduct: the simplicial cross product.
• TauCeti.singularCrossProduct_naturality: its naturality in both spaces.
• TauCeti.singularAugment_singularCrossProduct: the augmentation of the cross product of the chains of two points with coefficients a and b is a * b.
• TauCeti.quasiIso_singularCrossProduct: the simplicial cross product is a quasi-isomorphism (Eilenberg–Zilber).

References

• S. Eilenberg and S. Mac Lane, On the groups H(Π, n), I, Ann. of Math. 58 (1953).
• S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953).

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

The simplicial cross product of singular chains with coefficients in k, C(X; k) ⊗ C(Y; k) ⟶ C(X × Y; k): the shuffle map with the coefficients k ⊗ k identified with k by the unitor.

theorem TauCeti.singularCrossProduct_def (k : Type u) [CommRing k] (X Y : TopCat) : singularCrossProduct k X Y = CategoryTheory.CategoryStruct.comp (X.shuffle Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k)) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k))) (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat k)).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k))).hom).app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

The simplicial cross product is the shuffle map followed by the coefficient change along the unitor.

theorem TauCeti.singularCrossProduct_naturality (k : Type u) [CommRing k] {X X' Y Y' : TopCat} (f : X ⟶ X') (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((singularChains k).map f) ((singularChains k).map g)) (singularCrossProduct k X' Y') = CategoryTheory.CategoryStruct.comp (singularCrossProduct k X Y) ((singularChains k).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))

The simplicial cross product is natural in both spaces.

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

The simplicial cross product is natural in both spaces.

theorem TauCeti.singularAugment_singularCrossProduct (k : Type u) [CommRing k] (X Y : TopCat) (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := 0 })) (τ : (TopCat.toSSet.obj Y).obj (Opposite.op { len := 0 })) (a b : k) : (singularAugment k (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) ((CategoryTheory.ConcreteCategory.hom ((singularCrossProduct k X Y).f 0)) ((ModuleCat.Hom.hom (HomologicalComplex.ιTensorObj ((singularChains k).obj X) ((singularChains k).obj Y) 0 0 0 ⋯)) (simplexChain σ a ⊗ₜ[k] simplexChain τ b))) = a * b

The augmentation of the simplicial cross product of the chains of two singular points with coefficients a and b is a * b.

instance TauCeti.quasiIso_singularCrossProduct (k : Type u) [CommRing k] (X Y : TopCat) : QuasiIso (singularCrossProduct k X Y)

The simplicial cross product is a quasi-isomorphism: the shuffle map is a homotopy equivalence (Eilenberg–Zilber), and the coefficient change along the unitor is an isomorphism.