[pzjp]

See #1413.

[pzjp]

Should we change strongly 0-dim in T462 to Ultraparacompact? Then the Engelking reference is not of direct use.

[yhx-12243]

@prabau Request for your opinion.

[prabau]

T462:About replacing strongly 0-dim with ultraparacompact in the hypotheses: maybe. I want to think some more about it.

Apart from that, I really like this proof. It's slightly simpler than the proof in Engelking, due to the use of ultraparacompact.

A few comments about it.
I think it's better to talk about minimum and maximum elements for a total order, instead of minimal and maximal (since these last two have a slightly different meaning for general posets, even though they are the same for total orders).

Some of the $\mathscr U_n$ can have a finite number of elements. So the corresponding linear order on it will necessariy have a min and a max element. If $\mathscr U_n$ is infinite, does it need to have a min and max also to make the argument work, or it does not matter at all?
(except that if there is a min and max, talking about "a closed interval in $\mathscr U_{n+1}$" is easier to grasp maybe?)

I think it may be necessary. Thinking some more.

[prabau]

Yes, I think it's needed to ensure that each member of $\mathscr U_{n+1}$ has an immediate successor and an immediate predecessor.

Or maybe it's not needed, but what is needed is the second subbullet:
"for each $V\in \mathscr U_n$ the set ${ U\in\mathscr U_{n+1}: U\subseteq V}$ is a closed interval in $\mathscr U_{n+1}$.",
which is what ensures the order of $\mathscr U_{n+1}$ has a successor/predecessor for each element.
(i.e., one gives an order to that set for each $V$, and then one pieces all these orders together, according to a higher level "discrete" order (which is the order on $\mathscr U_n$), so the final result is also "discrete").

Anyway, do you think it's clear, or something needs to be added?

[pzjp]

Think about an isolated point. That's why we need maximum and minimum in each subdivision of $U_n$.
But the existence of successors/predecessors within a single partition has to be ensured separately.

[prabau]

@pzjp @yhx-12243 I have added #1425 including the direct result that the Baire space S102 is ultranormal. In combination with T462 here, that will allow to deduce the S102 is LOTS.
So we'll be able to consolidate both proofs of LOTS into one. (i.e., no need to refer to S102 in the proof of S102).
(But we may need to give some more details for the justification of LOTS at the end of the proof of T462.)

Let me know what you think about the above.

[prabau]

T462: I think it's not a bad idea to change the hypothesis of strongly zero-dim to ultraparacompact. It makes the argument of the proof a little tighter by focusing on the important ingredient.

Having [strongly zero-dim + metrizable => LOTS ] seems superficially more general, but it's equivalent since for metrizable spaces, being strongly zero-dim and and being ultraparacompact are equivalent (already known to pi-base).

What's your opinion?

[pzjp]

Switching to UPc seems a good idea. But then the proof should be more standalone (I wrote just an alternative hint) since the reference becomes slightly less relevant.

[prabau]

Switching to UPc seems a good idea. But then the proof should be more standalone (I wrote just an alternative hint) since the reference becomes slightly less relevant.

I agree. Will it become better to have it with details on mathse?

(I need to think some more about the details for the last paragraph of the proof.)

[pzjp]

Probably, since it becomes demanding and would be way longer if we try to explain all the details.
Also if we remove P133 for S102 the details on equality of topologies would be even more necessary.

[prabau]

Let me ask the question on mathse. Will post the link here.

[prabau]

https://math.stackexchange.com/questions/5093371/are-ultrapacompact-metrizable-spaces-orderable-lots

[prabau]

For the proof, to a point $x$ one associates a (unique) sequence $\phi(x)=(U_n)_{n<\omega}$ with $x\in U_n\in\mathscr U_n$.

I am having difficulty with one edge case: (wrt the order on the $\mathscr U_n$) if $x$ is there is an $N$ such that for all $n\ge N$ $U_{n+1}$ is the minimum element of the closed interval $\{ U\in\mathscr U_{n+1}: U\subseteq U_n\}$. (i.e., one could say $x$ is on a "minimal branch" in the corresponding poset). That would probably mean that $x$ is isolated on the left and one would have to find an immediate predecessor in the induced order on the image $\phi(X)$. I need to think more about this case. You'll probably explain it to me before I get the chance to figure it out :-)

Also, one needs to add that the elements of each $\mathscr U_n$ are nonempty (to make choosing suitable intervals in $\phi(X)$ possible).

[prabau]

Expanding on the above. Let $Z=\prod_{n<\omega} \mathscr U_n$ denote the LOTS space with the order topology induced by the lexicographic order as in the proof. So we have a map $\phi:X\to Z$. For the element $x\in X$ in the comment above, I can see that $\phi(x)$ has a predecessor in $Z$. But what needs to be shown and is not clear to me is: why does $\phi(x)$ have a predecessor in $\phi(X)$?

[pzjp]

I got to understand the importance of $f_i$ and $g_i$ function in the Engelking's hint. They imply that $U=[f_i(U),g_i(U)]$.

[prabau]

I did some minor tweaks for T462. In particular, when the mathse question of a mathse post is relevant to the topic, we usually refer to the full post (i.e., point to the question itself). We use name: Answer to "..." only if the full post is not relevant, but we want to point to a specific answer.

[prabau]

As far as I am concerned, this is ready to approve and merge, if you want to move it out of Draft.