Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space

Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

Maximal Kolmogorov Subspaces of a Topological Space as Stone Retracts of the Ambient Space

Zbigniew Karno: Warsaw University, Bialystok

Summary.

Let $X$ be a topological space. $X$ is said to be {\em $T_{0}$-space}\/ (or {\em Kolmogorov space}) provided for every pair of distinct points $x,\,y \in X$ there exists an open subset of $X$ containing exactly one of these points (see [1], [9], [5]). Such spaces and subspaces were investigated in Mizar formalism in [8]. A Kolmogorov subspace $X_{0}$ of a topological space $X$ is said to be {\em maximal}\/ provided for every Kolmogorov subspace $Y$ of $X$ if $X_{0}$ is subspace of $Y$ then the topological structures of $Y$ and $X_{0}$ are the same.\par M.H.~Stone proved in [11] that every topological space can be made into a Kolmogorov space by identifying points with the same closure (see also [12]). The purpose is to generalize the Stone result, using Mizar System. It is shown here that: (1) {\em in every topological space $X$ there exists a maximal Kolmogorov subspace $X_{0}$ of $X$}, and (2) {\em every maximal Kolmogorov subspace $X_{0}$ of $X$ is a continuous retract of $X$}. Moreover, {\em if $r : X \rightarrow X_{0}$ is a continuous retraction of $X$ onto a maximal Kolmogorov subspace $X_{0}$ of $X$, then $r^{-1}(x) = {\rm MaxADSet}(x)$ for any point $x$ of $X$ belonging to $X_{0}$, where ${\rm MaxADSet}(x)$ is a unique maximal anti-discrete subset of $X$ containing $x$} (see [7] for the precise definition of the set ${\rm MaxADSet}(x)$). The retraction $r$ from the last theorem is defined uniquely, and it is denoted in the text by ``Stone-retraction". It has the following two remarkable properties: $r$ is open, i.e., sends open sets in $X$ to open sets in $X_{0}$, and $r$ is closed, i.e., sends closed sets in $X$ to closed sets in $X_{0}$.\par These results may be obtained by the methods described by R.H. Warren in [16].

Presented at Mizar Conference: Mathematics in Mizar (Bia{\l}ystok, September 12--14, 1994).