The Eilenberg–Zilber theorem

For simplicial sets K and L, the Alexander–Whitney map C(K × L; R ⊗ S) ⟶ C(K; R) ⊗ C(L; S) and the shuffle map back are mutually inverse chain homotopy equivalences (SSet.eilenbergZilberHomotopyEquiv). Neither composite is the identity on unnormalized chains. Already for a 1-simplex x of K and a vertex y of L, the Alexander–Whitney map followed by the shuffle map sends the summand of the 1-simplex (x, s₀ y) of K × L to itself plus the summand of the degenerate 1-simplex (s₀ x₀, s₀ y), where x₀ is the initial vertex of x. Both homotopies come from the method of acyclic models.

For shuffle ∘ AW ≃ id (SSet.alexanderWhitneyShuffleHomotopy) the statement used is SSet.prodChainComplexHomotopy. Let φ and ψ be families of chain maps C(K × L; T) ⟶ C(K × L; T'), natural in maps K ⟶ K' and L ⟶ L', which agree in degree zero. Then φ and ψ are chain homotopic, through a homotopy natural in K and L (SSet.prodChainComplexHomotopy_hom_naturality). An n-simplex (x, y) of K × L is the image of the diagonal n-simplex of the model Δ[n] × Δ[n] under the map classifying (x, y), so by naturality the homotopy is determined by its values on these diagonal simplices. These values are built by induction on n: the chain that the homotopy must bound on the model is a cycle by the inductive hypothesis, and the cone from the vertex (0, 0) of Δ[n] × Δ[n] (SSet.stdSimplex.prodConeChain) bounds it, because this cone is a contracting homotopy in positive degrees.

For AW ∘ shuffle ≃ id (SSet.shuffleAlexanderWhitneyHomotopy) the statement used is the same one for families of chain maps C(K; R) ⊗ C(L; S) ⟶ C(K; R') ⊗ C(L; S') (SSet.tensorChainComplexHomotopy). Here the summand of a p-simplex x of K and a q-simplex y of L is the image of the summand of the pair of top simplices of the models Δ[p] and Δ[q], so there is one model for each bidegree. The bounding chains on the models come from the contracting homotopy c ⊗ 1 + e ⊗ c of C(Δ[p]; R') ⊗ C(Δ[q]; S') in positive degrees (SSet.stdSimplex.tensorConeChain). Here c is the cone from the vertex 0 on either factor (SSet.stdSimplex.coneChain), and e collapses the vertices of Δ[p] onto the vertex 0 (SSet.stdSimplex.constZeroChain).

Main definitions and results

• SSet.prodChainComplexHomotopy: two natural families of chain maps on the simplicial chains of products which agree in degree zero are chain homotopic.
• SSet.prodChainComplexHomotopy_hom_naturality: the homotopy is natural in both simplicial sets.
• SSet.alexanderWhitney_shuffle_f_zero: the Alexander–Whitney map followed by the shuffle map is the identity in degree zero.
• SSet.alexanderWhitneyShuffleHomotopy: the Alexander–Whitney map followed by the shuffle map is chain homotopic to the identity.
• SSet.stdSimplex.tensorConeChain: the contracting homotopy of C(Δ[a]; R) ⊗ C(Δ[b]; S) in positive degrees, with SSet.stdSimplex.tensorConeChain_d its boundary formula.
• SSet.tensorChainComplexHomotopy: two natural families of chain maps on tensor products of simplicial chains which agree in degree zero are chain homotopic, and SSet.tensorChainComplexHomotopy_hom_naturality: the homotopy is natural.
• SSet.shuffle_alexanderWhitney_f_zero: the shuffle map followed by the Alexander–Whitney map is the identity in degree zero.
• SSet.shuffleAlexanderWhitneyHomotopy: the shuffle map followed by the Alexander–Whitney map is chain homotopic to the identity.
• SSet.eilenbergZilberHomotopyEquiv: the Alexander–Whitney map is a chain homotopy equivalence with homotopy inverse the shuffle map.

References

• S. Eilenberg and J. A. Zilber, On products of complexes, Amer. J. Math. 75 (1953).
• S. Eilenberg and S. Mac Lane, Acyclic models, Amer. J. Math. 75 (1953).
• C. Weibel, An Introduction to Homological Algebra, Sections 8.5 and 8.6.

noncomputable def SSet.prodChainComplexHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {T T' : C} (φ ψ : (K L : SSet) → (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex T ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex T') (hφ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T) (φ K' L') = CategoryTheory.CategoryStruct.comp (φ K L) (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T')) (hψ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T) (ψ K' L') = CategoryTheory.CategoryStruct.comp (ψ K L) (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T')) (h₀ : ∀ (K L : SSet), (φ K L).f 0 = (ψ K L).f 0) (K L : SSet) : Homotopy (φ K L) (ψ K L)

Acyclic models for products of simplicial sets. Two families φ and ψ of chain maps C(K × L; T) ⟶ C(K × L; T') on the simplicial chains of products, natural in both simplicial sets and equal in degree zero, are chain homotopic. The homotopy is natural in K and L (SSet.prodChainComplexHomotopy_hom_naturality).

Equations

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

theorem SSet.prodChainComplexHomotopy_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {T T' : C} (φ ψ : (K L : SSet) → (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex T ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex T') (hφ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T) (φ K' L') = CategoryTheory.CategoryStruct.comp (φ K L) (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T')) (hψ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T) (ψ K' L') = CategoryTheory.CategoryStruct.comp (ψ K L) (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T')) (h₀ : ∀ (K L : SSet), (φ K L).f 0 = (ψ K L).f 0) {K K' L L' : SSet} (f : K ⟶ K') (g : L ⟶ L') (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T).f i) ((prodChainComplexHomotopy φ ψ hφ hψ h₀ K' L').hom i j) = CategoryTheory.CategoryStruct.comp ((prodChainComplexHomotopy φ ψ hφ hψ h₀ K L).hom i j) ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T').f j)

The homotopy of SSet.prodChainComplexHomotopy is natural in both simplicial sets.

theorem SSet.prodChainComplexHomotopy_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {T T' : C} (φ ψ : (K L : SSet) → (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex T ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex T') (hφ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T) (φ K' L') = CategoryTheory.CategoryStruct.comp (φ K L) (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T')) (hψ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T) (ψ K' L') = CategoryTheory.CategoryStruct.comp (ψ K L) (chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T')) (h₀ : ∀ (K L : SSet), (φ K L).f 0 = (ψ K L).f 0) {K K' L L' : SSet} (f : K ⟶ K') (g : L ⟶ L') (i j : ℕ) {Z : C} (h : ((CategoryTheory.MonoidalCategoryStruct.tensorObj K' L').chainComplex T').X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T).f i) (CategoryTheory.CategoryStruct.comp ((prodChainComplexHomotopy φ ψ hφ hψ h₀ K' L').hom i j) h) = CategoryTheory.CategoryStruct.comp ((prodChainComplexHomotopy φ ψ hφ hψ h₀ K L).hom i j) (CategoryTheory.CategoryStruct.comp ((chainComplexMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) T').f j) h)

The homotopy of SSet.prodChainComplexHomotopy is natural in both simplicial sets.

@[simp]

theorem SSet.alexanderWhitney_shuffle_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : CategoryTheory.CategoryStruct.comp ((K.alexanderWhitney L R S).f 0) ((K.shuffle L R S).f 0) = CategoryTheory.CategoryStruct.id (((CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).X 0)

In degree zero, the Alexander–Whitney map followed by the shuffle map is the identity: both maps send the summand of a vertex (x, y) to the summand of x tensored with that of y, and back.

@[simp]

theorem SSet.alexanderWhitney_shuffle_f_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) {Z : C} (h : ((CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.alexanderWhitney L R S).f 0) (CategoryTheory.CategoryStruct.comp ((K.shuffle L R S).f 0) h) = h

In degree zero, the Alexander–Whitney map followed by the shuffle map is the identity: both maps send the summand of a vertex (x, y) to the summand of x tensored with that of y, and back.

noncomputable def SSet.alexanderWhitneyShuffleHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : Homotopy (CategoryTheory.CategoryStruct.comp (K.alexanderWhitney L R S) (K.shuffle L R S)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)))

The Eilenberg–Zilber homotopy shuffle ∘ AW ≃ id: the Alexander–Whitney map C(K × L; R ⊗ S) ⟶ C(K; R) ⊗ C(L; S) followed by the shuffle map is chain homotopic to the identity of C(K × L; R ⊗ S). The homotopy is the one given by acyclic models, SSet.prodChainComplexHomotopy, and so is natural in K and L.

Equations

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

noncomputable def SSet.stdSimplex.tensorConeChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (a b : ℕ) (R S : C) (n : ℕ) : (CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).X n ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).X (n + 1)

The cone on the tensor product C(Δ[a]; R) ⊗ C(Δ[b]; S), as a map raising the degree by one: c ⊗ 1 + e ⊗ c, where c is the cone from the vertex 0 on either factor (SSet.stdSimplex.coneChain) and e collapses the 0-chains of Δ[a] onto the vertex 0 (SSet.stdSimplex.constZeroChain). It is a contracting homotopy in positive degrees (SSet.stdSimplex.tensorConeChain_d).

Equations

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

theorem SSet.stdSimplex.ι_tensorConeChain_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (a b : ℕ) (R S : C) (s n : ℕ) (h : 0 + s = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) 0 s n h) (tensorConeChain a b R S n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (coneChain a R 0) (((stdSimplex.obj { len := b }).chainComplex S).X s)) (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) 1 s (n + 1) ⋯) + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (constZeroChain a R) (coneChain b S s)) (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) 0 (s + 1) (n + 1) ⋯)

On a summand of bidegree (0, s), the cone on C(Δ[a]; R) ⊗ C(Δ[b]; S) is c ⊗ 1 + e ⊗ c.

theorem SSet.stdSimplex.ι_tensorConeChain_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (a b : ℕ) (R S : C) (s n : ℕ) (h : 0 + s = n) {Z : C} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) 0 s n h) (CategoryTheory.CategoryStruct.comp (tensorConeChain a b R S n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (coneChain a R 0) (((stdSimplex.obj { len := b }).chainComplex S).X s)) (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) 1 s (n + 1) ⋯) + CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (constZeroChain a R) (coneChain b S s)) (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) 0 (s + 1) (n + 1) ⋯)) h✝

On a summand of bidegree (0, s), the cone on C(Δ[a]; R) ⊗ C(Δ[b]; S) is c ⊗ 1 + e ⊗ c.

theorem SSet.stdSimplex.ι_tensorConeChain_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (a b : ℕ) (R S : C) (r s n : ℕ) (h : r + 1 + s = n) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) (r + 1) s n h) (tensorConeChain a b R S n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (coneChain a R (r + 1)) (((stdSimplex.obj { len := b }).chainComplex S).X s)) (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) (r + 1 + 1) s (n + 1) ⋯)

On a summand of bidegree (r + 1, s), the cone on C(Δ[a]; R) ⊗ C(Δ[b]; S) is the cone on the first factor.

theorem SSet.stdSimplex.ι_tensorConeChain_succ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (a b : ℕ) (R S : C) (r s n : ℕ) (h : r + 1 + s = n) {Z : C} (h✝ : (CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).X (n + 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) (r + 1) s n h) (CategoryTheory.CategoryStruct.comp (tensorConeChain a b R S n) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (coneChain a R (r + 1)) (((stdSimplex.obj { len := b }).chainComplex S).X s)) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.ιTensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S) (r + 1 + 1) s (n + 1) ⋯) h✝)

On a summand of bidegree (r + 1, s), the cone on C(Δ[a]; R) ⊗ C(Δ[b]; S) is the cone on the first factor.

theorem SSet.stdSimplex.tensorConeChain_d {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (a b : ℕ) (R S : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (tensorConeChain a b R S (n + 1)) ((CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).d (n + 1 + 1) (n + 1)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).X (n + 1)) - CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj ((stdSimplex.obj { len := a }).chainComplex R) ((stdSimplex.obj { len := b }).chainComplex S)).d (n + 1) n) (tensorConeChain a b R S n)

The cone on C(Δ[a]; R) ⊗ C(Δ[b]; S) is a contracting homotopy in positive degrees: ∂ (c ∘ σ) = σ - c ∘ ∂ σ for a chain σ of positive degree. On a summand u ⊗ v this combines the boundary formulas of the cones on the two factors with the Koszul sign rule.

noncomputable def SSet.tensorChainComplexHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] {R S R' S' : C} (φ ψ : (K L : SSet) → CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R') (L.chainComplex S')) (hφ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)) (φ K' L') = CategoryTheory.CategoryStruct.comp (φ K L) (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S'))) (hψ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)) (ψ K' L') = CategoryTheory.CategoryStruct.comp (ψ K L) (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S'))) (h₀ : ∀ (K L : SSet), (φ K L).f 0 = (ψ K L).f 0) (K L : SSet) : Homotopy (φ K L) (ψ K L)

Acyclic models for tensor products of simplicial chains. Two families φ and ψ of chain maps C(K; R) ⊗ C(L; S) ⟶ C(K; R') ⊗ C(L; S'), natural in both simplicial sets and equal in degree zero, are chain homotopic. The homotopy is natural in K and L (SSet.tensorChainComplexHomotopy_hom_naturality).

Equations

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

theorem SSet.tensorChainComplexHomotopy_hom_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] {R S R' S' : C} (φ ψ : (K L : SSet) → CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R') (L.chainComplex S')) (hφ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)) (φ K' L') = CategoryTheory.CategoryStruct.comp (φ K L) (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S'))) (hψ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)) (ψ K' L') = CategoryTheory.CategoryStruct.comp (ψ K L) (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S'))) (h₀ : ∀ (K L : SSet), (φ K L).f 0 = (ψ K L).f 0) {K K' L L' : SSet} (f : K ⟶ K') (g : L ⟶ L') (i j : ℕ) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)).f i) ((tensorChainComplexHomotopy φ ψ hφ hψ h₀ K' L').hom i j) = CategoryTheory.CategoryStruct.comp ((tensorChainComplexHomotopy φ ψ hφ hψ h₀ K L).hom i j) ((CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S')).f j)

The homotopy of SSet.tensorChainComplexHomotopy is natural in both simplicial sets.

theorem SSet.tensorChainComplexHomotopy_hom_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] {R S R' S' : C} (φ ψ : (K L : SSet) → CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R') (L.chainComplex S')) (hφ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)) (φ K' L') = CategoryTheory.CategoryStruct.comp (φ K L) (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S'))) (hψ : ∀ ⦃K K' L L' : SSet⦄ (f : K ⟶ K') (g : L ⟶ L'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)) (ψ K' L') = CategoryTheory.CategoryStruct.comp (ψ K L) (CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S'))) (h₀ : ∀ (K L : SSet), (φ K L).f 0 = (ψ K L).f 0) {K K' L L' : SSet} (f : K ⟶ K') (g : L ⟶ L') (i j : ℕ) {Z : C} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj (K'.chainComplex R') (L'.chainComplex S')).X j ⟶ Z) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R) (chainComplexMap g S)).f i) (CategoryTheory.CategoryStruct.comp ((tensorChainComplexHomotopy φ ψ hφ hψ h₀ K' L').hom i j) h) = CategoryTheory.CategoryStruct.comp ((tensorChainComplexHomotopy φ ψ hφ hψ h₀ K L).hom i j) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorHom (chainComplexMap f R') (chainComplexMap g S')).f j) h)

The homotopy of SSet.tensorChainComplexHomotopy is natural in both simplicial sets.

@[simp]

theorem SSet.shuffle_alexanderWhitney_f_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : CategoryTheory.CategoryStruct.comp ((K.shuffle L R S).f 0) ((K.alexanderWhitney L R S).f 0) = CategoryTheory.CategoryStruct.id ((CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S)).X 0)

In degree zero, the shuffle map followed by the Alexander–Whitney map is the identity: both maps send the summand of a pair of vertices (x, y) to the summand of the vertex (x, y) and back.

@[simp]

theorem SSet.shuffle_alexanderWhitney_f_zero_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) {Z : C} (h : (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S)).X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp ((K.shuffle L R S).f 0) (CategoryTheory.CategoryStruct.comp ((K.alexanderWhitney L R S).f 0) h) = h

In degree zero, the shuffle map followed by the Alexander–Whitney map is the identity: both maps send the summand of a pair of vertices (x, y) to the summand of the vertex (x, y) and back.

noncomputable def SSet.shuffleAlexanderWhitneyHomotopy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : Homotopy (CategoryTheory.CategoryStruct.comp (K.shuffle L R S) (K.alexanderWhitney L R S)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S)))

The Eilenberg–Zilber homotopy AW ∘ shuffle ≃ id: the shuffle map C(K; R) ⊗ C(L; S) ⟶ C(K × L; R ⊗ S) followed by the Alexander–Whitney map is chain homotopic to the identity of C(K; R) ⊗ C(L; S). The homotopy is the one given by acyclic models, SSet.tensorChainComplexHomotopy, and so is natural in K and L.

Equations

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

noncomputable def SSet.eilenbergZilberHomotopyEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : HomotopyEquiv ((CategoryTheory.MonoidalCategoryStruct.tensorObj K L).chainComplex (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) (CategoryTheory.MonoidalCategoryStruct.tensorObj (K.chainComplex R) (L.chainComplex S))

The Eilenberg–Zilber theorem: the Alexander–Whitney map C(K × L; R ⊗ S) ⟶ C(K; R) ⊗ C(L; 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 SSet.eilenbergZilberHomotopyEquiv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : (K.eilenbergZilberHomotopyEquiv L R S).hom = K.alexanderWhitney L R S

@[simp]

theorem SSet.eilenbergZilberHomotopyEquiv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorLeft X)] [∀ (X : C) (J : Type w), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.MonoidalCategory.tensorRight X)] (K L : SSet) (R S : C) : (K.eilenbergZilberHomotopyEquiv L R S).inv = K.shuffle L R S