Homotopies on a coproduct of complexes

A family of homotopies on the summands of a coproduct of complexes assembles into a homotopy on the coproduct (Homotopy.sigma): the components are the degreewise descriptions HomologicalComplex.sigmaXDesc of the given components, and the homotopy identity holds after restriction to each summand because the differential of the coproduct commutes with the summand inclusions. This is what makes the quotient functor to the homotopy category preserve coproducts.

Main definitions

• Homotopy.sigma: the assembled homotopy.

noncomputable def Homotopy.sigma {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] {ι : Type u_1} {c : ComplexShape ι} {κ : Type w} [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete κ) C] {X : κ → HomologicalComplex C c} {Y : HomologicalComplex C c} {g g' : ∐ X ⟶ Y} (H : (k : κ) → Homotopy (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X k) g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι X k) g')) : Homotopy g g'

Homotopies on the summands of a coproduct assemble to a homotopy on the coproduct: the components are sigmaXDesc of the components, and the homotopy identity holds after restriction to each summand because the differential of the coproduct commutes with the summand inclusions.

Equations

• Homotopy.sigma H = { hom := fun (i j : ι) => HomologicalComplex.sigmaXDesc (fun (k : κ) => (H k).hom) i j, zero := ⋯, comm := ⋯ }