Theorems · Theorem · category theory

HomotopyCategory.composableArrowsFunctor_map

∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X Y : CategoryTheory.ComposableArrows (CochainComplex C ℤ) 1}
  (φ : X ⟶ Y),
  (HomotopyCategory.composableArrowsFunctor C).map φ =
    CochainComplex.mappingCone.map
      (X.map' 0 1 HomotopyCategory.composableArrowsFunctor._proof_1 HomotopyCategory.composableArrowsFunctor._proof_2)
      (Y.map' 0 1 HomotopyCategory.composableArrowsFunctor._proof_1 HomotopyCategory.composableArrowsFunctor._proof_2)
      (φ.app 0) (φ.app 1) ⋯

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasBinaryBiproducts