Documentation

Mathlib.AlgebraicTopology.DoldKan.Notations

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.)

The alternating face map complex, on objects

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

    The normalized Moore complex functor, on objects.

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