Commit 2025-10-28 15:18 f482e48e

View on Github →

refactor(AlgebraicTopology): redefine the topological simplex using the convexity API (#28893) Before this PR, the n-dimensional topological simplex (in the AlgebraicTopology hierarchy) was defined as a subtype of Fin (n + 1) → ℝ≥0, which did not interact well with the convexity API which assumes the ambient type is a vector space. In this PR, we redefine the topological simplex functor (as a cosimplicial object in TopCat) using the already existing stdSimplex from Analysis.Convex.

Estimated changes

Modified Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean

added theorem SimplexCategory.concreteCategoryHom_id

Modified Mathlib/AlgebraicTopology/SingularSet.lean

deleted def TopCat.toSSetObjEquiv

Modified Mathlib/AlgebraicTopology/TopologicalSimplex.lean

deleted theorem SimplexCategory.coe_toTopMap

deleted theorem SimplexCategory.continuous_toTopMap

deleted def SimplexCategory.toTop

deleted def SimplexCategory.toTopMap

deleted theorem SimplexCategory.toTopObj.ext

deleted def SimplexCategory.toTopObj

deleted def SimplexCategory.toTopObjOneHomeo

deleted theorem SimplexCategory.toTopObj_one_add_eq_one

deleted theorem SimplexCategory.toTopObj_one_coe_add_coe_eq_one

deleted theorem SimplexCategory.toTopObj_zero_apply_zero

deleted def SimplexCategory.toTop₀

Modified Mathlib/Analysis/Convex/StdSimplex.lean

added theorem isPathConnected_stdSimplex

added theorem stdSimplex.add_eq_one

added theorem stdSimplex.eq_one_of_unique

added theorem stdSimplex.vertex_injective