Dieudonne complete + monotonically normal implies paracompact

[Moniker1998]

Follows from theorem of Balogh and Rudin as in the link. I have read the proof of theorem II before, so all I had to do is brush up on what screenable means and equivalence with paracompactness + the article of Engelking and Lutzer. So I can vouch for correctness of theorem I.

[prabau]

This is a very deep result. To help the understanding of all this, how about putting this PR on hold and start by adding the screenable property to pi-base?

[Moniker1998]

@prabau we could. Sorry for my previous comment. I meant strongly screenable is equivalent to paracompactness with good enough separation properties, screenable is not. We could add it but I don't see a particular reason to. Why do you want to add it? And why do you want to put this PR on hold?

Theorem I uses screenable in its proof that's true (with it essentially being the definition of screenable if not for the stationary subset of uncountable regular cardinal condition), but the proof, located in Nagata, that normal + countably paracompact + screenable implies strongly screenable and so paracompact, is easy.

Strongly screenable implies paracompact is part of equivalences of paracompactness in Engelking.

[Moniker1998]

How about we finish with this PR (which does not require screenable to be in pi-base, or helps in any deductions, as far as I'm aware), raise an issue to add screenable and strongly screenable properties to pi-base, and then later, add them?

[Moniker1998]

@prabau I have tried to find a source using google gemini and could not find it, which suggests to me that a single source does not exist and what I wrote in that math.se post is the best we have

[Moniker1998]

@prabau can you approve this? I don't know what's the obstruction, this is straightforward

[Moniker1998]

@prabau please work on my PR I beg of you on my metaphorical knees

[prabau]

I'll take a closer look later today.

@StevenClontz In the mean time, would you mind taking a look as well? What's your guidance on just quoting complicated results from the literature?

[Moniker1998]

@StevenClontz In the mean time, would you mind taking a look as well? What's your guidance on just quoting complicated results from the literature?

Personally I think we did cite such results in the past and it wasn't a problem. Heck, I'd argue some of the results in Steven's papers were of that type, and we cited them regardless.

I also don't see a reason why we should care to make it a problem. Why would we hold anybody back? That would lead to needless stagnation. That sounds pointless. A situation would perhaps be different if no one would check those results or vouch for their validity.

This case is different as well since it's not a direct citation. We have a solution, you and anyone else, are free to contribute an easier/more elementary one if you can come up with it (the thread on math.se is open for anyone to answer).

[StevenClontz]

@Moniker1998 has a good point that, not infrequently, researchers will quote and use powerful results from the literature in their papers as a black box, so having a higher standard of peer review here seems a little awkward.

What's important before merging into the database is that we agree that the definitions (not just names) are aligned, and that we're able to cite something from the literature or another source we accept as peer review. So for me it's just the lack of a direct citation from the literature, but we do point to MathSE frequently to put pieces together like this.

I agree with https://math.stackexchange.com/a/5144647/86887 which mostly relies on the power of Monotone normality (Belogh, Rudin) Theorem I. I'd word slightly differently it like this:

Consider a Dieudonne complete, monotonically normal space $X$. Given a closed subset $S\subseteq X$ which is a copy of a subset of a regular cardinal, we have that $S$ is Dieudonne complete GO-space. By Thm 3.2 of Paracompactness in ordered spaces by Engelking and Lutzer, $S$ is paracompact. Therefore by Thm 2.3 of the same paper, $S$ is not itself a copy of a stationary subset of a regular cardinal. Thus by Thm I of Belogh/Rudin, $X$ is paracompact.

(Aside: I prefer the more semantic alias "completely uniformizable" P221, but that's not really important here.)

[StevenClontz]

The MathSE reference here is a valid straight-forward proof (using powerful results from the literature), and this theorem answers https://topology.pi-base.org/spaces?q=Monotonically+normal+%2B+Dieudonn%C3%A9+complete+%2B%7E+Paracompact

[StevenClontz]

(off-topic, my master's thesis was re-proving the characterization paracompact iff doesn't contain stationary subset of regular cardinal, but in the much weaker situation of LOTS, so this was a fun look back for me, as I moved on to game-theoretic stuff pretty soon after that project.)

[Moniker1998]

@StevenClontz

As for your rewrite of my Math.SE answer, I agree that it would be perhaps less weird to say that $S$ is a Dieudonne complete GO-space, but I find that in the proof of Engelking, Lutzer theorem, they prove precisely that sets like $S$ are not Dieudonne complete. And since I was diving into the proofs of those theorems, I found it more natural to reference the proof itself.

As for completely uniformizable alias, we had discussions about this with @prabau, and Patrick doesn't like that alias, so I've been trying to avoid it (although I enjoy it as well).

[StevenClontz]

Yeah, your proof is fine as-is; when reviewing I often find myself rewriting the proof "how I'd do it" anyway to help me verify things.

I need to revisit #1821, after which we could see if the community would accept a guideline like "if multiple names are used in the peer reviewed literature, we prefer more semantic names" (wording could be workshopped a bit).

[prabau]

"Completely uniformizable" is not a bad name at all, and it's semantically descriptive. But I think "Dieudonne complete" is widely used for this, more than the other name (298 results vs 38 in Google scholar for example), and also does not have any ambiguity either. So I really think we should keep the more common name in this case.

[prabau]

Consider a Dieudonne complete, monotonically normal space X . Given a closed subset S ⊆ X which is a copy of a subset of a regular cardinal, we have that S is Dieudonne complete GO-space. By Thm 3.2 of Paracompactness in ordered spaces by Engelking and Lutzer, S is paracompact. Therefore by Thm 2.3 of the same paper, S is not itself a copy of a stationary subset of a regular cardinal. Thus by Thm I of Belogh/Rudin, X is paracompact.

Maybe it's just me. But I find this version clearer to follow.