Theorems · Definition · category theory

AlgebraicTopology.normalizedMooreComplex

(C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (ChainComplex C ℕ)

The (normalized) Moore complex of a simplicial object X in an abelian category C. The n-th object is intersection of the kernels of X.δ i : X.obj n ⟶ X.obj (n-1), for i = 1, ..., n. The differentials are induced from X.δ 0, which maps each of these intersections of kernels to the next.

Defined in

Mathlib.AlgebraicTopology.MooreComplex

Cited by

14 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Abelian