Simplicial homotopies induce chain homotopies

Given a simplicial homotopy between morphisms of simplicial objects in a preadditive category, we construct a chain homotopy between the induced morphisms on the alternating face map complexes.

Concretely, if H : Homotopy f g gives maps H.h i : X _⦋n⦌ ⟶ Y _⦋n+1⦌ indexed by i : Fin (n + 1), we define the degree-n component of the chain homotopy as the opposite of alternating sum ∑ i, (-1)^i • H.h i.

noncomputable def CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) (p q : ℕ) : X.obj (Opposite.op (SimplexCategory.mk p)) ⟶ Y.obj (Opposite.op (SimplexCategory.mk q))

The family of components of the induced chain homotopy

Equations

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

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) (p : ℕ) : hom H p (p + 1) = -∑ k : Fin (p + 1), (-1) ^ ↑k • H.h k

@[simp]

theorem CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom_eq_zero {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) (p q : ℕ) (hpq : p + 1 ≠ q) : hom H p q = 0

noncomputable def CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : SimplicialObject C} {f g : X ⟶ Y} (H : Homotopy f g) : _root_.Homotopy ((AlgebraicTopology.alternatingFaceMapComplex C).map f) ((AlgebraicTopology.alternatingFaceMapComplex C).map g)

A simplicial homotopy between f and g induces a chain homotopy between the induced morphisms on the alternating face map complexes.

Equations

• H.toChainHomotopy = { hom := CategoryTheory.SimplicialObject.Homotopy.ToChainHomotopy.hom H, zero := ⋯, comm := ⋯ }

theorem CategoryTheory.SimplicialObject.Homotopy.map_homology_eq {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : SimplicialObject C} {f g : X ⟶ Y} [CategoryWithHomology C] (H : Homotopy f g) (n : ℕ) : (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map ((AlgebraicTopology.alternatingFaceMapComplex C).map f) = (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n).map ((AlgebraicTopology.alternatingFaceMapComplex C).map g)