Fornasiere, Damiano (2019) Per questo documento il full-text online non disponibile. ## AbstractThe present thesis principally explores two ways for founding general topology in a constructive framework, both predicative and impredicative. The paths followed vary from a more classical one - through locale theory - to a more recent one, through positive topologies. All the work is supposed to be done generally enough to think that can be internalized inside a topos, therefore the first result exhibited asserts that a generic topos naturally has an intuitionistic structure. The main purpose is to understand how pointless topologies are related to topological spaces and whether the former can be seen as generalizations of latter. This aim is pursued trying to give the tools intended to prove two theorems that link these two worlds. We will analyze how the results obtained vary changing the underlying logic. We begin by showing some results in elementary topos theory, principally referring to (Borceux, 1994), (MacLane, 1971), (Mahany, 2012) and (Palmgren, 2009). The main goal here is to show that power objects PX in a topos naturally are internal Heyting algebras, while the subobjects Sub_{E}(X) are external Heyting algebras, and both often fails to be Boolean algebras. Then, motivated by the just seen emergence of Heyting algebras, referring to (Johnstone, 1982) and (MacLane & Moerdijk, 1992), we generalize constructively (but impredicatively) the notion of topological space, introducing and exploring the category *Loc* of locales, in order to prove the well-known theorem for which an adjunction *Top* - *Loc* exists. Afterwards, the third part of this thesis is first committed to becoming acquainted with the categories of *BP* of basic pairs and *BTop* of basic topologies introduced in (Sambin, 2019b), in order to eventually find a suitable environment to generalize topological spaces in a predicative setting. Finally we show the proof appeared in (Sambin, 2019a) which proves that there is an embedding *BP* → *BTop* which restricts to an embedding *CSpa* → *PTop*. These last two categories somehow constructively generalize *Top* and *Loc* respectively. Concluding, referring to (F. Ciraulo, 2019) and (Ciraulo & Vickers, 2018), we will show how building an adjunction between *Top* and *PTop *allows to factorize *Top* - *Loc* through the newly constructed adjunction.
Solo per lo Staff dell Archivio: Modifica questo record |