Zulip Chat Archive

Stream: condensed mathematics

Topic: extremely disconnected sets


view this post on Zulip Ben Lee (Dec 18 2020 at 18:58):

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

view this post on Zulip Adam Topaz (Dec 18 2020 at 18:59):

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

view this post on Zulip Adam Topaz (Dec 18 2020 at 19:01):

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

view this post on Zulip Calle Sönne (Dec 18 2020 at 19:04):

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

view this post on Zulip Adam Topaz (Dec 18 2020 at 19:04):

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

view this post on Zulip Calle Sönne (Dec 18 2020 at 19:06):

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

view this post on Zulip Ben Lee (Dec 18 2020 at 19:08):

Ok, I'll branch from Profinite2, thanks.

view this post on Zulip Johan Commelin (Dec 18 2020 at 20:56):

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

view this post on Zulip Johan Commelin (Dec 18 2020 at 20:56):

and the rest of that repo

view this post on Zulip Johan Commelin (Dec 18 2020 at 20:56):

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

view this post on Zulip Kevin Buzzard (Dec 18 2020 at 21:05):

Oh I completely forgot about that!

view this post on Zulip Ben Lee (Dec 18 2020 at 21:13):

Thanks! I'll definitely start there.

view this post on Zulip David Michael Roberts (Dec 23 2020 at 10:24):

Extremally disonnected?

view this post on Zulip Johan Commelin (Dec 23 2020 at 10:36):

@David Michael Roberts what exactly is the question?

view this post on Zulip David Michael Roberts (Dec 23 2020 at 10:47):

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

view this post on Zulip Johan Commelin (Dec 23 2020 at 10:56):

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


Last updated: May 09 2021 at 15:11 UTC