Theorems · Definition · category theory

CochainComplex.mappingCone.descHomotopy

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {K : CochainComplex C ℤ} →
              (f₁ f₂ : CochainComplex.mappingCone φ ⟶ K) →
                (γ₁ : CochainComplex.HomComplex.Cochain F K (-2)) →
                  (γ₂ : CochainComplex.HomComplex.Cochain G K (-1)) →
                    (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₁) ⋯ =
                        CochainComplex.HomComplex.δ (-2) (-1) γ₁ +
                            (CochainComplex.HomComplex.Cochain.ofHom φ).comp γ₂ ⋯ +
                          (CochainComplex.mappingCone.inl φ).comp (CochainComplex.HomComplex.Cochain.ofHom f₂) ⋯ →
                      CochainComplex.HomComplex.Cochain.ofHom
                            (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₁) =
                          CochainComplex.HomComplex.δ (-1) 0 γ₂ +
                            CochainComplex.HomComplex.Cochain.ofHom
                              (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.inr φ) f₂) →
                        Homotopy f₁ f₂

Constructor for homotopies between morphisms from a mapping cone.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Cited by

0 results in Mathlib

Foundations

Depth 62 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveHomologicalComplex.HasHomotopyCofiber