pi-base
Generalizing theorems by Kolmogorov quotient, automatically
One things noticeable is that, we can check all the theorems and strengthen it to the version that could be pass Kolmogorov quotient, that will be good for spaces like S18 whose Kolmogorov quotient has more property can be deduced.
For example, clearly $T_1$ in T381 can be weaken to $R_0$ and thus we would know {S18|¬P158}, etc.
Maybe it can be proposed in a separated issue/PR. Maybe a huge work.
Originally posted by @yhx-12243 in https://github.com/pi-base/data/issues/1166#issuecomment-2564602608
I realized after thinking about this comment that this process can be automated: given the Kolmogorov quotient, or indeed any function from the class of topological spaces to itself, we can list out the preimage of each property (or at least upper and lower bounds). Since preimage distributes over intersection and complement, we can use this to map each theorem to another valid theorem, then the deduction engine can check which of these are already known to the database.
Of note, the Kolmogorov quotient is a particularly nice sort of function for this purpose, being a reflector for the subcategory of $T_0$ spaces. This allows us better fallback upper and lower bounds for preimages, as well as the possibility of checking whether adjointness is known. Hypothetically any sort of function could work, however, such as, say, one-point compactifications.
I began the process of listing preimages in this spreadsheet. Beyond the Kolmogorov quotient/$T_0$ reflection, I also included columns for the $R_0$ coreflection/refinement, $T_1$ reflection/quotient, and $T_1$ coreflection/refinement, which are less fleshed out. I set it so that anyone can make suggestions on the spreadsheet, so feel free to suggest results that I may have missed or correct errors, as there are a lot of properties to look over. I should also probably add upper or lower bounds when no exact preimage exists, so feel free to suggest those as well.
The next step is to write some code to check for novel theorems, which I don't anticipate being much of a challenge.
Using the mappings in the above spreadsheet, I found that the following theorems can be generalized using the T0 quotient. I will package up and share my code in a bit.
| uid | generalization | by names |
|---|---|---|
| T28 | P134 ∧ P19 ∧ P28 ⇒ P11 | R1 ∧ Countably compact ∧ First countable ⇒ Regular |
| T374 | P135 ∧ P28 ∧ P159 ⇒ P111 | R0 ∧ First countable ∧ k-Menger ⇒ Hemicompact |
| T381 | P135 ∧ P158 ⇒ P111 | R0 ∧ Markov k-Rothberger ⇒ Hemicompact |
| T395 | P147 ∧ P18 ∧ P134 ⇒ P13 | P-space ∧ Lindelöf ∧ R1 ⇒ Normal |
| T399 | P147 ∧ P135 ∧ P23 ⇒ P185 | P-space ∧ R0 ∧ Weakly locally compact ⇒ Partition topology |
| T485 | P134 ∧ P16 ∧ P36 ⇒ P189 | R1 ∧ Compact ∧ Connected ⇒ σ-connected |
| T486 | P23 ∧ P36 ∧ P41 ∧ P134 ⇒ P189 | Weakly locally compact ∧ Connected ∧ Locally connected ∧ R1 ⇒ σ-connected |
| T516 | P11 ∧ P183 ∧ P28 ⇒ P121 | Regular ∧ Has a countable k-network ∧ First countable ⇒ Pseudometrizable |
| T517 | P11 ∧ P183 ∧ P23 ⇒ P121 | Regular ∧ Has a countable k-network ∧ Weakly locally compact ⇒ Pseudometrizable |
| T533 | P182 ∧ P23 ∧ P134 ⇒ P27 | Has a countable network ∧ Weakly locally compact ∧ R1 ⇒ Second countable |
There is a very easy way to make any topological space to be completely regular without modifying its continuous functions.
Namely, given a topological space $(X, \tau)$ simply let $\tau_c$ to be topology generated by cozero sets of $\tau$. Then as can be seen, if $f:(X, \tau)\to\mathbb{R}$ is continuous, then $f^{-1}(U)$ is a cozero set for any open $U\subseteq \mathbb{R}$, and so $f:(X, \tau_c)\to\mathbb{R}$ is continuous, with the converse being obvious.
This might be not as useful as Kolmogorov quotient, but it's still a very easy construction which would preserve some of the properties involving cozero sets, so easy that I thought I had to mention it.
This can of course be then combined with Kolmogorov quotient to lend a Tychonoff space.
So the completely regular spaces form a reflective subcategory of the category of topological spaces. The reflection of $(X,\tau)$ is the space $(X,\tau_c)$.
As of a few weeks ago @danflapjax is now my student at South! So today we discussed this a bit in my office as something they're interested in dusting off to both improve the pi-Base and serve as a chapter of their thesis.
I like the idea of an omnibus PR incorporating these improvements, but rather than reviewing the new theorems themselves, we will need to review the mathematics and code used to implement them.
This seems deeply related with meta-properties (see #1071), and implementation attempts should take into account whether we want to handle something more than just Kolmogorov quotients.
