Generalizing theorems by Kolmogorov quotient, automatically

[danflapjax]

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 $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.

[danflapjax]

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

[Moniker1998]

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]

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)$.