Factorizing the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction through positive topologies (Q2238147)

The aim of formal topology is to develop topology in a constructive framework where ``constructive'' is meant here to include both intuitionistic and predicative. In formal topology, taking a predicative point of view, frames are objectionable. This is obvious in the special case of discrete spaces, for the discrete topology on a set \(X\) is its powerset \(\mathcal P(X)\) and that is not a legitimate set in predicative type theory. The predicative approach is compelled to use not the full topology but just a base: a generating set of opens so that all other opens are joins of basics. A deep rethinking of the foundations of constructive topology has brought G. Sambin to a two-sided generalization of the notion of a convergent cover. This structure can be enriched by means of a second relation, called a positivity relation, which is used to speak about some particular sub-topologies (overt weakly closed sublocales). This enrichment produces a larger category \(\mathbf{PTop}\) (positive topologies) in which the category \(\mathbf{Loc}\) of locales embeds as a reflective subcategory. The category of positive topologies generalizes that of formal topologies as introduced by \textit{G. Sambin} [in: Mathematical logic and its applications, Proc. Adv. Int. Summer Sch. Conf., Druzhba/Bulg. 1986, 187--204 (1987; Zbl 0703.03040)] which correspond to overt locales. In this paper, the authors show, firstly, that the caracterization of positive topologies as locales endowed with a suitable family of suplattice homomorphisms can be organized into a fibration arising from a doctrine over \(\mathbf{Loc}\) via the so-called Grothendieck construction (see, e.g. [\textit{B. Jacobs}, Categorical logic and type theory. Amsterdam: Elsevier (1999; Zbl 0911.03001)]). Secondly, they use this representation of \(\mathbf{PTop}\) to give an adjunction between the category \(\mathbf{Top}\) of topological spaces and \(\mathbf{PTop}\); in particular, the notion of sobriety provided by this adjunction coincides with the one introduced in [\textit{G. Sambin}, The basic picture and positive topology. Oxford University Press (to appear)], which is known [\textit{P. Aczel} and \textit{C. Fox}, Oxf. Logic Guides 48, 176--192 (2005; Zbl 1095.03073)] to be constructively weaker than the notion of sobriety provided by the usual \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction [\textit{P. T. Johnstone}, Stone spaces. Cambridge: Cambridge University Press (1982)]. Moreover, the \(\mathbf{Top}\)-\(\mathbf{Loc}\) adjunction can be factorized as the composition of the \(\mathbf{Top}\)-\(\mathbf{PTop}\) adjunction above and the reflection \(\mathbf{PTop}\)-\(\mathbf{Loc}\). Thirdly, as a by-product, the authors get the completeness and cocompleteness of the category \(\mathbf{PTop}\) and of the wider category \(\mathbf{BTop}\) of basic topologies, which can be similarly characterized as a Grothendieck construction over the category of suplattices. This completes the picture in [\textit{H. Ishihara} and \textit{T. Kawai}, Math. Struct. Comput. Sci. 25, No. 8, 1626--1648 (2015; Zbl 1362.03057)], where the pointwise counterparts of \(\mathbf{BTop}\) and \(\mathbf{PTop}\) were shown to be complete and cocomplete. Finally, they show that the well-known adjunction between \(\mathbf{Top}\) and \(\mathbf{Loc}\) factors through the constructed adjunction.