Positive Topologies and Formal Maps: Pointfree Topology

Abstract This chapter shows that the transparent method to introduce notions of pointfree topology leads to the category of positive topologies and formal maps PTop. It is the subcategory of BTop obtained by adding consideration of convergence, just as CSpa is obtained from BP. In the example of trees, two natural axioms generate a positive topology whose formal open and closed subsets are Brouwer’s inductive bars and spreads, respectively. This makes methods of proof theory available to study them. pointfree versions of Baire and Cantor space are special cases. The embedding of BP into BTop restricts to an embedding of CSpa into PTop, thus proving Grothendieck’s claim that pointfree topology generalizes pointwise topology. Finally, a single functor embeds locales and formal topologies into PTop. All this shows that a more general, expressive, and intuitive version of constructive pointfree topology is achieved.