ExtrDisc

Stream: Copenhagen Masterclass 2023

[Johan Commelin]

Controversial question: In mathlib, should we use ExtrDisc as name for the category of compact Hausdorff extr.disc spaces? I know that in the lecture notes so far, extr.discs have always been considered in the CH setting. But I can imagine that in the broader scope of mathlib, we might want to reserve ExtrDisc for the topological spaces that are merely extr.disc and not necessarily CH.

There are other candidates: Stonean seems to be somewhat common in the literature. And another option would be CHED. In fact, recently I've been discussing about LCHED a bit with Reid (so that would be locally compact Hausdorff extr.discs).

cc @Dagur Ásgeirsson @Adam Topaz

[Johan Commelin]

I'm of course asking this question in relation to

feat: define the category of extremally disconnected compact Hausdorff spaces #5761

[Dagur Asgeirsson]

I vote for Stonean

[Johan Commelin]

/poll How should we call the category of compact Hausdorff extremally disconnected spaces

• ExtrDisc
• CompHausExtrDisc
• CHED
• Stonean

[Dagur Asgeirsson]

I've changed #5761 to Stonean (and also resolved the comments on that one and #5762, #5763)

[Dagur Asgeirsson]

#5761 should be ready to merge now @Johan Commelin