Stonean spaces

Stream: condensed mathematics

[Yaël Dillies]

Is ExtrDisc the same as Stonean spaces?

[Johan Commelin]

Yes, I think it is

[Johan Commelin]

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

[Johan Commelin]

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

[Yaël Dillies]

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

[Johan Commelin]

What definition of Stonean space do you propose?

[Yaël Dillies]

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

[Johan Commelin]

I don't think you should

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Sebastien Gouezel]

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]

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

[Yaël Dillies]

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

[Reid Barton]

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]

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

[Reid Barton]

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