Cosheaves and connectedness in formal topology

The localic definitions of cosheaves, connectedness and local connectedness are transferred from impredicative topos theory to predicative formal topology. A formal topology is locally connected (has base of connected opens) iff it has a cosheaf π0π0 together with certain additional structure and properties that constrain π0π0 to be the connected components cosheaf. In the inductively generated case, complete spreads (in the sense of Bunge and Funk) corresponding to cosheaves are defined as formal topologies. Maps between the complete spreads are equivalent to homomorphisms between the cosheaves. A cosheaf is the connected components cosheaf for a locally connected formal topology iff its complete spread is a homeomorphism, and in this case it is a terminal cosheaf.A new, geometric proof is given of the topos-theoretic result that a cosheaf is a connected components cosheaf iff it is a “strongly terminal” point of the symmetric topos, in the sense that it is terminal amongst all the generalized points of the symmetric topos. It is conjectured that a study of sites as “formal toposes” would allow such geometric proofs to be incorporated into predicative mathematics.

► Transfers results from impredicative topos theory to predicative formal topology.
► Gives a new definition of local connectedness using cosheaves.
► Introduces techniques of geometric logic into the study of cosheaves.
► Begins a new research program: the “formal topos”.
► Exemplifies it with the symmetric topos.