Notations for the Dold-Kan equivalence

This file defines the notation K[X] : ChainComplex C ℕ for the alternating face map complex of (X : SimplicialObject C) where C is a preadditive category, as well as N[X] for the normalized subcomplex in the case C is an abelian category.

(See Equivalence.lean for the general strategy of proof of the Dold-Kan equivalence.)

def DoldKan.«termK[_]» : Lean.ParserDescr

The alternating face map complex, on objects

Equations

• One or more equations did not get rendered due to their size.

def DoldKan.«termN[_]» : Lean.ParserDescr

The normalized Moore complex functor, on objects.

Equations

• One or more equations did not get rendered due to their size.