Theorems · Definition · category theory

CochainComplex.mappingCone.desc

{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 ℤ} →
              (α : CochainComplex.HomComplex.Cochain F K (-1)) →
                (β : G ⟶ K) →
                  CochainComplex.HomComplex.δ (-1) 0 α =
                      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β) →
                    (CochainComplex.mappingCone φ ⟶ K)

Given φ : F ⟶ G, this is the morphism mappingCone φ ⟶ K that is constructed from a cochain α : Cochain F K (-1) and a morphism β : G ⟶ K such that δ (-1) 0 α = Cochain.ofHom (φ ≫ β).

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Cited by

19 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveHomologicalComplex.HasHomotopyCofiber