mathlib3

dd5363b5 - feat(algebraic_topology): introduce the simplex category (#6173)

feat(algebraic_topology): introduce the simplex category (#6173) * introduce `simplex_category`, with objects `nat` and morphisms `n ⟶ m` order-preserving maps from `fin (n+1)` to `fin (m+1)`. * prove the simplicial identities * show the category is equivalent to `NonemptyFinLinOrd` This is the start of simplicial sets, moving and completing some of the material from @jcommelin's `sset` branch. Dold-Kan is the obvious objective; apparently we're going to need it for `lean-liquid` at some point. The proofs of the simplicial identities are bad and slow. They involve extravagant use of nonterminal simp (`simp?` doesn't seem to give good answers) and lots of `linarith` bashing. Help welcome, especially if you love playing with inequalities in `nat` involving lots of `-1`s. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Yakov Pechersky <ffxen158@gmail.com> Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>