Theorems · Theorem · category theory

Homotopy.nullHomotopicMap_f

∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {k₂ k₁ k₀ : ι},
  c.Rel k₂ k₁ →
    c.Rel k₁ k₀ →
      ∀ (hom : (i j : ι) → C.X i ⟶ D.X j),
        (Homotopy.nullHomotopicMap hom).f k₁ =
          CategoryTheory.CategoryStruct.comp (C.d k₁ k₀) (hom k₀ k₁) +
            CategoryTheory.CategoryStruct.comp (hom k₁ k₂) (D.d k₂ k₁)

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