Zulip Chat Archive

Stream: condensed mathematics

Topic: Stonean spaces


Yaël Dillies (Feb 18 2022 at 09:50):

Is ExtrDisc the same as Stonean spaces?

Johan Commelin (Feb 18 2022 at 09:51):

Yes, I think it is

Johan Commelin (Feb 18 2022 at 09:51):

In general, extremally disconnected spaces are something more general. But in this project we use it as a synonym for Stonean spaces.

Johan Commelin (Feb 18 2022 at 09:53):

@Yaël Dillies Are they about to enter mathlib?

Yaël Dillies (Feb 18 2022 at 10:03):

I will soon have CompleteBoolAlg, so proving the equivalence would be fun.

Johan Commelin (Feb 18 2022 at 10:03):

What definition of Stonean space do you propose?

Yaël Dillies (Feb 18 2022 at 10:06):

Compact Hausdorff extremally disconnected topological space sounds fine to me, but I don't know whether we should use Stonean locales instead.

Johan Commelin (Feb 18 2022 at 10:07):

I don't think you should

Johan Commelin (Feb 18 2022 at 10:07):

And "extremally disconnected" will be defined for general top. spaces?

Johan Commelin (Feb 18 2022 at 10:08):

We'll need some API for them. In particular the equivalence with the current definition (i.e., projective objects in Profinite or CompHaus, i.e., lifting against surjections)

Sebastien Gouezel (Feb 18 2022 at 10:10):

I wonder if some of my work on Polish spaces is related to what you do in LTE. Among other things, there are two basic topological results I prove there:

  • Any nonempty closed subset s of ℕ → ℕ is a retract, i.e., there is a continuous map from ℕ → ℕ to s coinciding with the identity on s.
  • Any nonempty Polish space (i.e., complete second-countable metric space) is a continuous image of ℕ → ℕ.

(and I also define analytic sets, as continuous images of Polish spaces).

If you have already pushed some related stuff, I should probably refactor my proofs to use what you have done.

Johan Commelin (Feb 18 2022 at 10:12):

The stuff about retracts seems related, but I don't immediately see a direct connection.

Johan Commelin (Feb 18 2022 at 10:12):

I don't think extremally disconnected spaces will ever be Polish, or vice versa. (Except maybe finite spaces.)

Sebastien Gouezel (Feb 18 2022 at 10:14):

Your spaces are compact but non-metrizable in general, right? (So, small from the topological point of view, but big from the cardinality point of view). While Polish spaces are complete but metrizable (so, bigger from the topological point of view, but smaller from the cardinality point of view).

Yaël Dillies (Feb 18 2022 at 10:15):

Oh, so ExtrDisc is not currently defined as in the nLab page?

Yaël Dillies (Feb 18 2022 at 10:20):

Disclaimer: I first learned about Stonean spaces a week ago.

Reid Barton (Feb 18 2022 at 13:16):

I have been thinking that there should be a descriptive set theory-flavored analogue to the condensed story, which ought to be adequate for applications to analysis, but I don't think there is a direct connection to the current setup.

Reid Barton (Feb 18 2022 at 13:43):

Is the Gleason definition (closure of open is open) useful for something? The nlab page isn't very informative

Reid Barton (Feb 18 2022 at 13:44):

I guess it could be related to this De Morgan property?


Last updated: Dec 20 2023 at 11:08 UTC