Zulip Chat Archive

Stream: condensed mathematics

Topic: projective objects in profinite sets


view this post on Zulip Johan Commelin (Apr 15 2021 at 08:10):

I'm just posting a pointer to this file in a pretty old repo:
https://github.com/ImperialCollegeLondon/condensed-sets/blob/master/src/extremally_disconnected.lean

In the near future we'll want to know that extremally disconnected sets are the profinite objects in profinite sets. This file contains one direction.

view this post on Zulip Johan Commelin (Apr 15 2021 at 08:11):

Do we have profinite objects in arbitrary categories? @Markus Himmel @Scott Morrison ?

view this post on Zulip Peter Scholze (Apr 15 2021 at 08:25):

Johan Commelin said:

In the near future we'll want to know that extremally disconnected sets are the profinite objects in profinite sets. This file contains one direction.

You mean the projective objects

view this post on Zulip Johan Commelin (Apr 15 2021 at 08:29):

Ooops... to many "pro"words. Edit: fixed.

view this post on Zulip Markus Himmel (Apr 15 2021 at 08:35):

Projective objects are defined in #7108, but there isn't any API yet for actually working with them.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 08:42):

Projective modules are in #6813 which is on the queue, and a first natural test will be to see whether these two PRs can interact fruitfully.

For the mathlib community one huge benefit of projects like this is that it has given us a lot of motivation to actually make stuff like projective objects and modules, and I'm really pleased about this because it conforms to my motto of driving mathlib towards interesting mathematics, which is the only way that software like this is going to be taken seriously by mathematicians in general.

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 08:44):

There is also the WIP #7113, which is the beginning of the experiment to see if they glue together well.


Last updated: May 09 2021 at 16:20 UTC