2017/07/18 by Tatsuji Kawai, Kawai, Tatsuji
Computer Science · Mathematics · #03F60 #06B35 #06D22 #54B20 #Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #cs.LO #math.CT #math.LO #msc:03F60 #msc:06B35 #msc:06D22 #msc:54B20
paper · pdf · doi:10.48550/arxiv.1709.06403
37 pages
arxiv created 2017/07/18 · arxiv updated 2017/09/20
We give geometric characterisations of patch and Lawson topologies in the context of predicative point-free topology using the constructive notion of located subset. We present the patch topology of a stably locally compact formal topology by a geometric theory whose models are the points of the given topology that are located, and the Lawson topology of a continuous lattice by a geometric theory whose models are the located subsets of the given lattice. We also give a predicative presentation of the frame of perfect nuclei on a stably locally compact formal topology, and show that it is essentially the same as our geometric presentation of the patch topology. Moreover, the construction of Lawson topologies naturally induces a monad on the category of compact regular formal topologies, which is shown to be isomorphic to the Vietoris monad.