Topological inductive definitions (Q450944)

The concept of locale is a satisfactory substitute for the notion of topological space in an intuitionistic framework. However, the notion of locale is unsatisfactory in the framework of predicative mathematics. For this reason, the categories \textbf{FSP} of formal spaces and \textbf{FSP}\(_i\) of inductively generated formal spaces have been introduced and studied. These categories are equivalent to the category of locales in an impredicative setting, but both are incomplete in some sense. The article aims at proposing another category, \textbf{ImLoc}, the category of \textit{imaginary} locales to circumvent the problems of \textbf{FSP} and \textbf{FSP}\(_i\) in the predicative setting. It turns out that \textbf{ImLoc} contains both \textbf{FSP} and \textbf{FSP}\(_i\) as subcategories, and it is equivalent to the categories of locales in the intuitionistic impredicative framework, thus meeting the initial objective. In simple terms, \textbf{ImLoc} is the opposite of the category of frame presentations, which are structures given by a preordered set over the base of the intended space together with a generalised covering system. The result is that a frame presentation does not always allow to define a concrete frame meeting its structure, but it always allows to identify a structure of opens that may be realised by a concrete frame. For this reason, \textbf{ImLoc} contains enough objects and continuous functions between them to be complete as a category, thus fixing the problem of \textbf{FSP}, and to represent all the formal spaces of interest, overcoming the difficulties of \textbf{FSP}\(_i\). The paper concludes presenting a few applications: a point-free version of the Tychonoff embedding theorem, and some set-representation theorems. This article is of prime interest for every mathematician interested in the categorical description of formal topology in constructive and predicative terms.