Theorems · Theorem · category theory

CochainComplex.mappingCone.ext_from_iff

∀ {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 φ] (i j : ℤ) (hij : j + 1 = i)
  {A : C} (f g : (CochainComplex.mappingCone φ).X j ⟶ A),
  f = g ↔
    CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) f =
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) g ∧
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) f =
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) g

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveHomologicalComplex.HasHomotopyCofiber