mathlib
7fccf40a - feat(algebraic_topology/topological_simplex): This defines the natural functor from Top to sSet. (#8305)

Commit

4 years ago

feat(algebraic_topology/topological_simplex): This defines the natural functor from Top to sSet. (#8305) This PR also provides the geometric realization functor and the associated adjunction.

Author

adamtopaz

Parents

7d53431e

mathlib 7fccf40a - feat(algebraic_topology/topological_simplex): This defines the natural functor from Top to sSet. (#8305)

mathlib
7fccf40a - feat(algebraic_topology/topological_simplex): This defines the natural functor from Top to sSet. (#8305)