Commit 2021-03-17 01:14 b9ccb8fa

View on Github →

feat(algebraic_topology/simplicial_objects + ...): Truncated simplicial objects + skeleton (#6711) This PR adds truncated simplicial objects and the skeleton functor (aka the truncation functor).

Estimated changes

Modified src/algebraic_topology/simplex_category.lean

added def simplex_category.len

added theorem simplex_category.len_mk

added theorem simplex_category.mk_len

added def simplex_category.truncated.inclusion

added def simplex_category.truncated

Modified src/algebraic_topology/simplicial_object.lean

added def category_theory.simplicial_object.sk

added def category_theory.simplicial_object.truncated

Modified src/algebraic_topology/simplicial_set.lean

added def sSet.sk

added def sSet.truncated