Completing Circle with two Origins S209

[felixpernegger]

As usual, Toronto is obviously false, but better keep that for now.

[GeoffreySangston]

The text of S83|P216, which the current change depends on ultimately, says the following.

Similar to the proof that {S83|P145}, using the fact that {S25|P216}.

How are these similar?

[felixpernegger]

The text of S83|P216, which the current change depends on ultimately, says the following.

Similar to the proof that {S83|P145}, using the fact that {S25|P216}.

How are these similar?

In that sense, that for any cover of the circle, we just add "one" more for the second origin. Then any locally finite refinement stays locally finite etc.

[GeoffreySangston]

No I meant how is the proof that line with two origins is locally hereditarily paracompact similar to the proof we've given that it's strongly paracompact? Or is that what you're answering? It looks like you're answering how a proof that the circle with two origins is hereditarily paracompact is similar to how the line with two origins is hereditarily paracompact, which is not what I asked.

[felixpernegger]

No I meant how is the proof that line with two origins is locally hereditarily paracompact similar to the proof we've given that it's strongly paracompact? Or is that what you're answering? It looks like you're answering how a proof that the circle with two origins is hereditarily paracompact is similar to how the line with two origins is hereditarily paracompact, which is not what I asked.

I mean one can use the same construction as for strongly paracompact, just replace "star finite" by "locally finite".

[GeoffreySangston]

So saying "the proof is similar to strongly paracompact" is a proof the line with two origins is paracompact or hereditarily paracompact? If the former why does the latter follow from the text? Shouldn't we include an actual argument?

[felixpernegger]

The proof why line with two orgins is hereditarily paracompact is similar to the proof of line with two origins being strongly paracompact.
The proof why Circle with two origins is hereditarily paracompact is in turn similar to why line with two orgins is hereditarily paracompact.

We could include an actual argument of course. The main reaosn I omitted that is because the proof is sort of annoying to write down.

[felixpernegger]

Sorry for the confusion

[GeoffreySangston]

I'm confused about how the proof that it's strongly paracompact is similar to how it's hereditarily paracompact, and what that has to do with the following line about the real line being hereditarily paracompact. The natural interpretation is that hereditary paracompactness must be preserved by finite unions of open subspaces, but I think that's not correct. Then I clicked strongly paracompact and the argument doesn't seem to apply to an arbitrary subspace without changing it in multiple places.

[prabau]

I have not looked at it, but if things are not clear, some more words may be needed. It is indeed annoying to write down arguments for this. Would something like '... the same construction as for strongly paracompact, just replace "star finite" with "locally finite" ... ' help?

[GeoffreySangston]

Ah okay I didn't realize you were saying do a sed replace of star-finite with locally finite and have a complete argument. That would have helped.

We also don't need the following line about hereditary paracompactness of the real line if we write that. That made me think the argument is about taking a union of hereditarily paracompact open subspaces.

[prabau]

(@GeoffreySangston Sorry if I interjected into your conversation. That was a general comment without having looked at it. So don't take my word for it.)

I wrote "I have looked at it", but meant "I have not looked at it".

[GeoffreySangston]

Your interjection helped. I was misunderstanding how the two things were similar. I think the following is a strict improvement, but I can see how most people familiar with these properties wouldn't have been as confused as me so it doesn't really matter.

Replace the text "star-finite" with "locally finite" in {S83|P145}.

(Also, "star-finite" and "star finite" both appear in {S83|P145}.)

---

Wait I'm still confused. That's just a proof the line with two origins is paracompact. Does the same exact proof go through if we replace X with an open subspace?

[felixpernegger]

Your interjection helped. I was misunderstanding how the two things were similar. I think the following is a strict improvement, but I can see how most people familiar with these properties wouldn't have been as confused as me so it doesn't really matter.

Replace the text "star-finite" with "locally finite" in {S83|P145}.

(Also, "star-finite" and "star finite" both appear in {S83|P145}.)

Wait I'm still confused. That's just a proof the line with two origins is paracompact. Does the same exact proof go through if we replace X with an open subspace?

Your interjection helped. I was misunderstanding how the two things were similar. I think the following is a strict improvement, but I can see how most people familiar with these properties wouldn't have been as confused as me so it doesn't really matter.

Replace the text "star-finite" with "locally finite" in {S83|P145}.

(Also, "star-finite" and "star finite" both appear in {S83|P145}.)

Wait I'm still confused. That's just a proof the line with two origins is paracompact. Does the same exact proof go through if we replace X with an open subspace?

Every subspace of line (circle) with two orginins is either a subspace of the normal euclidean line (in which case the subspace is paracompact since R is her. paracompact) or a subpace of R with "one line doubled": In that case one may apply the same argument as in strongly paracompact to show the subspace is paracompact (since without the point doubled it is paracompact)

[GeoffreySangston]

I think the following observation gives hereditary paracompactness using meta-properties we've already stated

An open subspace of the line with two origins is homeomorphic to a disjoint union of Euclidean lines and one or zero lines with two origins. Now apply the meta-property that hereditary paracompactness is preserved by disjoint unions together with paracompactness of the Euclidean line and the line with two origins

This is clean because we don't have to do any textual replacement of the proof of strong paracompactness of the line with two origins.

[prabau]

I finally took a look at it and I agree with Geoffrey that what is written now is not adequate. The proposal in #1719 (comment) is better, except for some minor details. Basically, it's enough to show that every open subset of X is paracompact. The whole space is paracompact, since it's compact. And every proper open set is a disjoint union of open sets, each homeomorphic to either the reals or the line with two origins, with each of them paracompact.

I have made a suggestion by modifying Geoffrey's suggestion slightly. Please take a look in preview mode.

[prabau]

Leaving it to @GeoffreySangston to do the final review.

[prabau]

@felixpernegger I am surprised you applied my suggestion without even taking the time to look at it in detail?

[felixpernegger]

it looks good to me

[GeoffreySangston]

@prabau @felixpernegger I think I fixed a minor oversight. I also tried to improve S83 while we're at it. Since I made this change I think @prabau should do a final review now (or ping-pong it back to me if my last update needs fixing?)

[prabau]

looks good