Add realcompactification of Rudin's space and basic properties #1153
Conversation
|
It seems that you forgot to add ~T5. |
Co-authored-by: yhx-12243 <yhx12243@gmail.com>
Yes, although #1135 is still open, so I'm not sure if I want to add this in this PR |
…data into realcomp-of-rudin-space
|
I thought "realcompactification" always refers to Hewitt realcompactification. Is there another one? If not, the shorter name "Realcompactification of Rudin's Dowker space" would be better. |
|
@prabau Just as "compactification" doesn't always refer to Stone-Cech compactification, similarly "realcompactification" doesn't always refer to Hewitt realcompactification. |
Co-authored-by: yhx-12243 <yhx12243@gmail.com>
Co-authored-by: yhx-12243 <yhx12243@gmail.com>
|
@yhx-12243 hi, are you going to review this PR? |
|
@felixpernegger do you want to review this PR? |
|
|
@felixpernegger I think "assigning" someone to a PR makes that person responsible for make changes. Instead, you probably want to make yourself a reviewer. |
felixpernegger
left a comment
felixpernegger
left a comment
There was a problem hiding this comment.
Seems good in general!
There was a problem hiding this comment.
I don't know any of the terms here so I cannot review this, but since the proof is so short, if you think it's fine, then it should be okay.
There was a problem hiding this comment.
I do think its fine. I can explain any of the terms you don't know if needed
Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
Co-authored-by: Felix Pernegger <s59fpern@uni-bonn.de>
|
the link I complained about takes me to this website maybe you are logged in or something? |
|
@felixpernegger that's odd. I'm not logged in, no |
|
@prabau could you look at this? We need help with this link issue |
|
maybe just use the zb reference, I think thats our standard way now anyways: |
|
@felixpernegger does that work for you? |
|
If I go tothe zb reference, the first "full text" link again just takes me to the polish math institute, but the second one (the eu one) works. |
|
I have no idea why you have no access to the articles of the Polish site. Might be issue with location |
|
but really, just use the zbmath reference always. Less risk of links breaking also. |
felixpernegger
left a comment
felixpernegger
left a comment
There was a problem hiding this comment.
This looks good to me now. Since this PR adds a new space (and has been open for over a year!) it would be nice if @prabau or @yhx-12243 can take a quick look before we merge this.
|
remember to delete everything below the title if you merge this |
sorry what do you mean with that? |
|
@felixpernegger you want to delete everything in Extended description when merging. This is not something people on github generally want, but people on pi-base want this. The explanation given to me is that this is useless data they don't want to see |
I'll take a look later today. |
|
S208 README: The second paragraph says that Rudin's paper shows that Added later: I saw now that it's mentioned as the space |
|
@prabau should be all I think |
|
I did not check the proof in the paper that |
Co-authored-by: Patrick Rabau <70125716+prabau@users.noreply.github.com>
|
@prabau I don't remember exactly but I think that specific trait is pretty hard to prove so you probably would be better off not reading it. Or maybe it was realcompactness. Either way, maybe I should. Those are notes though |
|
I have added a link to Hart's notes and approved. Feel free to merge if you agree. |
See #1139
While I'm not confident about Rudin's original proof that this space is ultraparacompact, I am confident that it is ultraparacompact. See those notes by K. P. Hart (maybe I should add those as a reference?).