Theorems · Theorem · category theory

Homotopy.comp_hom

∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c} {f₁ g₁ : C₁ ⟶ C₂} {f₂ g₂ : C₂ ⟶ C₃} (h₁ : Homotopy f₁ g₁)
  (h₂ : Homotopy f₂ g₂) (i j : ι),
  (h₁.comp h₂).hom i j =
    CategoryTheory.CategoryStruct.comp (h₁.hom i j) (f₂.f j) + CategoryTheory.CategoryStruct.comp (g₁.f i) (h₂.hom i j)

Defined in

Mathlib.Algebra.Homology.Homotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive