pi-base
Completing relative prime topology (S52)
Correctness is passed. Maybe there are other writing issues/explanations, waiting for @prabau to double check later.
I replaced P57 (countable) with P181 (countably infinite). This is preferable, as it is the same justification and gives a cleaner derivation of the non-asserted property.
P110: things don't quite make sense here. $x$ should be something else? Also, $U_a(b)$ cannot be a set of members of a cover ? Can you explain what you are trying to say?
P110: things don't quite make sense here. x should be something else? Also, U a ( b ) cannot be a set of members of a cover ? Can you explain what you are trying to say?
𝑥 here means 𝑎. For a pair of fixed parameter 𝑎, 𝑏: 𝒰 is indeed a cover and st(𝑎, 𝒰) = 𝑈ₐ(𝑏). Such parameter pairs (𝑎, 𝑏) are countable.
P110: things don't quite make sense here. x should be something else? Also, U a ( b ) cannot be a set of members of a cover ? Can you explain what you are trying to say?
𝑥 here means 𝑎. For a pair of fixed parameter 𝑎, 𝑏: 𝒰 is indeed a cover and st(𝑎, 𝒰) = 𝑈ₐ(𝑏). Such parameter pairs (𝑎, 𝑏) are countable.
I know that's what he is trying to say. But it needs to be rewritten to be made comprehensible.
In particular, \{U\in\mathscr{U}:x\in U\} is a subcover of a cover $\mathscr U$, and strictly speaking, that can't be the same as U_a(b), which is a subset of $X$. Is a bigcup missing somewhere, maybe?
For P110 (developable), the argument used here can changed and made into a separate theorem: [ second countable + countable + T1 => developable ].
We should even be able to replace T1 with the more general R0.
That will show that 11 more spaces are in fact developable: https://topology.pi-base.org/spaces?q=second+countable%2Bt1%2B57%2B%3FDevelopable
Can you make a separate PR for this? (please not in the same PR)
@felixpernegger No need to add \!. My example of \! is to adjust the space between \left( subtly.
Im a little bit unhappy with how the definition of s looks but I dont see a nice way around it
P82: I have to admit that I find this a little daunting to read. Did not spend my full energy trying to get into the details, but this seems too intricate for a self-contained justification in pi-base.
On the other hand, look at Prop. 3.2 in the Banakh et al. paper https://dml.cz/handle/10338.dmlcz/147548 From that, every nonempty open set contains an open subset that is not regular. What do you think of making use of that?
Disclaimer: I haven't had the time yet to read it in detail. But if we are going to use that, it would be good that at least one of us convincingly verifies the argument for themselves.
In fact the argument in that paper is more complex than this. However, using a existing justification is a good idea. I think we can keep it all, for some readers only need to an assertion that it is right. (I think the currently proof of S52|P82 is not hard to follow)
In fact the argument in that paper is more complex than this. However, using a existing justification is a good idea. I think we can keep it all, for some readers only need to an assertion that it is right. (I think the currently proof of S52|P82 is not hard to follow)
My argument feels a little bit math olympiad number theory style I guess haha.
For what its worth, I'm fine either way with how its handled.
Disclaimer: I haven't had the time yet to read it in detail. But if we are going to use that, it would be good that at least one of us convincingly verifies the argument for themselves.
FYI for countably many self continuous maps property, I quoted this paper but did not actually look at the proof. Might be a good idea to do that as well then.
Following @StevenClontz (References section in https://github.com/pi-base/data/wiki/Contributing), pi-base prefers to reference peer-reviewed publications when possible.
As for checking the results ourselves, as @Moniker1998 mentioned before, papers make mistakes. Unlikely in this case. But still, I personally think it's good if we can check the argument if the result is not too difficult.
@yhx-12243 If you really want to keep this more direct argument, I still think it's too intricate for pi-base. But we can have a question on mathse, see if people (not necessarily us) give a good answer, and refer to that.
@prabau The topologies on the integers are quite challenging, so I could check the proof but it'd take a while. Not surprised that @felixpernegger didn't check it. Still, I think there should be one or two people who read this before we add it. Trust but double check.
For P82 (locally metrizable), I checked Lemma 2.2 and Prop. 3.2 in the Banakh paper. That seems correct, well explained and clear to me, and really not that involved. So I would just refer to that for the fact that nonempty open subsets of $X$ are not regular. (Prop. 3.2 does not use the assumption $b\ge 2$ for the "regular" part of the result.)
I changed my proof for p82 to just refer to the paper now.
When this is done, one could start working on Kirch space. I think all the theorems are available, except countably many self continuous maps