Simplicial sets

Stream: maths

[Scott Morrison]

Just noting that I have mostly brought branch#sset up to date with mathlib master (a while back we PR'd some content across).

[Scott Morrison]

@Johan Commelin

[Scott Morrison]

It is not quite done: adjunction.lean runs aground on the shoals of universe polymorphism, and I'm out of enthusiasm for now.

[Johan Commelin]

@Scott Morrison Thanks a lot for doing this!

[Johan Commelin]

Do you have any idea what might be the best way to work with augmented simplicial objects?

[Bhavik Mehta]

Scott Morrison said:

It is not quite done: adjunction.lean runs aground on the shoals of universe polymorphism, and I'm out of enthusiasm for now.

Which file is this? I think I might have fun playing with the polymorphism here

[Adam Topaz]

I just made the simplicial circle: https://github.com/leanprover-community/mathlib/blob/0347f5d2e29b37a7f9cc9d2702bc64f5f2ae7443/src/algebraic_topology/simplicial_set.lean#L98

[Adam Topaz]

If we had an analogue of parallel_walking_pair with n morphisms instead of just 2, then one can easily construct the simplicial sphere as well :)

[Scott Morrison]

Bhavik Mehta said:

Scott Morrison said:

It is not quite done: adjunction.lean runs aground on the shoals of universe polymorphism, and I'm out of enthusiasm for now.

Which file is this? I think I might have fun playing with the polymorphism here

This is on branch#sset, in topology.simplicial.adjunction. (Note that in that branch the stuff that has already been PR'd to master is in the algebraic_topology folder. It would be fine to move the stuff in the branch over.

[Bhavik Mehta]

Adam Topaz said:

If we had an analogue of parallel_walking_pair with n morphisms instead of just 2, then one can easily construct the simplicial sphere as well :)

In #4885 I made this analogue and called it walking_parallel_chunk, I didn't think it'd be useful for anything though! Feel free to just copy that bit of code to save you a bit of time :)

[Adam Topaz]

@Bhavik Mehta Does that PR have a proof of the adjoint functor theorems?! Why is it not in mathlib! That sounds great!

[Bhavik Mehta]

It's a proof of the general adjoint functor theorem - I think the special aft should be doable now that we have subobjects though

[Bhavik Mehta]

It's not in mathlib because I'm lazy and I didn't need it :P

[Adam Topaz]

I didn't know there was a "general" and a "special" adjoint functor theorem

[Bhavik Mehta]

Perhaps those names aren't standard - I mean these names: https://ncatlab.org/nlab/show/adjoint+functor+theorem#statement

[Adam Topaz]

Oh, I guess the "general" version is also called "Freyd's ..."

[Bhavik Mehta]

In my mind, the general version has extra conditions on the functor, and the special version has extra conditions on the categories

[Adam Topaz]

Oh, that's a good way of remembering!