extremely disconnected sets

Stream: condensed mathematics

[Ben Lee]

Hello folks, I'm going to work on extremely disconnected sets (definition 2.4) unless someone else is already working on it.

[Adam Topaz]

As far as I know, all the work in this direction is taking place in this branch branch#Profinite2

[Adam Topaz]

This is @Calle Sönne 's branch. He probably knows the state of the art here

[Calle Sönne]

Ben Lee said:

Hello folks, I'm going to work on extremely disconnected sets (definition 2.4) unless someone else is already working on it.

I dont think anyone is doing this right now, so that would be great

[Adam Topaz]

Maybe @Kenny Lau is secretly working on this? (Via Stone duality :) )

[Calle Sönne]

Adam Topaz said:

As far as I know, all the work in this direction is taking place in this branch branch#Profinite2

On Profinite2 I am currently working towards showing that Profinite is a reflective subcategory of CompHaus

[Ben Lee]

Ok, I'll branch from Profinite2, thanks.

[Johan Commelin]

@Ben Lee Also see https://github.com/ImperialCollegeLondon/condensed-sets/blob/master/src/extremally_disconnected.lean

[Johan Commelin]

and the rest of that repo

[Johan Commelin]

there's not too much there... but you should at least be aware of it

[Kevin Buzzard]

Oh I completely forgot about that!

[Ben Lee]

Thanks! I'll definitely start there.

[David Michael Roberts]

Extremally disonnected?

[Johan Commelin]

@David Michael Roberts what exactly is the question?

[David Michael Roberts]

I mean, isn't it extremally, not "extremely"? Maybe I'm just being pedantic, but WP does complain about the latter: https://en.wikipedia.org/wiki/Extremally_disconnected_space

[Johan Commelin]

ooh, in the title of this thread. Yes, you are right. I glossed over it