Theorems · Definition · category theory

CochainComplex.HomComplex.Cochain.equivHomotopy

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ₁ φ₂ : F ⟶ G) →
          Homotopy φ₁ φ₂ ≃
            { z //
              CochainComplex.HomComplex.Cochain.ofHom φ₁ =
                CochainComplex.HomComplex.δ (-1) 0 z + CochainComplex.HomComplex.Cochain.ofHom φ₂ }

Given two morphisms of complexes φ₁ φ₂ : F ⟶ G, the datum of a homotopy between φ₁ and φ₂ is equivalent to the datum of a 1-cochain z such that δ (-1) 0 z is the difference of the zero cochains associated to φ₂ and φ₁.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Cited by

8 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive