pi-base
Property suggestion: 'Has a cofinite topology'
I was wondering what the community thinks about the following property?
- 'Has a cofinite topology' (S15 + S16, and the finite discrete spaces)
I think many of the traits for S15 and S16 will become theorems about 'Has a cofinite topology', so this should hopefully reduce the number of files overall. Hypothetically, having this let's a user reason about cofinite spaces not hardcoded into the pi-base, since there are various properties corresponding to conditions on cardinality.
What actually got me thinking about this is that while working on adding theorems for P199 (Contractible), I found a nice blog post which shows that nonempty + has cofinite topology + path connected => contractible. S15 is not path connected, so to add the theorem from this blog we only have to add it as a trait to S16, but I thought it could still be worth having a discussion about.
And just so I don't go asking this same question 3 more times, I also see the following similar properties (which determine a list of spaces parameterized by cardinality). Would it be desirable to add these in over time?
- 'Has a cocountable topology' (S17 + others)
- 'Has a particular point topology' (S7, S8, S9, S10)
- 'Has an excluded point topology' (S10, S11, S12, S13)
I think it's worth drafting this out and see how it looks - I could see e.g. S7, S8, S9, S10 being just "has a particular point topology" plus cardinality properties, and then everything else is a theorem consequence. However I could also see us taking up the theorem namespace for results that might be just as easily asserted directly as traits on those handful of examples.
Hmm, I understand what you are trying to do. Not completely sure it's worth it though. I'll try to think some more about it.
It's not a bad idea, but those topologies could also all be fully characterized by a small set of broader properties. If there are theorems that apply to those special cases exclusively and no others, I see some value in adding the properties, but I'm uncertain otherwise.
Using properties in the database already, I know the following is true (disregarding the empty space):
- Particular point topology = P126 Door ∧ P39 Hyperconnected ∧ P90 Alexandrov
- Excluded point topology = P126 Door ∧ P40 Ultraconnected
For the other two, I'm not sure there's any existing complete characterization. P168 ωC gets us part of the way there for the cofinite topology. I had been contemplating the idea of a "co-cardinality topology" property (i.e. spaces where any self-bijection is continuous) but wanted to establish some intermediate results on n-homogeneity and such first.
but those topologies could also all be fully characterized by a small set of broader properties.
Is there any way to determine from pi-base that a combination of properties uniquely characterizes a space? Otherwise adding Particular point topology hypothetically increases the utility of the website, because someone could use pi-base to learn that fact. I.e., on the explore page I type in
- "Particular point topology + ~Door" (and it tells me this is impossible by some sequence of facts)
- "Particular point topology + ~Hyperconnected"
- "Particular point topology + ~Alexandrov" and I also type in
- "Door + Hyperconnected + Alexandrov + ~Particular point topology". (And maybe your tools, which I haven't really explored, make this process easier?)
Yeah, there is a whole multi-dimensional cardinal scale of properties one could come up with. Others would be "generalized Fort/Fortissimo spaces" like in https://math.stackexchange.com/questions/4833761, or $(\alpha,\beta)$-compact/Lindelof, etc, etc.
It is really wise to add all these as a generalized property? That will lead to a proliferation of theorems, most of which will only be used to automate the deduction of some traits for two or three pi-base example spaces, and won't be used for much of anything else. Right now, "cofinite topology" in pi-base is only that topology on a countable set and on the reals. And similarly for cocountable topology, etc. Somehow it does not seem very worthwhile, while one could instead spend time adding more substantial examples and properties and theorems from the literature not already in pi-base. But I could be convinced otherwise.
Really, "particular point topology" is a pretty basic example, or rather set of examples (all combined as a group with the same explanations on page 44 of Steen & Seebach). I am not sure there is a need to help people explore this much further than they can already do themselves with pi-base + pen & paper + book.
Somewhat related to the current topic. Some spaces are uniquely characterized by a set of properties. See chapter f-10 in Encyclopedia of general topology.
For example, we already gave two of them for the rational numbers (https://topology.pi-base.org/spaces/S000027), including "Every countably infinite, metrizablespace without isolated point is homeomorphic to $\mathbb Q$".
Since all our properties are topological (i.e. preserved by homeomorphism), we could introduce a "convenience property" like "homeomorphic to the $\mathbb Q$". It's a little extreme, but would be an abbreviation for a set of other properties. And that would allow to deduce that a bunch of other spaces are homeomorphic to the rationals. Instead we listed a few examples directly in the README page.
I am not advocating to do the above, just exploring the possibilities here.
Similarly about "particular space topology" ...
Suggestion for better way:
Maybe if we had a more powerful way to model things, we would have spaces and "super-spaces"/"meta-spaces"(= grouping of spaces with similar properties) with properties asserted in general for the super-spaces, and then particular spaces being specializations of a specific super-space (like in object oriented programming). That would be a better way to organize things than with theorems.
I'm reminded of a conversation we had a year or so (?) ago: being homeomorphic to a topological space is itself a topological property. In that perspective, a "property" is a class of topological spaces, and a "space" is a class of spaces that happens to be pairwise homeomorphic. Then both "theorems" and "space/property traits" are just assertions about subclasses.
Yeah, I was thinking about that too.
In any case, I think an "object-oriented" proposal for organizing some spaces would be of benefit. Trying to limit the amount of work in the infrastructure, we would not introduce yet another namespace to parallel spaces, but just mark some spaces with a special attribute to indicate they are a type of generic instance (in the metadata, something like "is_generic: true"), and also label the name accordingly. For example:
- "[Generic] Particular point topology" (uid = S...)
- "[Generic] Excluded point topology"
The contents for these generic spaces would be README file as usual, plus asserted traits to cover all the traits valid across all spaces for that class.
Then we'd have instantiations of these. For example:
- "Particular point topology on $\omega$" (with "parent_uid: ..." in the metadata)
- etc.
These latter spaces would contain additional traits as necessary, together with all the traits from the parent.
As far as implementation goes, the part requiring more work would be carrying over the traits from the parent. I don't know the internals of the web engine for pi-base, but it seems it would be a localized pre-processing step to carry over the parent traits to the children spaces, and not much else would have to change.
Comments?
This all sounds reasonable. I don't even think we need is_generic: true; while for a while we were pushing for well-defining each space up to homeomorphism, I think it's a fine pivot to simply say that every S[id] is actually a class of topological spaces that hold certain properties, and in some (many) cases they will be pairwise homeomorphic, in some cases they won't, and in some models of set theory they will be empty (e.g. we could add the Suslin line). Then we could have a specifies: attribute to list every class of more general spaces a space/subclass belongs to.
But as for when this can be implemented, it's unclear.
Somewhat related to the current topic. Some spaces are uniquely characterized by a set of properties. See chapter f-10 in Encyclopedia of general topology.
For example, we already gave two of them for the rational numbers (https://topology.pi-base.org/spaces/S000027), including "Every countably infinite, metrizablespace without isolated point is homeomorphic to Q ".
Since all our properties are topological (i.e. preserved by homeomorphism), we could introduce a "convenience property" like "homeomorphic to the Q ". It's a little extreme, but would be an abbreviation for a set of other properties.
This idea is inspired by this quote and @danflapjax's recent PR https://github.com/pi-base/data/pull/1058. Each space (and generic space, based on @prabau's other comment) could automatically carry a dummy property with the same label as the space. This dummy property semantically means 'Is homeomorphic to' (or, 'is homeomorphic to an element of the family of the generic-space'). It is allowed to exist in the 'then:' block of the propositions, or in the 'if:' block as negation. That would allow us to include topological characterization theorems in the pi-base logic. (You would end up changing how the Empty property works, and maybe some others. If the generic-space idea is added, you would end up changing the Indiscrete property, and some of the others already mentioned.)
One question I'm not sure about is how pi-base should make the various characterizations known to pi-base visible to the user. I'm guessing a feature which let's the user automatically see how pi-base can distinguish two chosen spaces will one day be added, and maybe that could display any known topological characterizations.
An aesthetic pitfall with this is, maybe it's not very common that a space is actually fully topologically characterizable in pi-base. For some of the most important spaces there are topological characterizations (e.g., of the real line), so maybe that's enough to justify it.
Once upon a time, I wanted every space to be defined up to homeomorphism. Then at some point we decided it was reasonable to leave some ambiguity (e.g. there are $2^c$-many spaces satisfying https://topology.pi-base.org/spaces/S000057 and there's no good reason to further specify the definition).
But at some point, if Sxyz isn't unique up to homeomorphism, then it's really just another topological property. And of course even if it is unique, that's still a property.
So a model that respects this is reasonable. I'm giving a talk at the JMM on the pi-Base next month in which this will be my open question: what's the right way to approach this? Because I'm not sure it's clear yet, and even if it is, the right people will need the right amount of time to implement it.
Wow that sounds like a really cool talk. Any chance it'll be videotaped?
The spaces based on non-principal ultrafilters are probably also good to keep in mind for this: S000145. I studied ultrafilters in my logic class in the long long ago times, but I assume S145 is never going to be factored into a single homeomorphism class.
So the idea of generic spaces / families is sort of already implicit in pi-base. Though when reading 'generic space' I have something like a C++ template / C macro in mind, and a 'family' is any space which is not distinguishable from some huge collection of spaces, for which any single example is as good as all the others.
Obnoxiously, the AMS and MAA don't have recording or virtual support for their national meetings (outside a few plenary talks, which I definitely don't make the cut for!). Here's the abstract, whatever that's worth: https://meetings.ams.org/math/jmm2025/meetingapp.cgi/Paper/38809
I like the idea that spaces might inherit from other spaces as in an OO approach. Then I guess things could go two ways: we can assert traits on the broader space-class, and if it is inherited by two different space[-classe]s that different on a property, the broader space-class reports that it's not determined.