Explicit description of condensed sets

Stream: mathlib4

[Dagur Asgeirsson]

I've opened #6731 with a huge file Mathlib.Condensed.Explicit containing all the code me, @Riccardo Brasca , @Filippo A. E. Nuccio and others wrote during the Copenhagen masterclass, giving the explicit descriptions of condensed sets. I've broken it down into sections and in a comment at the top of the file I describe the structure, a plan for PR-ing this in smaller pieces. If anyone is interested, feel free to help with this process, and we can use this thread to coordinate.

[Dagur Asgeirsson]

Let me also mention that getting this into mathlib will mean that we can actually start working with condensed sets. This gets us closer to the definition of condensed sets in LTE and hopefully we'll be able to "port" some stuff from there to mathlib.

[Yaël Dillies]

Should this be a new top folder or rather a subfolder of an existing one?

[Johan Commelin]

Probably depends on who you ask. I guess there are people who think it shouldn't even be a new top folder, but just the root (-;

[Adam Topaz]

It should be a new top folder. Eventually Condensed should replace Topology, right? (not serious, in case it's not clear)

[David Michael Roberts]

Dagur Asgeirsson said:

This gets us closer to the definition of condensed sets in LTE ...

So actually as small sheaves, rather than as more pyknotic objects, using Lean's universes?

[Johan Commelin]

No, I think everything is still pyknotic.

[Dagur Asgeirsson]

Yes, still pyknotic (like in LTE)

[Dagur Asgeirsson]

Yaël Dillies said:

Should this be a new top folder or rather a subfolder of an existing one?

I'm not sure I understand the terminology. Condensed is a top folder now, right?

[Dagur Asgeirsson]

Anyway, I've opened the preliminary PR's #6750 and #6758

[Yaël Dillies]

That's right. Your PR currently makes it a top folder.

[Dagur Asgeirsson]

Well not my PR, it's been a top folder since #4527 was merged

[Dagur Asgeirsson]

Do you want to change this? If so, where do you think it should live?

[Yaël Dillies]

I don't really mind! I just want to make sure the question was asked.

[Dagur Asgeirsson]

Ok! I think it makes sense as it is. For example, it's highly categorical, but the way I see it, it wouldn't make sense to put it in the CategoryTheory folder, in the same way as e.g. algebraic geometry doesn't belong in the CategoryTheory folder.

[Dagur Asgeirsson]

I've opened a few more PR's about Stonean: #6771, #6774, #6779

[Dagur Asgeirsson]

Related but independent: #6809, #6810