Adds P201 'Has a generic point'

[GeoffreySangston]

We're breaking up #847 into multiple pull requests, as discussed in #849 (comment)

I noticed that Hartshorne uses "generization" instead of "generalization" (which appears on Wikipedia).

[GeoffreySangston]

I think I should remove P39 (Hyperconnected) from S144 (Diamond poset), i.e. ( https://topology.pi-base.org/spaces/S000144/properties/P000039 ), and add P201 (Has a generic point) to S144. The manual proof of P39 is exactly that there exists a generic point.

[danflapjax]

T594 is currently contradictory for the empty space btw; it should be Quasi-sober ∧ Hyperconnected ∧ ¬Empty ⇒ Has a generic point.

[GeoffreySangston]

T594 is currently contradictory for the empty space btw; it should be Quasi-sober ∧ Hyperconnected ∧ ¬Empty ⇒ Has a generic point.

Just checking, but is there a tool / warning for catching that kind of thing automatically? I noticed after you pointed it out that the values of the properties on the Empty space page were replaced with ? marks (I didn't check if values in other places were replaced with ? marks though.)

[prabau]

I noticed that Hartshorne uses "generization" instead of "generalization" (which appears on Wikipedia).

For what it's worth, the Stacks project also uses "generalization": https://stacks.math.columbia.edu/tag/0060

[prabau]

Added some formatting changes, but feel free to edit further if desired.

[prabau]

T594: Phrasing things in a positive fashion seems more natural:
[quasi-sober + hyperconnected + nonempty ==> has generic point]

Also, the following result cannot be deduced right now, but would be helpful:
[has a generic point + T1 ==> not has multiple points]
(would imply for example that S16 (cofinite topology on the reals) does not have a generic point)

or maybe the contrapositive would be fine:
[T1 + multiple points ==> not has generic point]

[prabau]

should be single braces {S10}. Or just say "This space has a particular point topology ..."

[prabau]

I think I should remove P39 (Hyperconnected) from S144 (Diamond poset), i.e. ( https://topology.pi-base.org/spaces/S000144/properties/P000039 ), and add P201 (Has a generic point) to S144. The manual proof of P39 is exactly that there exists a generic point.

Note that there is no redundancy as pi-base now knows already that there is a generic point for S144:
https://topology.pi-base.org/spaces/S000144/properties/P000201
But if you want to do the change, that would probably be even clearer.

[danflapjax]

Also, the following result cannot be deduced right now, but would be helpful:
[has a generic point + T1 ==> not has multiple points]
(would imply for example that S16 (cofinite topology on the reals) does not have a generic point)

Even better would be Has a generic point + R0 => Indiscrete.

Another straightforward theorem is Has a generic point + Homogeneous => Indiscrete.

Just checking, but is there a tool / warning for catching that kind of thing automatically? I noticed after you pointed it out that the values of the properties on the Empty space page were replaced with ? marks (I didn't check if values in other places were replaced with ? marks though.)

What tipped me off is that the Advanced page said there were way fewer traits than there ought to be. I then used the tool of mine linked to from that same page to look at which spaces had contradictions, but it's not great for seeing what the contradiction actually is at the moment. It would be nice if the Advanced page just listed which spaces had contradictions when that happens.

[GeoffreySangston]

Perhaps for a future commit... Since I know nothing about quasi-sober spaces, I was thinking it might be nice to include an example satisfying '~quasi-sober + Hyperconnected + Has a generic point' (for which none exist in pi-base presently, or perhaps one does, but is not detected).

[prabau]

The new T596 is nice. Now allows to deduce that S42 (right ray topology on the reals) has no generic point:
https://topology.pi-base.org/spaces/S000042/properties/P000201

Now all that remains is replacing T595 with @danflapjax suggestion with R0.

[GeoffreySangston]

I briefly looked over the remaining spaces for which pi-base is currently agnostic about 'Has a generic point'.

I believe the following should 'Have generic point' == true

• {S44}. E.g., $\frac{1}{4}$.
• {S45}. E.g., 0
• {S199}. The 0 ordinal is contained in every left ray.

And the following should 'Have generic point' == false

• {S46}
• {S200}. Any point is not contained in some right ray.

This one seemed more complicated to me so I haven't thought it it through yet.

• {S48}

[prabau]

Looks really good now. I am ready to approve.

@danflapjax Anything else you want here? If not, I'll approve.

Alternatively, you can approve and merge. But I have a pet peeve here. When you do "squash and merge", can you please wipe out the detailed list of intermediate commits and only leave the title. Steven does not think it's worth to be bothered by this, but if you leave the detailed list, doing git log on the command line gives a ridiculously long list of little commits that are completely irrelevant and distracting. All that matters is the combined commit from the title. If anybody really cares about the details of the individual commits, they will always be accessible from the PR page.
See the explanation and screenshots at #779 (comment).

[prabau]

@GeoffreySangston Let's get this out already. You can do more as suggested in a separate PR.