Documentation

Mathlib.AlgebraicTopology.MooreComplex

Moore complex #

We construct the normalized Moore complex, as a functor SimplicialObject C ⥤ ChainComplex C ℕ, for any 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.

This functor is one direction of the Dold-Kan equivalence, which we're still working towards.

References #

The definitions in this namespace are all auxiliary definitions for NormalizedMooreComplex and should usually only be accessed via that.

The normalized Moore complex in degree n, as a subobject of X n.

Instances For

    The differentials in the normalized Moore complex.

    Instances For
      @[simp]
      theorem AlgebraicTopology.NormalizedMooreComplex.obj_d {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] (X : CategoryTheory.SimplicialObject C) (i : ) (j : ) :

      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.

      Instances For