Repository navigation
Generalizing theorems by Kolmogorov quotient, automatically #1198
Description
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 #1166 (comment)
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
I began the process of listing preimages in this spreadsheet. Beyond the Kolmogorov quotient/$T_0$ reflection, I also included columns for the
The next step is to write some code to check for novel theorems, which I don't anticipate being much of a challenge.
Activity
danflapjax commentedon Jan 24, 2025
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.
Moniker1998 commentedon Feb 14, 2025
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.
prabau commentedon Feb 16, 2025
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)$ .
StevenClontz commentedon Sep 10, 2025
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.
pzjp commentedon Sep 21, 2025
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.