Theorems · Theorem · category theory

CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ₁ φ₂ : F ⟶ G)
  (z :
    { z //
      CochainComplex.HomComplex.Cochain.ofHom φ₁ =
        CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ })
  (i j : ℤ),
  ((CochainComplex.HomComplex.Cochain.equivHomotopy φ₁ φ₂).symm z).hom i j =
    if hij : i + -1 = j then (↑z).v i j hij else 0

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive