Theorems · Definition · category theory

CochainComplex.HomComplex.Cochain

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → CochainComplex C ℤ → CochainComplex C ℤ → ℤ → Type v

A cochain of degree n : ℤ between two cochain complexes F and G consists of a family of morphisms F.X p ⟶ G.X q whenever p + n = q, i.e. for all triplets in HomComplex.Triplet n.

Defined in

Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Cited by

341 results in Mathlib

Foundations

Depth 38 from the axioms, rests on 499 definitions · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive