Zulip Chat Archive

Stream: maths

Topic: Simplicial sets


view this post on Zulip Scott Morrison (Mar 14 2021 at 02:18):

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

view this post on Zulip Scott Morrison (Mar 14 2021 at 02:18):

@Johan Commelin

view this post on Zulip Scott Morrison (Mar 14 2021 at 02:19):

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

view this post on Zulip Johan Commelin (Mar 15 2021 at 06:10):

@Scott Morrison Thanks a lot for doing this!

view this post on Zulip Johan Commelin (Mar 15 2021 at 06:10):

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

view this post on Zulip Bhavik Mehta (Mar 15 2021 at 16:10):

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

view this post on Zulip Adam Topaz (Mar 15 2021 at 20:22):

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

view this post on Zulip Adam Topaz (Mar 15 2021 at 20:29):

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 :)

view this post on Zulip Scott Morrison (Mar 15 2021 at 21:07):

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.

view this post on Zulip Bhavik Mehta (Mar 16 2021 at 17:19):

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 :)

view this post on Zulip Adam Topaz (Mar 16 2021 at 17:21):

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

view this post on Zulip Bhavik Mehta (Mar 16 2021 at 17:22):

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

view this post on Zulip Bhavik Mehta (Mar 16 2021 at 17:22):

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

view this post on Zulip Adam Topaz (Mar 16 2021 at 17:23):

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

view this post on Zulip Bhavik Mehta (Mar 16 2021 at 17:25):

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

view this post on Zulip Adam Topaz (Mar 16 2021 at 17:25):

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

view this post on Zulip Bhavik Mehta (Mar 16 2021 at 17:26):

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

view this post on Zulip Adam Topaz (Mar 16 2021 at 17:27):

Oh, that's a good way of remembering!


Last updated: May 12 2021 at 08:14 UTC