Commit 2025-01-24 19:52 a7e69b0a

View on Github →

chore(AlgebraicTopology): split SimplicialSet.Basic (#21025) This PR only splits the file AlgebraicTopology.SimplicialSet.Basic by creating three new files StdSimplex, Boundary, Horn. This prepares for a refactor and future developments of API for these simplicial sets. For example, the boundary and the horn should be redefined (keeping the defeq) as subcomplexes of the standard simplex using the Subpresheaf API, see #20840.

Estimated changes

deleted def SSet.asOrderHom
deleted def SSet.boundary
deleted def SSet.horn.const
deleted def SSet.horn.edge
deleted def SSet.horn.edge₃
deleted def SSet.horn.face
deleted theorem SSet.horn.hom_ext
deleted def SSet.horn
deleted def SSet.hornInclusion
deleted def SSet.stdSimplex.id
deleted theorem SSet.stdSimplex.map_apply
deleted theorem SSet.stdSimplex.map_id
deleted def SSet.stdSimplex
deleted def SSet.yonedaEquiv
added def SSet.boundary
added def SSet.horn.const
added def SSet.horn.edge
added def SSet.horn.face
added theorem SSet.horn.hom_ext
added def SSet.horn
added def SSet.asOrderHom
added theorem SSet.stdSimplex.map_id
added def SSet.stdSimplex
added def SSet.yonedaEquiv