[Merged by Bors] - feat(algebraic_topology): introduce the simplex category

[semorrison]

• 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 -1s.

---

• depends on: [Merged by Bors] - feat(data/fin): pred_above_monotone #6170

[b-mehta]

It might not be the best idea, but it's possible to do

@[reducible] def simplex_category.mk (n : ℕ) : simplex_category := n
notation `[`n`]` := simplex_category.mk n

and then we can write

/-- The `i`-th face map from `[n]` to `[n+1]` -/
def δ {n : ℕ} (i : fin (n+2)) : [n] ⟶ [n+1] :=
(fin.succ_above i).to_preorder_hom

which is satisfying notation, probably should be local or in a locale though

[semorrison]

I'm very dubious about defining notation, even localized, that clashes with list notation. If we move to variant square brackets it becomes much less satisfying, so on balance I'm happy without notation. (But I am generally a notation skeptic, so am happy to be over-ruled here.)

[b-mehta]

I'm very dubious about defining notation, even localized, that clashes with list notation. If we move to variant square brackets it becomes much less satisfying, so on balance I'm happy without notation. (But I am generally a notation skeptic, so am happy to be over-ruled here.)

Reasonable, I'm also happy to be over-ruled. Perhaps there's a middle-ground though, possibly just a named constructor simplex.mk : nat -> simplex_category or nat.to_simplex so that the type doesn't need to be given, especially to make it easier to have n : nat in the type signature and then refer to morphisms n.to_simplex -> m.to_simplex.

[semorrison]

I think I've finished dealing with non-terminal simps, and also added the notation Bhavik suggested, but only as a local notation.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests