simplex category

Stream: maths

[Kevin Buzzard]

Emily Riehl is speaking "in London" in a couple of weeks and now that term is winding down I thought I would prepare a little for her talk by learning some basic simplicial stuff, as discussed at the beginning of her book with Verity. I was very pleased to discover simplex_category.lean in mathlib and I have been attempting to learn the theory from it. I was a bit confused by the special case of the first simplicial identity and its 10-line slow-to-elaborate proof: what is wrong with

/-- The special case of the first simplicial identity -/
lemma δ_comp_δ_self {n} {i : fin (n+2)} : δ i ≫ δ i.cast_succ = δ i ≫ δ i.succ :=
(δ_comp_δ (le_refl i)).symm

using the lemma before? This proof made me wonder whether this special case should even be a lemma, because if you regard these lemmas relating $\delta$ and $\sigma$ as some kind of "reduction rules" then the proof above seems to indicate that it's going the wrong way.

There's an interesting-looking "todo" in simplex_category.lean (line 142) which seems to imply that these relations (the "n'th simplicial identity" for all n -- is this standard terminology?) are generators of all relations. I guess one neat way of formalising this would be to show that to give a simplicial set is to give what's going on for deltas and sigmas, subject to these relations (one of which, I'm observing, seems to follow from another one, to my mild surprise). What is a reference for this stuff? I'm surprised there's not one in the module doc, and Riehl-Verity seem to treat it all as standard, which it no doubt is, so I'm wondering where the reference is. Something else which seems to be missing in the Lean file is the proof that any injection in the simplex category is a composition of deltas, and any surjection a composition of sigmas. And what is a reference for the proof that the relations in the Lean file are the "only relations"?

[Johan Commelin]

I don't know of anyone who as written out the details that these are the "only relations". The paper proof is very straightforward. The Lean proof will be some ugly induction.

[Johan Commelin]

I guess Kerodon has an appendix on some basics of simplicial stuff. (I actually don't know where I learned the basics, probably in some lecture...)

[Kevin Buzzard]

Oh, so is the result not important? I'm still struggling to work out what I need to know. The main thing I've discovered so far is that the simplicial set corresponding to one 0-simplex seems to have simplexes in every degree!

[Johan Commelin]

Yes, but they are all degenerate... :lol: (So it is still a finite simplicial set.)

[Kevin Buzzard]

This is different to how I learnt about simplicial complexes, where these degenerate things were not there. It reminds me a bit of when you're making the Cech complex of a cover and you start asking yourself whether you should have $U_i\cap U_j$ for all ordered pairs $(i,j)$ or just all unordered pairs -- you need to check it makes no difference.

[Adam Topaz]

Kevin, one nice way of recovering the topological intuition is to think of the topological n-simplex as the representable simplicial set represented by [n]. You can then glue such things as you would do for simplicial complexes by taking colimits which exist because of abstract nonsense.

[Adam Topaz]

And if you continue to develop this point of view you will eventually reach the geometric realization functor.

[Kevin Buzzard]

I was expecting the simplicial set to have nothing in degree n+1 but it seems to have a ton of degenerate objects

[Adam Topaz]

If the n-simplex is represented by [n], then the map from the n-simplex to the 1-simplex must be given by a morphism from [n] to [1] by Yoneda, so when you consider the presheaf represented by [1] which is the 1-simplex, you must have degenerate simplices.

[Adam Topaz]

(And similarly in higher dimensions as well, which you can see either explicitly or by taking products)

[Adam Topaz]

One word of caution: mathlib's [n] : simplex_category would correspond to [n+1] in the above.

[Kyle Miller]

Kevin Buzzard said:

This is different to how I learnt about simplicial complexes, where these degenerate things were not there.

They're more like what Hatcher calls delta-complexes in his book on algebraic topology. Where in traditional simplicial complexes, simplicies are identified by their vertex sets, in delta complexes this constraint is relaxed (at the cost of needing gluing data).