Commit 2024-01-15 16:06 d8dff07d

View on Github →

feat(AlgebraicTopology): generalize universes for the standard simplex (#9631) The PR generalizes universes for standardSimplex, which is now a functor SimplexCategory ⥤ SSet.{u} for any universe u.

Estimated changes

Modified Mathlib/AlgebraicTopology/ExtraDegeneracy.lean

Modified Mathlib/AlgebraicTopology/Quasicategory.lean

Modified Mathlib/AlgebraicTopology/SimplicialSet.lean

modified def SSet.boundary

modified def SSet.horn.face

added theorem SSet.standardSimplex.coe_edge_down_toOrderHom

deleted theorem SSet.standardSimplex.coe_edge_toOrderHom

added theorem SSet.standardSimplex.coe_triangle_down_toOrderHom

deleted theorem SSet.standardSimplex.coe_triangle_toOrderHom

added theorem SSet.standardSimplex.const_down_toOrderHom

deleted theorem SSet.standardSimplex.const_toOrderHom

added theorem SSet.standardSimplex.map_apply

added theorem SSet.standardSimplex.map_id

added def SSet.standardSimplex.objEquiv

modified def SSet.standardSimplex

added def SSet.uliftFunctor

added def SSet.yonedaEquiv

Modified Mathlib/AlgebraicTopology/SingularSet.lean

Modified Mathlib/CategoryTheory/Yoneda.lean

added def CategoryTheory.yonedaCompUliftFunctorEquiv