Theorems · Definition · category theory

CochainComplex.mappingCone.lift

{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.Cocycle K F 1) →
                (β : CochainComplex.HomComplex.Cochain K G 0) →
                  CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0 →
                    (K ⟶ CochainComplex.mappingCone φ)

Given φ : F ⟶ G, this is the morphism K ⟶ mappingCone φ that is constructed from a cocycle α : Cochain K F 1 and a cochain β : Cochain K G 0 when a suitable cocycle relation is satisfied.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Cited by

12 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveHomologicalComplex.HasHomotopyCofiber