Theorems · Definition · category theory

CochainComplex.HomComplex.Cochain.single

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} → {p q : ℤ} → (K.X p ⟶ L.X q) → (n : ℤ) → CochainComplex.HomComplex.Cochain K L n

The cochain in Cochain K L n that is given by a single morphism K.X p ⟶ L.X q and is zero otherwise. (As we do not check that p + n = q, this will be the zero cochain when p + n ≠ q.)

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Cited by

11 results in Mathlib

Foundations

Depth 40 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive