Commit 2026-04-28 07:38 28584a10

feat(AlgebraicTopology): the splitting of a simplicial set (#38544) Let X be a simplicial set. The fact that any simplex x : X _⦋n⦌ can be written in a unique way as X.map f.op y for an epimorphism f : ⦋n⦌ ⟶ ⦋m⦌ and a nondegenerate simplex y : X _⦋m⦌ is translated in this PR as the data of a splitting of X. (The namespace where SimplicialObject.Splitting lies is also fixed.)