Topological inductive definitions

DOI10.1016/J.APAL.2011.12.005MaRDI QIDQ450944zbMATH OpenOpenAlexFDO

Authors Giovanni Curi

Publication date 26 September 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.apal.2011.12.005

zbMATH Keywords

constructive set theory inductive definitions point-free topology

Mathematics Subject Classification ID

Other constructive mathematics (03F65) Frames, locales (06D22) Product spaces in general topology (54B10)

Review text

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.NEWLINENEWLINEThe 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.NEWLINENEWLINEIn 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\).NEWLINENEWLINEThe paper concludes presenting a few applications: a point-free version of the Tychonoff embedding theorem, and some set-representation theorems.NEWLINENEWLINEThis article is of prime interest for every mathematician interested in the categorical description of formal topology in constructive and predicative terms.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Topological inductive definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q450944)