Commit 2026-03-26 10:27 4b77bd7b

View on Github →

feat(AlgebraicTopology): API for the geometric realization of simplicial sets (#37099)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

added theorem SSet.stdSimplex.δ_one_eq_const

added theorem SSet.stdSimplex.δ_zero_eq_const

added theorem SSet.yonedaEquiv_const

added theorem SSet.yonedaEquiv_symm_comp

added theorem SSet.yonedaEquiv_symm_zero

Created Mathlib/AlgebraicTopology/SimplicialSet/TopAdj.lean

added theorem SSet.stdSimplex.toSSetObj_app_const_one

added theorem SSet.stdSimplex.toSSetObj_app_const_zero

added theorem SSet.stdSimplex.δ_one_toSSetObjI

added theorem SSet.stdSimplex.δ_zero_toSSetObjI

added theorem SSet.stdSimplex.ι₀_whiskerLeft_toSSetObjI_μ

added theorem SSet.stdSimplex.ι₁_whiskerLeft_toSSetObjI_μ

added theorem SimplexCategory.toTopHomeo_naturality

added theorem SimplexCategory.toTopHomeo_naturality_apply

added theorem SimplexCategory.toTopHomeo_symm_naturality

added theorem SimplexCategory.toTopHomeo_symm_naturality_apply

added def TopCat.stdSimplexHomeomorphI

added theorem TopCat.toSSet_map_const

added theorem sSetTopAdj_homEquiv_stdSimplex_zero

Modified Mathlib/AlgebraicTopology/SingularSet.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

added theorem CategoryTheory.uliftYonedaEquiv_symm_comp