Vietoris and open maps
The topological analogue of the powerset monad is the Vietoris hyperspace. Given a (compact Hausdorff) topological space , we define to be the space of closed subsets of with the least topology containing The pointfree analogue was introduced by Johnstone. Given a frame , its Vietoris powerlocale is defined as the free frame on the set subject to the following equations
Johnstone then proved that, if is a compact Hausdorff space which is dual to the frame , then is also dual to .
The points of the pointfree Vietoris
In fact, Johnstone showed that the dual space of the Vietoris frame can be computed directly (and constructively) without talking about the points of . Assuming that is compact and regular and that is its topological dual, the Vietoris space is homeomorphic to the space where the topology is generated by the elements of the form for every . The intuition behind this is that instead of the space of closed set we have the space of opens and then the expressions and are just rewritten accordingly in the language of open sets.
What Johnstone does not emphasise is that the mapping extends to a functor (although, as I found much later, his Lemma 4.7 (ii) in Stone spaces gives a clue). Let be a frame homomorphism between two compact regular frames and let be the corresponding dual continuous map.
Then, as I showed in Section 4.4 of my thesis, the map sending to can be equivalently expressed as the map where is the right adjoint to , i.e. the localic map corresponding to .
Remark: A similar formula can be also used for stably compact frames. The only difference is that we need to take the dual topology into account. For details, see Remark 4.4.1 and Lemma 4.4.6 in my thesis.
It was proved by Celia Borlido and Mai Gehrke that the preimage mapping is continuous w.r.t. the Vietoris topology precisely when the underlying map is open:
Let be a continuous map between compact Hausdorff spaces. The following statements are equivalent:
- is an open map.
- is continuous.
- is continuous (where is the map ).
In the following I will give a pointfree proof of “(1) (2)”. Let us first recall recall some facts about open frame homomorphisms (note that the third characterisation has deep connections with logic):
Let be a frame morphism. Then, the following are equivalent:
- maps open sublocales to open sublocales
- is a Heyting algebra homomorphism
- has a left adjoint satisfying the Frobenius identity: .
- has a left adjoint satisfying the identity: .
If, moreover, is the dual frame homomorphisms of a continuous map between two spaces, then is open iff is open.
This means that if a frame homomorphism is open then it is both left and right adjoint: Recall also that, if is dual to a continuous map between compact Hausdorff spaces, then we know that the map corresponds to taking the preimage and corresponds to taking forward image . With this in mind, let us now state and prove the pointfree version of the implication “(1) (2)” in Theorem 1:
Let be an open homomorphism between compact regular frames. Then, seen as a map is continuous.
First we show that the preimage of , for , under the map is open: Next, recall that in a regular frame the pseudocomplement of can be equivalently expressed as . In other words, we have that iff .
In the rest of the proof we show that is equal to . Observe that Therefore, if then, because is compact and regular and because is a frame homomorphism, there exists an rather bellow (i.e. ) such that . Therefore Conversely, if , then for some rather below . Because is an open homomorphism, we see that (We used the Frobenius identity in the second “iff” and the fact that is a Heyting algebra homomorphism in the last “iff”).
Lastly, since is rather bellow , it follows that (and vice versa) and so . We have proved that if and only if , or in other words that is equal to .
Showing the opposite direction seems a bit more elaborate but I believe that it should be also doable. Assuming the Axiom of Choice we know that it is true as it follows from Theorem 1. Furthermore, the proof of the opposite direction is classically completely straightforward. Indeed, in Theorem 1, (1) => (2) follows automatically and to show (3) => (1) it is enough to observe that which is open by (2). Anyway, I’ll leave it for the next time :-).
Question 1: Can we characterise the continuous maps (or equivalently ) that arise this way?
Question 2: If is an open map, when is or also open?
Relationship to logic
Let be a homomorphism of Boolean algebras and its continuous dual. Then, as Celia and Mai also proved,
has a left adjoint iff is open.
The left adjoint can be thought to express existential quantification (cf. hyperdoctrines for details). Note that it is not difficult to show that if the left adjoint exists then also the right adjoint of exists. It can be expressed by . The right adjoint represents universal quantification.
From what we’ve discussed above we see that if has a left adjoint then the extension of to the homomorphism between the corresponding frames automatically has a left adjoint which satisfies the Frobenius identity.
Remark 1: Geometric morphisms between toposes also introduce a double adjunction , which then takes care of dependent quantifiers in topos type theory. See ncatlab for references.
Remark 2: Another property required by hyperdoctrines is the Beck-Chevalley condition. This is a global property of hyperdoctrines, as it requires commutativity of certain squares. The Beck-Chevalley condition together with the Frobenius identity make sure that subsitution is well-behaved with respect to existential quantification, see e.g. here.