Theorems · Theorem · category theory

CochainComplex.mappingCone.map_comp

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (φ₃ : K₃ ⟶ L₃) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) (a' : K₂ ⟶ K₃)
  (b' : L₂ ⟶ L₃) (comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃),
  CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a')
      (CategoryTheory.CategoryStruct.comp b b') ⋯ =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
      (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm')

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasBinaryBiproducts