Commit 2025-03-14 12:47 cc796381

refactor(AlgebraicTopology/SimplicialSet): use the Subpresheaf API (#21090) Some new API is introduced for subcomplexes of the standard simplex: any S : Finset (Fin (n + 1)) defines a subcomplex face S of Δ[n], and this face is isomorphic to Δ[m] when Fin (m + 1) ≃o S. Then, boundaries and horns are redefined as subcomplexes of the standard simplex and it is shown that they are unions of certain codimension one faces of the standard simplex.

• depends on: #21543
• depends on: #21540
• depends on: #21542
• depends on: #21303
• depends on: #21047
• depends on: #20840
• depends on: #21096