Theorems · Theorem · category theory

Homotopy.comp_nullHomotopicMap

∀ {ι : 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 : C ⟶ D) (hom : (i j : ι) → D.X i ⟶ E.X j),
  CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap hom) =
    Homotopy.nullHomotopicMap fun i j => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j)

Compatibility of nullHomotopicMap with the precomposition by a morphism of complexes.

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