pi-base / data

A community database of topological counterexamples
https://topology.pi-base.org/
Creative Commons Attribution 4.0 International
72 stars 25 forks source link

Property suggestion: 'Has a cofinite topology' #883

Open GeoffreySangston opened 2 weeks ago

GeoffreySangston commented 2 weeks ago

I was wondering what the community thinks about the following property?

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?

StevenClontz commented 2 weeks ago

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.

prabau commented 2 weeks ago

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.

danflapjax commented 2 weeks ago

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):

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.

GeoffreySangston commented 2 weeks ago

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

prabau commented 2 weeks ago

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.

prabau commented 2 weeks ago

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.

prabau commented 2 weeks ago

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.

StevenClontz commented 2 weeks ago

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.

prabau commented 2 weeks ago

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:

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:

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?

StevenClontz commented 2 weeks ago

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.