Skip to content

S60: homogeneity, cut points and more#1170

Merged
prabau merged 9 commits intomainfrom
pr1164
Jan 2, 2025
Merged

S60: homogeneity, cut points and more#1170
prabau merged 9 commits intomainfrom
pr1164

Conversation

@pzjp
Copy link
Copy Markdown
Collaborator

@pzjp pzjp commented Dec 29, 2024

A few more missing traits for Pointed rational extension of R:

Then P28 and P46 are redundant. Should I remove them simultaneouslty?

@pzjp pzjp marked this pull request as ready for review December 30, 2024 10:00
@prabau
Copy link
Copy Markdown
Collaborator

prabau commented Jan 1, 2025

FYI, several of the previously asserted traits were just referring to the "General Reference Chart" at the end of Steen & Seebach. Not necessarily to be done in this PR, but we'd like to replace this at some point with a proper justification. (There have even been cases of a few errors in that table.)

@prabau
Copy link
Copy Markdown
Collaborator

prabau commented Jan 1, 2025

And yes, it's fine to do the cleanup of some of the redundant traits at the same time.

@pzjp
Copy link
Copy Markdown
Collaborator Author

pzjp commented Jan 1, 2025

I've noticed those "general reference chart" entries and was actually thinking that these should be explained further.
For this PR the cleanup seems enough, though.

@prabau prabau self-requested a review January 1, 2025 18:53
@prabau
Copy link
Copy Markdown
Collaborator

prabau commented Jan 1, 2025

P205 (cut point space): We should also mention that $X$ is connected, which is part of the definition of cut point space.

Now, P36 (connected) should be a consequence of P205, so what we should do is add the reasoning for connected to P205 and remove the P36 trait file, which is redundant. (That also avoid circular reasoning.)

The current reasoning for connected refers to item 8 of S&S example 68. But that's a confusing justification for it. Instead, it should refer to item 4 of that example (which is what item 8 implicitly uses to show something else).

Summary: add something like the following to P205:

$X$ is {P36}: see item #4 for space #68 in {{doi:10.1007/978-1-4612-6290-9_6}}.

@prabau prabau merged commit 3f74c4f into main Jan 2, 2025
@prabau prabau deleted the pr1164 branch January 2, 2025 19:24
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.

2 participants