Theorems · Definition · category theory

ChainComplex

(V : Type u) →
  [inst : CategoryTheory.Category.{v, u} V] →
    [CategoryTheory.Limits.HasZeroMorphisms V] →
      (α : Type u_2) → [AddRightCancelSemigroup α] → [One α] → Type (max (max u_2 u) v)

An α-indexed chain complex is a HomologicalComplex in which d i j ≠ 0 only if j + 1 = i.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

350 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 28 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsAddRightCancelSemigroupOne