Theorems · Theorem · category theory

Homotopy.compLeft_hom

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

Defined in

Mathlib.Algebra.Homology.Homotopy

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive