Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Some missing traits for Radial intervals at 0 (S135) #1191

Merged
merged 25 commits into from
Jan 18, 2025
Merged

Conversation

pzjp
Copy link
Collaborator

@pzjp pzjp commented Jan 11, 2025

Adding for S135:

Cleanup (redundant traits):

  • P8 ($T_5$)
  • P18 (Lindelof)
  • P23 (weakly loc. compact)
  • P26 (separable)
  • P28 (first countable)
  • P29
  • P38 (arc connected)
  • P56 (meager)
  • P65 (card. continuum)
  • P129 (indiscrete)

@yhx-12243
Copy link
Collaborator

yhx-12243 commented Jan 12, 2025

Here is what can be suggested for now:
P64 (Baire): Maybe we can directly prove stronger P206 (Strongly Choquet), because second player can get into an interval first round.
P23 (WLC), P38 (Arc connected), P65 (Cardinality = $\mathfrak c$): redundant.

Other known traits (no need to add now, just sketch):
¬P63 (Čech complete): Contains S131 as closed subspace, which is not Čech complete (I'll upload S131|¬P63 some time)
P109 (Monotonically normal): Simple but tedious. Use the half interval technique provided in T669.
P118 (Has a σ-locally finite k-network): Simple but very tedious. Maybe waiting for a good proof.

@pzjp pzjp marked this pull request as ready for review January 12, 2025 17:41
Co-authored-by: yhx-12243 <[email protected]>
@prabau
Copy link
Collaborator

prabau commented Jan 17, 2025

P15 (perfectly normal): two things are needed for a space to be perfectly normal: (1) $X$ is normal; (2) every open set is an $F_\sigma$ (for example). Right now, condition (1) is missing and there is circular reasoning here, because checking on the web page, the justification for normal uses that the space is perfectly normal. We should add (1) in a first paragraph mentioning item #2 for space #141 in S&S.

Maybe the following is obvious, but I am not sure. Can you explain to me why showing that a point (all points?) has a local base of open $F_\sigma$ nbhds is enough to show every open set is an $F_\sigma$?

@prabau
Copy link
Collaborator

prabau commented Jan 17, 2025

P34 (fully normal):
https://topology.pi-base.org/spaces/S000135/properties/P000034
We should remove this trait, which only quotes the General Reference Chart, and replace it with P30 (paracompact) referencing item #5 of space #141 in S&S.

@yhx-12243
Copy link
Collaborator

Maybe the following is obvious, but I am not sure. Can you explain to me why showing that a point (all points?) has a local base of open $F_\sigma$ nbhds is enough to show every open set is an $F_\sigma$ ?

Of course this space is very special that we can directly prove it. Generally, if every open set in the basis is $F_\sigma$ and if an open set can be written as the union of $\sigma$-locally finite collection of open set in basis, then it is still $F_\sigma$ (because union of locally finite closed set is still closed), and furthermore every paracompact space suffices.

@prabau
Copy link
Collaborator

prabau commented Jan 17, 2025

@yhx-12243 So assume a space $X$ is paracompact. Given a single open set $O\subseteq X$, how do you get a $\sigma$-locally finite collection of basic open sets whose union is $O$?

@yhx-12243
Copy link
Collaborator

yhx-12243 commented Jan 17, 2025

@yhx-12243 So assume a space X is paracompact. Given a single open set O ⊆ X , how do you get a σ -locally finite collection of basic open sets whose union is O ?

Let $X$ be regular paracompact and $U_x$ be an open neighborhood of $x$. Then $\{U_x\}$ is an open cover, and by paracompactness, it has a open refinement $\{V_\alpha\}$ such that it is locally finite. Furthermore, for any open subset $U$, $U = \bigcup_{\alpha \in I_U} V_\alpha$ for some index subset $I_U$.

Now, if every open set in $V_\alpha$ is $F_\sigma$, i.e., $V_\alpha = \bigcup F_{\alpha, n}$, then we can concluded that $U = \bigcup K_n$, where $K_n = \bigcup F_{\alpha, n}$ is closed.

However, $V_\alpha$ may not be $F_\sigma$ usually, e.g., S41 (Lexicographic unit square).

@prabau
Copy link
Collaborator

prabau commented Jan 17, 2025

I had no problem getting an F-sigma from a sigma-locally finite family of F-sigma open sets. But the rest of the setup does not quite make sense for me.

We are given a single fixed open set $U$ to start with and we want to show it is an F-sigma. This $U$ will have maybe nothing to do with the collections of $U_x$ or of $V_\alpha$. The goal is to show something specifically for $U$.

Also, there was no assumption of a regular space (although it is true for S135). But let's assume it if needed.

@prabau
Copy link
Collaborator

prabau commented Jan 17, 2025

I am not convinced the argument works. It would be an interesting question for mathse.

Anyway, I agree that a more direct proof for S135 is possible and preferable.

@yhx-12243
Copy link
Collaborator

I see because this argument did not work on S41, as previously mentioned.

pzjp and others added 8 commits January 17, 2025 09:59
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
@pzjp
Copy link
Collaborator Author

pzjp commented Jan 17, 2025

@prabau My proof is not about $F_\sigma$ open base at every point, but about base at the origin and all open sets missing the origin being $F_\sigma$. Then every open set is the union of an $F_\sigma$ neighborhood of $0$ (if necessary) and an $F_\sigma$ open set missing $0$. Added one line at the end and made it P132.

@prabau
Copy link
Collaborator

prabau commented Jan 18, 2025

@pzjp

Recalling my experience with pi-Base entries, I'm surprised with the thoroughness of the review process. :)

Some of the entries in pi-base were added a long time ago, when there was not as much scrutiny. In the early days, I heard that there was even a topology class of undergraduates where the students edited pi-base, which explains some of the sloppiness (although there have been sloppy entries added later on also :-) ). Anyway, I hope you don't mind. I think that by making the entries as mathematically (and grammatically) correct as possible, pi-base will become a great resource that people can reliably make use of.

pzjp and others added 4 commits January 18, 2025 08:50
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
Co-authored-by: Patrick Rabau <[email protected]>
@prabau prabau merged commit 87bd795 into main Jan 18, 2025
1 check passed
@prabau prabau deleted the pzjp/s135-jan25 branch January 18, 2025 19:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants