mathlib documentation

algebraic_topology.dold_kan.notations

Notations for the Dold-Kan equivalence #

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