Theorems · Inductive type · category theory

HomologicalComplex

{ι : Type u_1} →
  (V : Type u) →
    [inst : CategoryTheory.Category.{v, u} V] →
      [CategoryTheory.Limits.HasZeroMorphisms V] → ComplexShape ι → Type (max (max u u_1) v)

A HomologicalComplex V c with a "shape" controlled by c : ComplexShape ι has chain groups X i (objects in V) indexed by i : ι, and a differential d i j whenever c.Rel i j. We in fact ask for differentials d i j for all i j : ι, but have a field shape requiring that these are zero when not allowed by c. This avoids a lot of dependent type theory hell! The composite of any two differentials d i j ≫ d j k must be zero.

Defined in

Mathlib.Algebra.Homology.HomologicalComplex

Cited by

1,691 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms