projective objects in profinite sets

Stream: condensed mathematics

[Johan Commelin]

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.

[Johan Commelin]

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

[Peter Scholze]

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

[Johan Commelin]

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

[Markus Himmel]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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