The Eilenberg–Zilber theorem for singular chains

For topological spaces X and Y, the Alexander–Whitney map C(X × Y; R ⊗ S) ⟶ C(X; R) ⊗ C(Y; S) on singular chains is a chain homotopy equivalence with homotopy inverse the shuffle map (TopCat.eilenbergZilberHomotopyEquiv).

The composite shuffle ∘ AW is the simplicial composite for Sing X and Sing Y, conjugated by the canonical isomorphism Sing (X × Y) ≅ Sing X × Sing Y (TopCat.alexanderWhitney_shuffle), so its homotopy to the identity (TopCat.alexanderWhitneyShuffleHomotopy) is the simplicial one, SSet.alexanderWhitneyShuffleHomotopy, transported along this isomorphism. The composite AW ∘ shuffle is the simplicial composite itself (TopCat.shuffle_alexanderWhitney), so its homotopy to the identity (TopCat.shuffleAlexanderWhitneyHomotopy) is SSet.shuffleAlexanderWhitneyHomotopy.

References

• S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953).

noncomputable def TopCat.alexanderWhitneyShuffleHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive 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) : Homotopy (CategoryTheory.CategoryStruct.comp (X.alexanderWhitney Y R S) (X.shuffle Y R S)) (CategoryTheory.CategoryStruct.id ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)))

The Eilenberg–Zilber homotopy on singular chains: the Alexander–Whitney map C(X × Y; R ⊗ S) ⟶ C(X; R) ⊗ C(Y; S) followed by the shuffle map is chain homotopic to the identity of C(X × Y; R ⊗ S).

Equations

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

noncomputable def TopCat.shuffleAlexanderWhitneyHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive 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) : Homotopy (CategoryTheory.CategoryStruct.comp (X.shuffle Y R S) (X.alexanderWhitney Y R S)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S)))

The Eilenberg–Zilber homotopy on singular chains: the shuffle map C(X; R) ⊗ C(Y; S) ⟶ C(X × Y; R ⊗ S) followed by the Alexander–Whitney map is chain homotopic to the identity of C(X; R) ⊗ C(Y; S).

Equations

• X.shuffleAlexanderWhitneyHomotopy Y R S = (Homotopy.ofEq ⋯).trans ((TopCat.toSSet.obj X).shuffleAlexanderWhitneyHomotopy (TopCat.toSSet.obj Y) R S)

noncomputable def TopCat.eilenbergZilberHomotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive 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) : HomotopyEquiv ((toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (CategoryTheory.MonoidalCategoryStruct.tensorObj ((toSSet.obj X).chainComplex R) ((toSSet.obj Y).chainComplex S))

The Eilenberg–Zilber theorem for singular chains: the Alexander–Whitney map C(X × Y; R ⊗ S) ⟶ C(X; R) ⊗ C(Y; S) is a chain homotopy equivalence, with homotopy inverse the shuffle map.

Equations

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

@[simp]

theorem TopCat.eilenbergZilberHomotopyEquiv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive 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) : (X.eilenbergZilberHomotopyEquiv Y R S).hom = X.alexanderWhitney Y R S

@[simp]

theorem TopCat.eilenbergZilberHomotopyEquiv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive 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) : (X.eilenbergZilberHomotopyEquiv Y R S).inv = X.shuffle Y R S