mathlib
df967907 - feat(algebraic_topology): split simplicial objects (#16072)

Commit
3 years ago
feat(algebraic_topology): split simplicial objects (#16072) This PR introduces the notion of split simplicial objects. Future PRs will show that simplicial sets are split (in a unique way). It will also be a consequence of the Dold-Kan correspondence that in (pseudo-)abelian categories, all simplicial objects have at least a splitting. Split simplicial objects will be used in the proof of the Dold-Kan correspondence.
Author
Parents
Loading