Theory and Applications of Categories, Vol. 12, No. 13, 2004, pp. 372–422.

THE DOUBLE POWERLOCALE AND EXPONENTIATION: A CASE STUDY IN GEOMETRIC LOGIC

STEVEN VICKERS

Abstract. If X is a locale, then its double powerlocale ℙX is defined to be P_{U}(P_{L}(X)) where P_{U} and P_{L} are the upper and lower powerlocale constructions. We prove various results relating it to exponentiation of locales, including the following. First, if X is a locale for which the exponential 𝕊^{X} exists (where 𝕊 is the Sierpinski locale), then ℙX is an exponential 𝕊^{𝕊^{X}}. Second, if in addition W is a locale for which ℙW is homeomorphic to 𝕊^{X}, then X is an exponential 𝕊^{W}.

The work uses geometric reasoning, i.e. reasoning stable under pullback along geometric morphisms, and this enables the locales to be discussed in terms of their points as though they were spaces. It relies on a number of geometricity results including those for locale presentations and for powerlocales.

1. Introduction

Why should exponentiable locales be locally compact? That is, if a locale X is such that the exponential Y^{X} exists for every locale Y, why does it follow that the frame ΩX of opens is a continuous lattice? The proof in [Johnstone 82] involves an analysis of injective locales, but [Hyland 81] gives a more direct proof. We paraphrase it in a naive way that, on the face of it, is just too simple to be right.

1. If X is exponentiable, then, in particular, 𝕊^{X} exists, where 𝕊 is the Sierpinski locale whose frame is free on one generator. The points of 𝕊^{X} are in bijective (and order preserving – cf. Hyland’s sublemma 2.1) correspondence with the continuous maps from X to 𝕊, and hence with the opens of X. We should therefore like to think of 𝕊^{X} as a particular topology on the frame ΩX, and one whose specialization order is the frame order.

2. The evaluation map ev : 𝕊^{X} × X → 𝕊 corresponds to an open of 𝕊^{X} × X, and that can be expressed in the form

ev = ⋁{V × b V ∈ Ω𝕊^{X}, b ∈ ΩX, V × b ≤ ev}.

3. If V × b ≤ ev then b is a lower bound of V. This is because if a is in V (we are thinking of V as an open subset of ΩX here) and x is in b then ⟨a, x⟩ is in ev and

Received by the editors 2001-11-21 and, in revised form, 2004-09-20. Transmitted by Peter Johnstone. Published on 2004-11-01. 2000 Mathematics Subject Classification: 06D22, 03G30, 03F55, 54C35, 18C15. Key words and phrases: locale, powerlocale, exponentiable, geometric logic. \begin{matrix}c \\ ◯ \end{matrix} Steven Vickers, 2004. Permission to copy for private use granted.

so x is in a. Hence b ≤ a. Indeed, b ≪ a (b is way below a), for suppose a ≤ ⋁_{i}^{↑} c_{i}. In a locale every open V is also Scott open, and it follows that c_{i} ∈ V for some i, and then b ≤ c_{i}. (cf. Hyland’s sublemma 2.3.)

4. If a is an open of X, then (Hyland’s sublemma 2.4)

a = ⋁^{↑}{b ∈ ΩX ∃V ∈ Ω𝕊^{X}. (V × b ≤ ev, a ∈ V)}

This join is directed, for if V_{i} × b_{i} ≤ ev and a ∈ V_{i} (i = 1, 2), then a ∈ V_{1} ∧ V_{2}, (V_{1} ∧ V_{2}) × b_{i} ≤ ev and so (V_{1} ∧ V_{2}) × (b_{1} ∨ b_{2}) ≤ ev. Also, the set of joined elements is inhabited, for it contains b = ∅ because 𝕊^{X} × ∅ = ∅ ≤ ev.

To show that a is this join, suppose x ∈ a. Then ⟨a, x⟩ ∈ ev and so ⟨a, x⟩ ∈ V × b ≤ ev for some V, b.

5. Hence every open of X is a join of opens way below it, which suffices to show that ΩX is a continuous lattice.

We have used very spatial modes of reasoning here, treating opens as sets of points. On the other hand, we have also used the sobriety of locales in step 3, since that is what tells us that every open is Scott open. It appears to be an argument that could only work for sober spaces or spatial locales, and if we tried to restrict it to those we should have the problem of saying just which category X is exponentiable in.

The flaw in such spatial arguments is, of course, that in general locales are not spatial: they do not have enough points. It is for this reason that one usually approaches locales through pure lattice theory, as captured in the phrase “point-free topology” [Johnstone 82].

An underlying goal of this paper is to show that, nonetheless, naive spatial arguments of this kind can in fact be essentially correct.

The correctness does not come for free, however. If the points of X are understood as the maps from 1 to X, in other words the global points, then there really are not enough in general. It is only by understanding points in a generalized fashion, maps from an arbitrary locale Y to X, that one finds enough. Reasoning about these points can be carried through by replacing ordinary sets by sheaves over Y, but these do not conform with all classical reasoning principles – one must instead reason constructively.

This, then, is a practical benefit of constructive reasoning. If it is of the kind that is valid in toposes (which we shall refer to as intuitionistic reasoning), it can be applied to give results about sheaves, treating them as though they were sets. This is perhaps most strikingly displayed in [JoyTie 84]. This also allows results about locales to be turned for free into results about continuous maps between locales, since a map targeted on X is equivalent to an internal locale in the category SX of sheaves over X.

A further refinement is to use the more stringent geometric reasoning, stable under pullback along geometric morphisms. Under this regime, reasoning in SX about the generic point of X can be transferred to all points of X, and this can be exploited to give a very spatial view of locale theory. A locale is then defined by saying (geometrically) what its points are, and a geometric morphism – a map – is defined by saying (geometrically) how it transforms points. Topology is intrinsic, and continuity is automatic. This technique, actually an old trade secret of topos theorists, is used very explicitly in [Vickers 99], [Vickers 01].

The present paper develops this in an example where geometric constructions must be used not only on points, but even on locales themselves. To see this in overview, the main result is that if a locale X is exponentiable then so is 𝕊^{X} (where 𝕊 is the Sierpinski locale), and 𝕊^{𝕊^{X}} is homeomorphic to a different construction ℙX, the double powerlocale of the title. (It is defined as P_{U} P_{L} X ≅ P_{L} P_{U} X, but we shall not use that for the moment.)

Looking at global points, this implies an equivalence between points of ℙX and opens of 𝕊^{X} (i.e. maps 𝕊^{X} → 𝕊). However, the definition of exponential goes beyond this to require an equivalence between maps Y × 𝕊^{X} → 𝕊 and maps Y → ℙX for any locale Y. Consider what happens when we work intuitionistically in SY. The maps Y × 𝕊^{X} → 𝕊 are equivalent to opens of a locale over Y given by the projection fst : Y × 𝕊^{X} → Y. If we have a proof for global points that is intuitionistic then we can apply it in SY to get an equivalence with points over Y of ℙ_{Y} (Y × X → Y) where ℙ_{Y} is the ℙ construction carried out in SY.

Y × X  ℙ_{Y} (Y × X → Y)
↘_{fst}  ↙_{p}
Y

Such a point over Y is a map e : Y → ℙ_{Y} (Y × X → Y) such that e; p = Id_{Y}. However, it remains to make a connection between ℙ_{Y} and ℙ, and what is needed is that ℙ itself should be geometric, preserved by pullback. This is to say that

ℙ_{Y} (Y × X → Y) ≅ (Y × ℙX → Y)

and then points of Y × ℙX over Y are just maps Y → ℙX.

The geometricity of a construction such as ℙ is highly non-trivial. This is because locales are defined as frames (certain complete lattices), but the frames are not geometric. If f : X → Y is a map and A is a frame in SY, then f^{∗}(A) is not in general a frame in SX. The reason is that completeness of A in SY means having all Y -set-indexed joins, joins of all families (a_{i})_{i∈I} indexed by objects I of SY. This property is preserved in f^{∗}(A), but to be a frame in SX it needs more general X-set-indexed joins. In effect, f^{∗}(A) is only a basis, not the full topology, for the pulled back locale, and this provides the essential idea for our geometric working. We must deal not directly with the frames themselves but with presentations of them (by generators and relations) and show how ℙ can be constructed geometrically in terms of the presentations. In fact this result is one of considerable depth, relying on “coverage theorems” to relate presentations of frames to those of suplattices and preframes, and showing that some messy geometric constructions can be given universal characterizations intuitionistically.

That, then, is the underlying shape of the paper: geometricity results can be exploited to simplify some localic reasoning. We now move on to discussing the double powerlocale ℙ.

In locale theory one encounters a number of ways of forming locales whose points are sublocales of other locales. Obvious examples are the powerlocales (upper, lower and Vietoris), and in addition if a locale X is exponentiable then the points of 𝕊^{X} (where 𝕊 is the Sierpinski locale) are the maps from X to 𝕊 and hence in bijective correspondence with the open or with the closed sublocales of X.

Some interesting ways in which these relate to each other are shown in the case of algebraic dcpos.

1.1. Proposition. If X is an algebraic dcpo then 𝕊^{𝕊^{X}} ≅ P_{L}(P_{U}(X)) where P_{L} and P_{U} denote the lower and upper powerlocales.

Proof. An algebraic dcpo is one of the form Idl P where P is a poset. Its frame of Scott opens is isomorphic to the Alexandrov topology on P, an open being an upper closed subset of P. This is equivalent to a filter of FP (the finite powerset) under the upper preorder

S ⊑_{U} T iff ∀t ∈ T. ∃s ∈ S. s ⊑ t

This is the same as an ideal of FP under (⊑_{U})^{op}, and in fact Idl(P) is exponentiable with 𝕊^{X} homeomorphic to the ideal completion of (FP, (⊑_{U})^{op}). On the other hand, the upper powerlocale is the ideal completion of (FP, ⊑_{U}), so for algebraic dcpos X the exponential 𝕊^{X} is found by first taking the upper powerlocale and then taking the “Hofmann-Lawson” dual that inverts the generating poset (of compact points). A consequence is that 𝕊^{𝕊^{X}} is got by first taking the upper powerlocale, then dualizing, then taking the upper powerlocale again, then dualizing again. But the last three steps are equivalent to taking the lower powerlocale, for that is given by the ideal completion of (FP, ⊑_{L}) where

S ⊑_{L} T iff ∀s ∈ S. ∃t ∈ T. s ⊑ t

Hence for an algebraic dcpo X we have 𝕊^{𝕊^{X}} ≅ P_{L}(P_{U}(X)), which we write as ℙX.

We shall show (Theorem 11.1) that this result extends to all exponentiable locales. To some extent this is no surprise. It is a result stating that the points of ℙX are in

bijective correspondence with the maps from 𝕊^{X} to 𝕊, in other words the opens of 𝕊^{X}. By [JoVic 91], the global points of ℙX are known to be the functions from ΩX to Ω that preserve directed joins. On the other hand, it is also known that if 𝕊^{X} exists then X is exponentiable and ΩX is a continuous lattice whose Scott topology gives the locale 𝕊^{X}. Hence the opens of 𝕊^{X}, the Scott opens of ΩX, are just the Scott continuous maps from ΩX to Ω – in other words, the functions that preserve directed joins.

We therefore know already that the global points of ℙX correspond to the global opens of 𝕊^{X}. However, we do not rely on established results about exponentiability, but show direct from the definition that if 𝕊^{X} exists then 𝕊^{𝕊^{X}} (exists too and) is homeomorphic to ℙX. In a partial converse, we also show that if 𝕊^{X} is homeomorphic to ℙW then 𝕊^{W} exists and is homeomorphic to X. In the process we also prove many properties of ℙ and ℙ-algebras.

Recent work of Paul Taylor [Taylor 01] has investigated an abstract formalism that includes the monad Σ^{2} : X ↦ 𝕊^{𝕊^{X}} on locally compact (i.e. exponentiable) locales (the Sierpinski locale is Σ in Taylor’s notation). The Σ^{2}-algebras are frames, and amongst other topics Taylor considers the Σ^{2}-algebra structure on 𝕊 and (hence) on exponentials 𝕊^{X}, showing for instance a Stone duality result that maps X → Y are equivalent to Σ^{2}-homomorphisms 𝕊^{Y} → 𝕊^{X}.

Another purpose therefore of the present paper is to show how Σ^{2} is the restriction to locally compact locales of a monad (ℙ) that does not rely on exponentiability.

2. Miscellaneous remarks on locales and toposes

Locales and maps. We use the words “locale” and “frame” following [Johnstone 82] (as opposed to “space” and “locale” in [JoyTie 84]) and we shall always take care to use notation and language for locales that is appropriate to their spatial aspect. We write Loc for the category of locales. If X is a locale, then we write ΩX for its corresponding frame of opens and SX for its category of sheaves. We write true and false for the top and bottom elements of a frame.

If X and Y are locales, then notation such as f : X → Y will always denote a continuous map from X to Y, corresponding to a frame homomorphism Ωf (also written as f^{∗}) from ΩY to ΩX.

Dcpo enrichment. We write ⊑ for the specialization order on Loc,

f ⊑ g iff ∀b ∈ ΩY. Ωf(b) ≤ Ωg(b)

Loc is dcpo (directed complete poset) enriched under ⊑, with directed joins defined by

Ω(⨆_{i}^{↑} f_{i})(b) = ⋁_{i}^{↑} Ωf_{i}(b)

(This will be elaborated in Section 6.) The superscript ^{↑} after a join symbol will indicate that the join is directed.

Presentations. Crucial to our development will be the use of generators and relations for presenting frames (see in particular [Vickers 89]), using notation such as

Fr⟨G|R⟩

Here G is a set of generators and R a set of relations of the form ϕ_{1} ≤ ϕ_{2} or ϕ_{1} = ϕ_{2}, ϕ_{1} and ϕ_{2} being expressions formed from the generators using finite meets and arbitrary joins. (This will be formalized in Section 5.) If G has structure (e.g. poset or semilattice) that is to be preserved in the frame, then it is convenient to indicate this by the word “qua”, for instance, “G (qua ∧-semilattice)”.

Sierpinski locale. The Sierpinski locale 𝕊 is defined by

Ω𝕊 = Fr⟨1⟩,

i.e. the free frame on one generator. Its points are the subsets of 1, and in particular we have two classical points ⊥ = ∅ and ⊤ = 1. We write {⊤} for the generating open, since ⊤ is the sole point of 𝕊 in it.

¿From the definition it is clear that there is a bijection between opens of X and maps X → 𝕊. By abuse of notation, we shall use the same symbol a for –

• an open a ∈ ΩX,

• the map a : X → 𝕊,

• the open sublocale a ↪ X.

However, if X is exponentiable, we shall use different notation^{⌜}a^{⌝} for the corresponding point of 𝕊^{X}.

Toposes. ¿From time to time, mostly in discussing the constructive reasoning, we shall refer to toposes. Just as with locales, we shall use notation and language adapted to their aspect as generalized spaces rather than generalized universes of sets. For a topos X, we write SX for its category of sheaves, its generalized universe of sets. This is its ordinary category-theoretic expression: in the conventional language one simply says that the topos is this category. Note also that what we refer to as sheaves over a topos are exactly the objects of this category. We also write ΩX for its frame of opens, the frame of subobjects of 1 (or global elements of Ω) in SX. Notationally a locale X is thus just a special “localic” kind of topos, one in which the whole of SX is determined by ΩX. We make no attempt to say whether a locale “is” its frame or “is” its category of sheaves. It simply has both and can be defined by either.

If X and Y are toposes, then notation such as f : X → Y will always denote a geometric morphism from X to Y, never a functor from SX to SY. We shall often refer to this as a map from X to Y.

Note that the inverse image functor f^{∗} : SY → SX is pullback along f in the following sense. Sheaves over Y (objects of SY) correspond, up to homeomorphism, with local homeomorphisms (étale maps) targeted at Y, and then f^{∗} on sheaves corresponds to pullback along f (also written f^{∗}) applied to the local homeomorphisms.

Important to our development will be the geometric logic of sets, i.e. that fragment of the internal intuitionistic logic of categories of sheaves that is preserved by inverse image functors. See [Vickers 99] for an account of how that includes not only the pure logic (⋁, ∧, =, ∃) but also set constructions (principally colimits, finite limits, free algebras). We shall consistently understand finite to mean Kuratowski finite, and then the finite power set F (free semilattice) and finitely bounded universal quantification are also geometric.

If T is a geometric theory, we write [T] for its classifying topos (as generalized space) and S[T] for the corresponding category of sheaves (generalized universe of sets).

Very important to us will be the fact that locale theory, insofar as it is constructive, can be conducted internally in categories of sheaves SB (B a topos). From an internal frame ΩX in SB one can construct a category of sheaves SX with a localic geometric morphism f : X → B (i.e. what [JoyTie 84] Section VI.5 call a spatial geometric morphism). The frame ΩX can be recovered (up to isomorphism) as f_{∗}(Ω_{X}), where Ω_{X} is the subobject classifier in SX. An important fact is that continuous maps between the locales (in the sense of frame homomorphisms between the frames) are equivalent to geometric morphisms between the toposes:

2.1. Theorem. Let f : X → B be a map (geometric morphism) that is localic. Then for any other map g : E → B, there is an equivalence between maps from E to X over B, and frame homomorphisms from f_{∗}Ω_{X} to g_{∗}Ω_{E} in SB. (Ω_{X} and Ω_{E} are the subobject classifiers in SX and SE.)

Proof. Joyal and Tierney [JoyTie 84].

Stages of definition. We now turn to the spatial aspects of locale theory. As is well-known, a locale X may not have an adequate supply of points in the sense of maps 1 → X (global points), and so reasoning solely in terms of those points cannot give full results about the locale. Instead, we must consider generalized points, maps Y → X, where Y, an arbitrary topos, is the stage of definition. In particular, the identity map Id : X → X can be considered a point (the generic point) in the internal logic of SX, and for many purposes it is already a sufficiency of points. For instance, as discussed at length in [Vickers 99] and [Vickers 01], a map f : X → Y can be described in full simply by giving a geometric construction of f(x) for the generic point x of X. The fact that this construction is intuitionistic means that it can be done internally in SX, thus obtaining a point of Y there, and the fact that it is geometric means that it is preserved by pullback along geometric morphisms and so the same construction applies at any stage of definition.

Let us examine the relationship between global locale theory and locale theory at some stage B.

If X is a (global) locale, then we have a corresponding locale over B, namely the first projection, a localic map, B × X → B. This can be expressed concretely in frames, but in Section 5 we shall see how to express it using frame presentations.

Suppose Y is another global locale. A map from X to Y at stage (or over) B is a map from B × X to B × Y making this triangle commute:

B × X ⟶ B × Y
↘ ↓
B

Globally, this is equivalent to a map from B × X to Y. The correspondence respects order, for a pair of maps f ⊑ g : X → Y is equivalent to a map 𝕊 × X → Y. Working over B, this is equivalent to (B × 𝕊) ×_{B} (B × X) ≅ B × 𝕊 × X → B × Y over B (it follows from the main result of Section 5 that the Sierpinski locale as calculated at stage B is just B × 𝕊 → B), and that is equivalent to 𝕊 × B × X → Y, i.e. two maps B × X → Y with one less than the other.

The final locale at stage B is the identity map B ≅ B × 1 → B, and so a point of X at stage B, a map 1 → X at stage B, is, globally, a map B → X.

An open of X at stage B is a map X → 𝕊 at stage B and hence, globally, a map B × X → 𝕊, in other words an open of B × X.

If, at stage B, we have a point x and an open a of X, then we write x ⊨ a for the truth value (point of 𝕊) calculated over B as x; a : 1 → X → 𝕊. Globally, this is given as ⟨B, x⟩; a : B → B × X → 𝕊.

2.2. Proposition. Let X be a locale, and let a and b be two sublocales. Then a ≤ b iff every point of a is also in b.

Proof. If the generic point of a is also in b, then the same goes for every point at every stage. Working with the generic point is equivalent to working over a. Viewed globally, the generic point Δ : a → a × a is, as point of X, ⟨Id_{a}, i_{a}⟩ : a → a × X where i_{a} : a ↪ X is the sublocale inclusion. For this to be in b we must have some ⟨Id_{a}, f⟩ : a → a × b with ⟨Id_{a}, f⟩; ⟨Id_{a}, i_{b}⟩ = ⟨Id_{a}, i_{a}⟩. In other words i_{a} = f; i_{b}, i.e. a ≤ b.

Suplattices and preframes. A suplattice [JoyTie 84] is a complete join semilattice; the homomorphisms are the functions that preserve all joins. A preframe [JoVic 91] is a poset equipped with finite meets and directed joins, the former distributing over the latter. The homomorphisms are the functions that preserve finite meets and directed joins. In various contexts we shall use “SupL” and “PreFr” as abbreviations for these.

Continuous dcpos. We shall need some results on continuous dcpos (or continuous posets), treated as locales. To access geometric methods for handling them, we present them using the continuous information systems of [Vickers 93].

2.3. Definition. A continuous information system is a set P equipped with an idempotent binary relation <.

“Idempotent” means that <; <=<. The ⊆ direction of this says that < is transitive, while the ⊇ direction says that it is interpolative — if x < z then x < y < z for some y.

2.4. Definition. Let P be a continuous information system. Then an ideal of P is a subset I such that

1. I is inhabited.

2. I is lower closed under <.

3. If x, y ∈ I then there is some z ∈ I such that x < z and y < z.

(Note from (3) that if x ∈ I then there is some z ∈ I such that x < z: in other words, I is rounded.)

The ideal completion Idl(P) of P is the locale whose points are the ideals of P. It can be presented as

Ω Idl(P) = Fr⟨↑ x (x ∈ P)|true ≤ ⋁_{x∈P} ↑ x
↑ y ≤↑ x (x < y)
↑ x∧ ↑ y ≤ ⋁{↑ z x < z, y < z}⟩

where for any ideal I we have I ⊨↑ x iff x ∈ I.

3. The upper and lower powerlocales

The powerlocales P_{L} (lower) and P_{U} (upper) are conveniently summarized in [Vickers 97]. They are the functor parts of two monads on Loc, denoted (P_{L}, ↓, ⊔) and (P_{U}, ↑, ⊓).

3.1. Definition. The lower powerlocale is defined by

Ω P_{L} X = Fr⟨ΩX (qua SupL)⟩
= Fr⟨♢a (a ∈ ΩX)|♢ preserves all joins⟩
Ω P_{L}(f)(♢b) = ♢Ωf(b) (f : X → Y)
Ω(↓)(♢a) = a
Ω(⊔)(♢a) = ♢♢a

(Its points are the weakly closed sublocales of X with open domain.)

3.2. Definition. The upper powerlocale is defined by

Ω P_{U} X = Fr⟨ΩX (qua PreFr)⟩
= Fr⟨□a (a ∈ ΩX)|□ preserves finite meets and directed joins⟩
Ω P_{U}(f)(□b) = □Ωf(b) (f : X → Y)
Ω(↑)(□a) = a
Ω(⊓)(□a) = □□a

(Its points are the compact fitted sublocales of X.)

Note a crucial feature of these definitions: they are not geometric in form. This is because neither suplattice structure nor preframe structure is preserved by inverse image functors. A substantial part of this paper is devoted to showing that, nonetheless, the powerlocales are geometric.

An important feature is that P_{L} is a KZ-monad and P_{U} is a coKZ-monad (i.e. a KZ-monad on Loc^{co}, with the order reversed), so we first mention some of the standard properties of these.

3.3. Definition. Let C be a poset-enriched category, and let (T, η, μ) be a monad on C for which T preserves the order on morphisms. Then the monad is a KZ-monad iff, for each X, T η_{X} ⊑ η_{T X}.

3.4. Proposition. Let C be a poset-enriched category, and let (T, η, μ) be a KZ-monad on C.

1. For each object X, μ_{X} is right adjoint to T η_{X} and left adjoint to η_{T X} – this amount

to two inequalities

μ; T η_{X} ⊑ Id_{T^{2}X} ⊑ μ; η_{T X}

(In fact, these conditions are also sufficient for the KZ-property.)

2. If X is an object and α : T X → X is T -algebra structure on X, then α is left adjoint to η_{X}. Hence T -algebra structure on X, if it exists at all, is unique.

Proof. [Kock 95]

Dually, a monad (T, η, μ) is coKZ iff T η_{X} ⊒ η_{T X}.

3.5. Proposition. P_{L} is a KZ-monad.

Proof. We omit the proof that it is a monad. To show it is KZ, we show

P_{L}(↓_{X}) ⊑ ↓_{P_{L} X}: P_{L} X → P_{L}^{2} X

The finite meets ⋀_{a∈S} ♢a form a basis for P_{L} X, and so the opens ♢ ⋀_{a∈S} ♢a form a subbasis of P_{L}^{2} X. Examining inverse image functions, we find that the required inequalities follows from

♢ ⋀_{a∈S} a ≤ ⋀_{a∈S} ♢a

3.6. Proposition. P_{U} is a coKZ-monad.

Proof. To show it is coKZ, we show

P_{U}(↑_{X}) ⊒ ↑_{P_{U} X}: P_{U} X → P_{U}^{2} X.

The finite joins ⋁_{a∈S} □a form a preframe basis for P_{U} X, in the sense that every open is a directed join of finite meets of them. This is because the □bs form a subbasis, so every open is a join of finite meets of them. An arbitrary join is a directed join of finite joins, and by finite distributivity a finite join of finite meets is a finite meet of finite joins. Hence the opens □ ⋁_{a∈S} □a form a subbasis of P_{U}^{2} X. Examining inverse image functions, we find that the required inequalities follows from

□ ⋁_{a∈S} a ≥ ⋁_{a∈S} □a

3.7. Proposition. Let X be a locale. Then the following are equivalent.

1. The unique map ! : X → 1 and the diagonal map Δ : X → X^{2} have right adjoints.

2. For every n, the diagonal Δ : X → X^{n} has a right adjoint.

3. X is a localic semilattice whose semilattice operations are meets with respect to the specialization order.

Proof. 2 ⇒ 1 a fortiori.

1 ⇒ 3: Let us write ⊤ and ⊓ for the right adjoints of ! and Δ. It is easy to show that these operations satisfy the semilattice laws. For instance, for associativity one shows that both sides of the equation give right adjoints for the diagonal Δ : X → X^{3}. To define n-ary meets with respect to the specialization order is to define a right adjoint ⊓ for the diagonal Δ : X → X^{n}: for we want ⊓_{i=1}^{n}x_{i} ⊑ y iff (x_{i}) ⊑ Δ(y).

3 ⇒ 2 also now follows.

3.8. Definition. A locale X is a localic meet semilattice if it satisfies the equivalent conditions of Proposition 3.7.

Proposition 3.7 dualizes, replacing right adjoints by left adjoints and meets by joins. A locale satisfying the dual proposition is a localic join semilattice.

3.9. Proposition.

1. Any P_{U}-algebra is a localic meet semilattice.

2. Any P_{L}-algebra is a localic join semilattice.

Proof. 1. Let X be a locale. We first show that P_{U} X is a localic meet semilattice. We define ⊤ : 1 → P_{U} X and ⊓ : (P_{U} X)^{2} → P_{U} X by

Ω⊤(□a) = true
Ω ⊓ (□a) = □a × □a

To show that ⊤ is right adjoint to !, we calculate ⊤; ! ⊑ Id_{1} (actually, equality is obvious) and Id_{P_{U} X} ⊑ !; ⊤. The latter follows because

□a ≤ true = Ω!(true) = Ω! ∘ Ω⊤(□a).

For ⊓ right adjoint to Δ, we want ⊓; Δ ⊑ Id_{(P_{U} X)^{2}} and Id_{P_{U} X} ⊑ Δ; ⊓. For the former, we note that the opens □a of P_{U} X form a basis, and so the opens □a × □b of (P_{U} X)^{2} form a basis. We then calculate

Ω(⊓; Δ)(□a × □b) = Ω ⊓ (□a ∧ □b) = Ω ⊓ (□(a ∧ b))
= □(a ∧ b) × □(a ∧ b) ≤ □a × □b

For the latter,

Ω(Δ; ⊓)(□a) = ΩΔ(□a × □a) = □a ∧ □a = □a

Now let X be any P_{U}-algebra with structure map α : P_{U} X → X. We can define its semilattice operations ⊓_{n} : X^{n} → X by the composite

X^{n} ⟶^{↑^{n}} (P_{U} X)^{n} ⟶^{⊓_{n}} P_{U} X ⟶^{α} X

Now

Δ; ↑^{n}; ⊓_{n}; α = ↑; Δ; ⊓_{n}; α =↑; α = Id_{X}
↑^{n}; ⊓_{n}; α; Δ = ↑^{n}; ⊓_{n}; α; Δ; ↑^{n}; α^{n}
= ↑^{n}; ⊓_{n}; α; ↑; Δ; α^{n}
⊑ ↑^{n}; ⊓_{n}; Δ; α^{n}
⊑ ↑^{n}; α^{n} = Id_{X^{n}}

so that these are right adjoint to the diagonals as required.

2. The proof is more or less dual. The localic join semilattice operations ⊥ and ⊔ on P_{L} X are defined by

Ω⊥(♢a) = false
Ω ⊔ (♢a) = ♢a ⊙ ♢a

(In a product X × Y, we write a ⊙ b for a × Y ∨ X × b.)

We shall need results on powerlocales of dcpos.

3.10. Definition. Let (X, <) be a continuous information system. Then the orderings <_{U} and <_{L} on FG, the upper and lower orders, are defined by

S <_{U} T iff ∀t ∈ T. ∃s ∈ S. s < t
S <_{L} T iff ∀s ∈ S. ∃t ∈ T. s < t

Both are idempotent. If in addition < is reflexive (so it is a preorder), then so are <_{U} and <_{L}, and we write ≡_{U} and ≡_{L} for the corresponding equivalence relations.

3.11. Theorem. Let (X, <) be a continuous information system. Then –

P_{U}(Idl(X)) ≅ Idl(FX, <_{U})
P_{L}(Idl(X)) ≅ Idl(FX, <_{L})

Proof. [Vickers 93].

4. The double powerlocale ℙ

In [JoVic 91] it is shown that the upper and lower powerlocales commute up to isomorphism. We shall write ℙ for (without prejudice) P_{U} P_{L} or P_{L} P_{U}. Under the isomorphisms, the open □♢a of P_{U} P_{L} X (a an open of X) corresponds to the open ♢□a of P_{L} P_{U} X. We write ⊠a for the corresponding open of ℙX, ⊠ being intended as a kind of combination of □ and ♢.

Another way to understand the monad structure on P_{U} P_{L} is in terms of distributivities [Beck 69]: P_{U} and P_{L} distribute over each other.

4.1. Definition. Let (T_{i}, η_{i}, μ_{i}) be a monad (i = 1, 2). A distributive law of T_{2} over T_{1} is a natural transformation σ : T_{2} ∘ T_{1} → T_{1} ∘ T_{2} such that the following diagrams commute.

T_{2} ⟶^{T_{2}η_{1}} T_{2} ∘ T_{1} ⟵^{η_{2}T_{1}} T_{1}
↘_{η_{1}T_{2}} ↓ σ  ↙_{T_{1}η_{2}}
T_{1} ∘ T_{2}
T_{2} ∘ T_{1} ∘ T_{1} ⟶^{T_{2}μ_{1}} T_{2} ∘ T_{1} ⟵^{μ_{2}T_{1}} T_{2} ∘ T_{2} ∘ T_{1}
↓_{σT_{1}}  ↓_{T_{2}σ}
T_{1} ∘ T_{2} ∘ T_{1} ↓_{σ} T_{2} ∘ T_{1} ∘ T_{2}
↓_{T_{1}σ}  ↓_{σT_{2}}
T_{1} ∘ T_{1} ∘ T_{2} ⟶^{μ_{1}T_{2}} T_{1} ∘ T_{2} ⟵^{T_{1}μ_{2}} T_{1} ∘ T_{2} ∘ T_{2}

There is then a monad structure on T_{1} ∘ T_{2}, with unit

η = η_{1}η_{2} : Id → T_{1} ∘ T_{2}

and multiplication

μ = (T_{1}σT_{2}); (μ_{1}μ_{2}) : T_{1} ∘ T_{2} ∘ T_{1} ∘ T_{2} → T_{1} ∘ T_{1} ∘ T_{2} ∘ T_{2} → T_{1} ∘ T_{2}

4.2. Proposition. The isomorphism P_{L} P_{U} ≅ P_{U} P_{L} is a distributive law of P_{L} over P_{U}. Its inverse is a distributive law of P_{U} over P_{L}.

Proof. The conditions are routine to check.

4.3. Corollary. ℙ is the functor part of a monad on Loc, with unit ↕: X → ℙX defined by Ω ↕ (⊠a) = a and multiplication H : ℙℙX → ℙX defined by ΩH(⊠a) = ⊠ ⊠ a.

(The notation is explained as follows. The powerlocales give monads (P_{U}, ↑, ⊓) and (P_{L}, ↓, ⊔), where the notation is chosen to match the fact that the points of the powerlocales are sublocales of the original locale. Then, for instance, if x is a point of X, then the point ↑ x of P_{U} X is the compact saturated sublocale of X whose points are those of X that are bigger than x in the specialization order. Then ↕ is chosen as a combination of ↑ and ↓, and H as a combination of ⊓ and ⊔.)

4.4. Theorem. ΩℙX ≅ Fr⟨ΩX (qua dcpo)⟩.

Proof. [JoVic 91].

Our contention is that the ℙ-algebras are in some sense “localic frames”. They are both P_{U}-algebras and P_{L}-algebras, and this makes them both localic meet-semilattices and localic join semilattices. Moreover, as lattices they are distributive. But every locale has directed joins (of its points), and the meets, being continuous, preserve those directed joins. Hence we can reasonably think of a ℙ-algebra as having all joins as well as frame distributivity.

We shall show in due course that the Sierpinski locale 𝕊, whose points are the subsets of 1, is the initial ℙ-algebra (in fact, 𝕊 ≅ ℙ∅). Also, for locale X, the exponential 𝕊^{X} is a ℙalgebra if it exists. Then the points of X are equivalent to the ℙ-algebra homomorphisms from 𝕊^{X} to 𝕊, and we have lifted to Loc the standard fact that the points of X are equivalent to the frame homomorphisms from ΩX to Ω.

In a frame the meets and joins are determined by the order. In a locale the specialization order is intrinsic, and so we should expect that ℙ-algebra structure, where it exists at all, is unique. We shall now prove this.

4.5. Proposition. Let α : ℙX → X make X a ℙ-algebra.

1. X is a P_{U}-algebra and α is a P_{U}-homomorphism.

2. X is a P_{L}-algebra and α is a P_{L}-homomorphism.

3. α is the unique ℙ-algebra structure of X.

Proof. 1. Define α_{U} = P_{U}(↓); α : P_{U} X → P_{U} P_{L} X = ℙX → X. The properties of distributivities tell us that

↕= (↑; P_{U}(↓)) : X → P_{U} X → P_{U} P_{L} X = ℙX,

and it follows that

↑; α_{U} =↕; α = Id_{X}

Next, to complete the proof that α_{U} makes X a P_{U}-algebra, we should prove that ⊓; α_{U} = P_{U}(α_{U}); α_{U}. However, it is easier to prove first that α is a P_{U}-homomorphism (note that ℙX = P_{U} P_{L} X is itself a P_{U}-algebra), i.e. that ⊓; α = P_{U} α; α_{U}. For this, note first that

⊓ = P_{U}(↓); H : P_{U} ℙX → ℙ^{2}X → ℙX

for both have inverse image map ⊠a ⟼ □□♢a. It follows that

⊓; α = P_{U}(↓); H; α
= P_{U}(↓); ℙα; α
= P_{U}(↓; P_{L} α); α
= P_{U}(α; ↓); α
= P_{U} α; P_{U}(↓); α
= P_{U} α; α_{U}

Now to complete the proof that α_{U} makes X a P_{U}-algebra, we have

⊓; α_{U} = ⊓; P_{U}(↓); α
= P_{U}^{2}(↓); ⊓; α
= P_{U}^{2}(↓); P_{U} α; α_{U}
= P_{U}(P_{U}(↓); α); α_{U}
= P_{U}(α_{U}); α_{U}

The proof of (2) is formally very similar, using α_{L} = P_{L}(↑); α : P_{L} X → P_{L} P_{U} X ≅ ℙX → X.

For (3), suppose β : ℙX → X also makes X a ℙ-algebra. By Proposition 3.4 we have α_{U} = β_{U} and α_{L} = β_{L}. Let us fix on ℙX as P_{U} P_{L} X and be careful about the isomorphism with P_{L} P_{U} X. α_{L} is strictly speaking the map

α_{L} = P_{L}(↑); ≅; α : P_{L} X → P_{L} P_{U} X ≅ P_{U} P_{L} X = ℙX → X

We can see that P_{L}(↑); ≅ is equal to ↑, since the inverse image functions for both take □♢a ↦ ♢a. It follows that α is the unique P_{U}-homomorphism from P_{U} P_{L} X to X extending α_{L}. Similarly β is the unique P_{U}-homomorphism from P_{U} P_{L} X to X extending β_{L}, and since α_{L} = β_{L} we deduce α = β.

The following result is analogous to the fact that any order isomorphism between frames is a frame isomorphism.

4.6. Corollary. Any homeomorphism between ℙ-algebras is a ℙ-algebra isomorphism.

Proof. Let α : ℙX → X and β : ℙY → Y be ℙ-algebras, and let f : X → Y be a homeomorphism. It is straightforward to verify that ℙf; β; f^{−1} is a ℙ-algebra structure on X, so ℙf; β; f^{−1} = α.

4.7. Proposition. The initial ℙ-algebra ℙ∅ is 𝕊. Its structure map, from ℙ𝕊 to 𝕊, corresponds to the open ⊠{⊤}.

Proof. This is most conveniently calculated applying Theorem 3.11 in the special case of algebraic dcpos, Idl P where P is a poset.

Now the initial locale ∅ is the ideal completion of the empty set, so P_{L} ∅ is the ideal completion of {∅}. This is just the final, one-point locale. Then P_{U} P_{L} ∅ is the ideal completion of a 2-element poset {⊥ ⊑ ⊤}. A point of P_{U} P_{L} ∅ is an ideal of {⊥, ⊤}, i.e. a subset I ⊆ {⊥, ⊤} that is directed and lower closed. Since it is inhabited and lower closed it must contain ⊥, so it is completely determined by whether it contains ⊤ — in other words, by its intersection with {⊤}. But if I′ is an subset of {⊤} then {⊥}∪I′ is an ideal. Hence there is a bijection between points of P_{U} P_{L} ∅ and subsets of 1. Moreover, this bijection is geometrically definable. The Sierpinski locale 𝕊 is defined by its frame being free on one generator, and it follows that its points are the subsets of 1. We therefore have that ℙ∅ is homeomorphic to 𝕊.

The generator {⊤} of Ω𝕊 is □false in P_{U} 1, i.e. □♢false in P_{U} P_{L} ∅, i.e. ⊠false in ℙ∅. The structure map is just H, and the corresponding open is ΩH({⊤}) = ΩH(⊠false) = ⊠ ⊠ false = ⊠{⊤}.

We now investigate the localic lattice structure of ℙ-algebras.

4.8. Proposition. Let X be a ℙ-algebra. Then X is both a localic meet semilattice and a localic join semilattice, and the resulting lattice structure is distributive.

Proof. We have already shown that X is both a P_{U}-algebra and a P_{L}-algebra. We show distributivity first for algebras ℙY. We must consider two maps (ℙY)^{3} → ℙY. The first takes (u, v, w) to u ⊓ (v ⊔ w), and its inverse image function takes

⊠a ↦ ⊠a × ⊠a ↦ ⊠a × (⊠a ⊙ ⊠a)

The second takes (u, v, w) to (u ⊓ v) ⊔ (u ⊓ w). Its inverse image function takes

⊠a ↦ ⊠a ⊙ ⊠a ↦ (⊠a × ⊠a) ⊙ (⊠a × ⊠a)
= ((⊠a × ℙY × ℙY × ℙY) ∧ (ℙY × ⊠a × ℙY × ℙY))
∨ ((ℙY × ℙY × ⊠a × ℙY) ∧ (ℙY × ℙY × ℙY × ⊠a))

↦ ((⊠a × ℙY × ℙY) ∧ (ℙY × ⊠a × ℙY)) ∨ ((⊠a × ℙY × ℙY) ∧ (ℙY × ℙY × ⊠a))

= (⊠a × ℙY × ℙY) ∧ ((ℙY × ⊠a × ℙY) ∨ (ℙY × ℙY × ⊠a))
= ⊠a × (⊠a ⊙ ⊠a)

Hence the two are equal, and ℙY is distributive. Since the corresponding maps for X are got by composing the ones for ℙX with ↕^{3}: X^{3} → (ℙX)^{3} and α : ℙX → X, it follows that the arbitrary ℙ-algebra X is also distributive.

Since ⊓ : X^{2} → X is continuous, it also distributes over directed joins in X, and this justifies our claim that ℙ-algebras are localic frames.

5. Geometricity of presentations

With this section we begin a series of geometricity results, essential for the geometric reasoning in the main results about ℙ and exponentiation. We start by discussing the geometricity of frame presentations. This is important, because frames themselves are not geometric.

A frame presentation will include sets G and R of generators and relations, and each relation can be written in the form e_{1} ≤ e_{2}, where e_{1} and e_{2} are frame expressions in the generators. Using frame distributivity, each e_{i} can be written as a join of finite meets of generators; and then the relation can be replaced by a set of relations, one for each disjunct in e_{1}, saying that the disjunct is ≤ e_{2}. After all this rewriting we have that each relation r is of the form –

finite meet of generators ≤ join of finite meets of generators

Let us write λ(r) ∈ FG for the finite set of conjuncts on the left. For the right-hand side, we have an arbitrary set of disjuncts: so what we should do is take the set D of all disjuncts in all relations, fibred over R by some π : D → R. Each disjunct d is a conjunction of a finite set ρ(d) of generators, so the relation r has been formalized as –

⋀ λ(r) ≤ ⋁_{π(d)=r} ⋀ ρ(d)

5.1. Definition. A frame presentation (or a (G,R,D)-system) is a structure comprising three sets G, R and D with functions λ : R → FG, ρ : D → FG, and π : D → R.

We write FrPr for the (geometric) theory of frame presentations.

Given such a frame presentation, then in conformity with established notation we shall write Fr⟨G|R⟩ for the frame presented by it. (Of course, this conceals the involvement of D, λ, ρ and π.) Then a frame homomorphism from Fr⟨G|R⟩ to a frame A is given by a function γ : G → A that respects the relations in the following way. Since A is a semilattice under ∧, and FG is the free semilattice over G, γ extends uniquely to a semilattice homomorphism γ′ : (FG, ∪) → (A, ∧) such that γ′({g}) = γ(g). We want for each relation r that

γ′ ∘ λ(r) ≤ ⋁{γ′ ∘ ρ(d) : π(d) = r}

5.2. Theorem. Let T be a geometric theory whose ingredients include a frame presentation as above, and let A be the frame in S[T] presented by it. Then the corresponding locale over [T] classifies the theory T′ that is T extended by –

• a predicate symbol I(g) (g : G)

• an axiom

∀r : R.((∀g∈λ(r). I(g)) ⟶ ∃d : D. (π(d) = r ∧ ∀g∈ρ(d). I(g)))

Proof. Let f : E → [T] be any topos over [T]. We know (by Theorem 2.1) that geometric morphisms over [T] from E to the locale are equivalent to frame homomorphisms in S[T] from A to f_{∗}Ω_{E}, and these are equivalent to functions from G to f_{∗}Ω_{E} that respect the relations. On the other hand, geometric morphisms over [T] from E to [T′] are equivalent to subsets of f^{∗}(G) that satisfy the axiom. We show that these are equivalent, and that suffices to show that the locale and [T′] are equivalent over [T].

Functions γ : G → f_{∗}Ω_{E} are equivalent to functions from f^{∗}G to Ω_{E}, which in turn are equivalent to subsets I of f^{∗}G. The difficult part is to show that the one respects the relations iff the other satisfies the axiom.

Recall some general properties about how f^{∗} and f_{∗} relate to algebras for any finitary algebraic theory. First, because both f_{∗} and f^{∗} preserve finite products, they transform algebras into algebras. (In particular, this gives the distributive lattice structure on f_{∗}Ω_{E}, though not the frame structure – for Mikkelson’s description of joins in f_{∗}Ω_{E} see [Johnstone 77], Proposition 5.36.) Moreover, if X and Y are algebras in S[T] and SE respectively, and θ : X → f_{∗}Y and ϕ : f^{∗}X → Y are adjoint transposes of each other, then θ is a homomorphism iff ϕ is. Finally, if 𝔽 denotes the free algebra construction, then f^{∗} preserves it: f^{∗}𝔽X ≅ 𝔽(f^{∗}X) by an algebra isomorphism in SE (we shall apply this for the theory of semilattices, so that 𝔽 is F). We interrupt the proof of the theorem with a lemma about finitely bounded universal quantification,

5.3. Lemma. Let θ : X → f_{∗}Ω_{E} in S[T] give semilattice homomorphism θ′ : FX → (f_{∗}Ω_{E}, ∧), and let their adjoint transposes be ϕ : f^{∗}X → Ω_{E} and ϕ′ : f^{∗}FX → Ω_{E}. Then the function

≅; ϕ′ : F(f^{∗}X) ≅ f^{∗}FX → Ω_{E}

maps S to the truth value [∀x ∈ S. ϕ(x)].

Proof.

\begin{aligned}& & f^{∗}X & ⟶^{ϕ} & Ω_{E} \\ & ^{\{−\}} ↙ & ↓_{f^{∗}\{−\}} & ↗_{ϕ′} \\ Ff^{∗}X & ⟶_{≅} & f^{∗}FX \end{aligned}  \begin{matrix}X & ⟶^{θ} & f_{∗}Ω_{E} \\ _{\{−\}} ↓ & ↗_{θ′} \\ FX \end{matrix}

In the left-hand diagram, both triangles commute: the left-hand one by definition of the isomorphism, and the right-hand one by naturality of the adjoint transpose. Also, ϕ′ is a semilattice homomorphism (Ω_{E} as ∧-semilattice) because θ′ is. It follows that ≅; ϕ′ is the unique semilattice homomorphism mapping each {x} to ϕ(x), but S ↦ [∀x ∈ S.ϕ(x)] is such a one.

Proof. We now return to the proof of the theorem. From the lemma (applied to γ : G → f_{∗}Ω_{E}), and using naturality, it follows that the adjoint transposes of λ; γ′ : R → f_{∗}Ω_{E} and ρ; γ′ : D → f_{∗}Ω_{E} correspond to the subsets {r : ∀g ∈ f^{∗}λ(r). I(g)} and {d : ∀g ∈ f^{∗}ρ(d). I(g)} of f^{∗}R and f^{∗}D. It remains to show that the adjoint transpose of the function r ↦ ⋁{γ′ ∘ ρ(d) : π(d) = r} from R to f_{∗}Ω_{E} corresponds to the subset

{r : ∃d. (f^{∗}π(d) = r ∧ ∀g∈f^{∗}ρ(d). I(g)}

of f^{∗}R. Our function from R to f_{∗}Ω_{E} calculates the join of a generalized element of Ω_{[T]}^{f_{∗}Ω_{E}}, namely r ↦ {γ′ ∘ ρ(d) : π(d) = r}. The generalized element comes from a function from R × f_{∗}Ω_{E} to Ω_{[T]}, and this corresponds to a subset of R × f_{∗}Ω_{E}, namely the image of ⟨π, γ′ ∘ ρ⟩ : D → R × f_{∗}Ω_{E}. We obtain a function ⟨f^{∗}π, α⟩ : f^{∗}D → f^{∗}R × Ω_{E}, where α : f^{∗}D → Ω_{E} is the adjoint transpose of γ′ ∘ ρ, which by the lemma corresponds to the subset {d : ∀g ∈ f^{∗}ρ(d). I(g)} of f^{∗}D. The image of ⟨f^{∗}π, α⟩ gives a function from f^{∗}R to Ω_{E}^{Ω_{E}},

r ↦ {a ∈ Ω_{E} ∃d : f^{∗}D. (f^{∗}π(d) = r ∧ a = [∀g ∈ f^{∗}ρ(d). I(g)])}

and the join of this set is the truth value [∃d : f^{∗}D. (f^{∗}π(d) = r ∧ ∀g ∈ f^{∗}ρ(d). I(g)], and Mikkelson’s description says that this is the adjoint transpose of

r ↦ ⋁{γ′ ∘ ρ(d) π(d) = r}.

5.4. Corollary. Let E be a topos, let P = (G, R, D, λ, ρ, π) be a frame presentation in SE and let X → E be the corresponding locale over E. Let f : E′ → E be a map. Then the locale X′ over E′ corresponding to the frame presentation f^{∗}(P) in SE′ is the pullback E′ ×_{E} X.

Proof. Let [FrPr][pt] classify a frame presentation together with a point described by predicate I and axiom as in Theorem 5.2. The map [FrPr][pt] → [FrPr] that forgets the point is localic, and is in effect the generic presented locale. The theorem tells us that X ≃ E ×_{[FrPr]} [FrPr][pt] and X′ ≃ E′ ×_{[FrPr]} [FrPr][pt] ≃ E′ ×_{E} X.

Corollary 5.4 enables us to address the geometricity of locale constructions in the following way. Suppose T : Loc → Loc is a functorial construction of locales that can be described intuitionistically. Then for any topos E we have a functor T_{E} : Loc/E → Loc/E. Now suppose we have a map p : E′ → E. If we have a locale X over E, then we have two locales over E′, namely p^{∗}(T_{E}(X)) and T_{E′}(p^{∗}(X)). How do they relate to each other? In general there is no obvious morphism between them. However, we shall be interested in the case where they are isomorphic. In this case we shall say T is geometric, in that it is preserved by pullback along maps.

Corollary 5.4 allows us to use frame presentations to reduce the problem to geometric constructions on sets, in other words those set constructions that are preserved by the inverse image functors. As remarked earlier, the principal geometric set constructions are colimits, finite limits and free algebra constructions, and also universal quantification bounded over (Kuratowski) finite sets.

5.5. Proposition. Let T : Loc → Loc be an intuitionistically describable functorial construction of locales as above, and let T′ be a geometric construction on frame presentations (in other words, an endomorphism T′ : [FrPr] → [FrPr] of the classifying topos for frame presentations). Suppose we have an intuitionistic proof (valid over any topos) that if a (G,R,D)-system P presents a locale X then T′(P) presents (up to homeomorphism) T (X). Then T is geometric.

Proof. We shall write T′_{E} and T_{E} for T′ and T working at stage E. Let f : E′ → E be a map of toposes, and suppose, working over E, that X is a locale presented by P. Then by Corollary 5.4, f^{∗}X is presented over E′ by f^{∗}(P). Hence T_{E′}(f^{∗}X) is presented by T′_{E′}(f^{∗}P). By geometricity of T′ this is isomorphic to f^{∗}(T′_{E}(P)), and that, using Corollary 5.4 again, presents f^{∗}(T_{E}(X)). Hence f^{∗}(T_{E}(X)) ≅ T_{E′}(f^{∗}X) as desired.

In what follows, the set of generators will often have structure (partial order, or meets or joins) that is to be preserved in the frame generated. This can easily be incorporated into the relations and disjuncts, and we use the “qua” notation to indicate that this should be done.

5.6. Definition. Let (G, R, D, λ, ρ, π) be a GRD-system in which G is equipped with a preorder ≤_{G}. Then by

(G (qua preorder), R, D, λ, ρ, π)

we denote the GRD-system

(G, R′, D′, λ′, ρ′, π′)

in which

R′ = R+ ≤_{G}
λ′(r) = λ(r), λ′(g_{1}, g_{2}) = {g_{1}}
D′ = D+ ≤_{G}
ρ′(d) = ρ(d), ρ′(g_{1}, g_{2}) = {g_{2}}
π′ = π+ ≤_{G}

This presents

Fr⟨G| ⋀ λ(r) ≤ ⋁_{π(d)=r} ⋀ ρ(d) (r ∈ R),
g_{1} ≤ g_{2} (g_{1} ≤ g_{2} in G)⟩

which is isomorphic to Fr⟨G (qua preorder)| ⋀ λ(r) ≤ ⋁_{π(d)=r} ⋀ ρ(d) (r ∈ R)⟩.

In fact, we shall find it best to order not only G, but also R and D. The reasons for this will be revealed later. For the moment, let us say first, that we shall sometimes require the joins in the relations to be directed, and that requires an order on D. Second, in satisfying meet and join stability conditions, the generators G get incorporated into both R and D in such a way that the order cannot be neglected.

5.7. Definition. An ordered GRD-system is a system (G (qua poset), R, D, λ, ρ, π) in which G, R and D are equipped with partial orders ≤, π is monotone and λ and ρ are monotone with respect to ≤_{U} on FG.

Notes:

• The orders on R and D make no difference to the frame that is presented.

• We expect the orders to be partial orders and not preorders.

• Ordinary GRD-systems can always be ordered by the discrete order.

5.8. Definition.

1. Let (G, R, D, λ, ρ, π) be an ordered GRD-system in which G is a meet semilattice.

Then by

(G (qua ∧ -semilattice), R, D, λ, ρ, π)

we denote the GRD-system

(G (qua poset), R′, D′, λ′, ρ′, π′)

in which

R′ = R + 1 + G × G
λ′(r) = λ(r), λ′(∗) = ∅, λ′(g_{1}, g_{2}) = {g_{1}, g_{2}}
D′ = D + 1 + G × G
ρ′(d) = ρ(d), ρ′(∗) = {⊤_{G}}, ρ′(g_{1}, g_{2}) = {g_{1} ∧ g_{2}}
π′ = π + 1 + G × G

The extra relations are imposing true ≤ ⊤_{G} and (g_{1}) ∧ (g_{2}) ≤ (g_{1} ∧ g_{2}).

2. Let (G, R, D, λ, ρ, π) be an ordered GRD-system in which G is a join semilattice.

Then by

(G (qua ∨ -semilattice), R, D, λ, ρ, π)

we denote the GRD-system

(G (qua poset), R′, D′, λ′, ρ′, π′)

in which

R′ = R + 1 + G × G
λ′(r) = λ(r), λ′(∗) = {⊥_{G}}, λ′(g_{1}, g_{2}) = {g_{1} ∨ g_{2}}
D′ = D + ∅ + (G × G + G × G)
ρ′(d) = ρ(d), ρ′((g_{1}, g_{2})_{1}) = {g_{1}}, ρ′((g_{1}, g_{2})_{2}) = {g_{2}}
π′ = π+! + ∇

where ∇ is the codiagonal. The extra relations are imposing ⊥_{G} ≤ false and (g_{1} ∨ g_{2}) ≤ (g_{1}) ∨ (g_{2}).

6. Geometricity of internal directed joins

We have already mentioned in Section 2 that Loc is dcpo enriched. However, the directed joins there are as indexed by external directed sets. More deeply we find that if (y_{i}) is a family of maps from X to Y indexed by a directed set I internal to sheaves over X, then they have a directed join ⋁_{i∈I}^{↑} y_{i} : X → Y. Moreover, this is geometric: the directed joins are preserved under pullback along maps into X. (This corresponds at the global level to precomposition preserving directed joins, but we have to be more careful about looking after the directed index set.)

It is convenient to use the “Ω-set” description of sheaves [FoScott 79]. This approach is slightly misleading, since the use of Ω-sets is very specific to locales. It therefore obscures the fact that geometricity of directed joins for locales is just a special case of geometricity of filtered colimits for toposes. However, we retain the account here for its concreteness.

6.1. Definition. Let X be a locale. Then an ΩX-set is a set S equipped with a function E : S^{2} → ΩX, (p, q) ↦ E_{pq}, such that

1. E_{pq} ≤ E_{qp}

2. E_{pq} ∧ E_{qr} ≤ E_{pr}

Working in SX, we find that E defines a partial equivalence relation on S – condition (1) expresses symmetry, and condition (2) expresses transitivity. To put it another way, each point x of X gives a partial equivalence relation ≡_{x} on S, p ≡_{x} q iff x ⊨ E_{pq}, and in SX we consider this for the generic point. Its quotient S/E is an object of SX, i.e. a sheaf over X. (To form the quotient of a partial equivalence relation ≡ on S, you first restrict to S′ = {p ∈ S p ≡ p}, on which ≡ is an equivalence relation, and form S′/ ≡.) It is shown in [FoScott 79] that, with respect to suitable morphisms, the category of ΩX-sets is equivalent to SX, and so ΩX-sets are just another way to describe sheaves over locales.

6.2. Proposition. Let X be a locale. Then a directed set at stage X is a set P equipped with a function L : P × P → ΩX, (p, q) ↦ L_{pq}, that satisfies the following conditions.

1. L_{pq} ≤ L_{pp} ∧ L_{qq}

2. L_{pq} ∧ L_{qr} ≤ L_{pr}

3. true ≤ ⋁_{p∈P} L_{pp}

4. L_{pp} ∧ L_{qq} ≤ ⋁_{r∈P} (L_{pr} ∧ L_{qr})

Proof. Let (P, E) be an ΩX-set. As a binary relation, a partial order is given by a subsheaf of (P/E)^{2}, and this is given by a function L : P × P → ΩX, (p, q) ↦ L_{pq}, satisfying

L_{pq} ∧ E_{p′p} ∧ E_{q′q} ≤ L_{p′q′}
L_{pq} ≤ E_{pp} ∧ E_{qq}

The partial order properties (reflexive, transitive, antisymmetric) are then

E_{pp} ≤ L_{pp}
L_{pq} ∧ L_{qr} ≤ L_{pr}
L_{pq} ∧ L_{qp} ≤ E_{pq}

and directedness is

true ≤ ⋁_{p∈P} E_{pp}
E_{pp} ∧ E_{qq} ≤ ⋁_{r∈P}(L_{pr} ∧ L_{qr})

If we have E and L satisfying these, then we must have E_{pq} = L_{pq} ∧ L_{qp}. The ≥ direction is already hypothesized, and for ≤ we have

E_{pq} = E_{pp} ∧ E_{pp} ∧ E_{pq} ≤ E_{pp} ∧ L_{pp} ∧ E_{pq} ≤ L_{pq}

and E_{pq} ≤ L_{qp} by symmetry. It follows that E_{pp} = L_{pp}, and we can easily deduce the properties listed in the statement.

Conversely, suppose we have L satisfying the stated properties and we define E_{pq} = L_{pq} ∧ L_{qp}. We can then check that (P, E) is an ΩX-set and that L defines a directed partial order on it.

6.3. Proposition. Let X and Y be locales and let P be a directed set at stage X (equipped with order L). Then a P -indexed family of points of Y is a family of maps y_{p} : L_{pp} → Y such that y_{p}|_{L_{pq}} ⊑ y_{q}|_{L_{pq}} : L_{pq} → Y.

Proof. Each element of P/L is represented by an element p of P, but it is only partial – it exists where L_{pp} holds. The corresponding point of Y is a map y_{p} : L_{pp} → Y. The remaining condition represents the monotonicity of the family, if p ≤ q then y_{p} ⊑ y_{q}.

6.4. Theorem. Let X and Y be locales, let P be a directed set over X, and let (y_{p}) be a P -indexed family of points of Y at stage X. Then the directed join ⨆_{p∈P}^{↑} y_{p} is the map y : X → Y defined by

Ωy(b) = ⋁_{p∈P} Ωy_{p}(b)

(Note that we are taking ΩL_{pp} = ↓ L_{pp} ⊆ ΩX.)

Proof. The requirement on y is that it should be the least map from X to Y such that for every p ∈ P we have

y_{p} ⊑ y|_{L_{pp}} : L_{pp} → Y,

in other words that Ωy_{p}(b) ≤ Ωy(b) for every p ∈ P and every b ∈ ΩY. The function Ωy in the statement is clearly the least function from ΩY to ΩX that satisfies this, and so it suffices to show that it is a frame homomorphism.

It is evident that Ωy preserves all joins. For finite meets, first,

Ωy(true) = ⋁_{p∈P} Ωy_{p}(true) = ⋁_{p∈P} L_{pp} = true

For binary meets,

Ωy(b) ∧ Ωy(c) = ⋁_{p∈P} Ωy_{p}(b) ∧ ⋁_{q∈P} Ωy_{q}(c)

= ⋁_{p,q∈P}(Ωy_{p}(b) ∧ Ωy_{q}(c))

= ⋁_{p,q∈P}(Ωy_{p}(b) ∧ Ωy_{q}(c) ∧ L_{pp} ∧ L_{qq})

≤ ⋁_{p,q,r∈P}(Ωy_{p}(b) ∧ Ωy_{q}(c) ∧ L_{pr} ∧ L_{qr})

≤ ⋁_{p,q,r∈P}(Ωy_{r}(b) ∧ Ωy_{r}(c) ∧ L_{pr} ∧ L_{qr})

≤ ⋁_{r∈P} Ωy_{r}(b ∧ c) = Ωy(b ∧ c)

Next we prove that composition of maps distributes on both sides over directed joins. For precomposition, we must explain how to shift the stage of a directed set.

6.5. Proposition. Let X be a locale, let P be a directed set at stage X, and let f : W → X be a map. Then the pullback of P along f, f^{∗}P, is the directed set at stage W with the same underlying set P and with order f^{∗}L defined by

(f^{∗}L)_{pq} = Ωf(L_{pq}) = f^{∗}(L_{pq})

Proof. This is simply the way f^{∗} works with Ω-sets.

6.6. Definition. Let X be a locale, let P be a directed set at stage X, and let f : W → X be a map. If (y_{p}) is a P -indexed family of points of Y, then we denote by (f; y_{p}) the following f^{∗}P -indexed family of points of Y. For each p, let i_{p} : L_{pp} ↪ X be the sublocale inclusion. Then, abusing notation slightly, f; y_{p} here denotes (i_{p}^{∗}f); y_{p} : f^{∗}L_{pp} → L_{pp} → Y.

6.7. Theorem. Let X and Y be locales, let P be a directed set over X, and let (y_{p}) be a P -indexed family of points of Y at stage X.

1. If f : W → X is a map, then

f; ⨆_{p∈P}^{↑} y_{p} = ⨆_{p∈f^{∗}P}^{↑} (f; y_{p})

2. If g : Y → Z is a map, then

(⨆_{p∈P}^{↑} y_{p}); g = ⨆_{p∈P}^{↑} (y_{p}; g)

Proof. 1. We have

Ω(f; ⨆_{p∈P}^{↑} y_{p})(b) = Ωf(⋁_{p} Ωy_{p}(b)) = ⋁_{p} Ωf(Ωy_{p}(b))
Ω(⨆_{p∈f^{∗}P}^{↑} (f; y_{p}))(b) = ⋁_{p} Ω(f; y_{p})(b)

We must therefore show that Ωf(Ωy_{p}(b)) = Ω(f; y_{p})(b) – this is not completely obvious, because we have slightly redefined what f; y_{p} means. If i_{p} : L_{pp} ↪ X is the sublocale inclusion then Ω(f; y_{p})(b) = Ω(i_{p}^{∗}f)(Ωy_{p}(b)), where Ωy_{p}(b) ∈ ΩL_{pp}. But when we identify this with ↓ L_{pp} in ΩX, and make a similar identification for f^{∗}L_{pp}, we find this is equal to Ωf(Ωy_{p}(b)).

2.

Ω((⨆_{p∈P}^{↑} y_{p}); g)(c) = ⋁_{p} Ωy_{p}(Ωg(c))

= ⋁_{p} Ω(y_{p}; Ωg)(c) = Ω(⨆_{p∈P}^{↑} (y_{p}; g))(c)

7. Geometricity of the lower powerlocale

We shall now use the technique of Proposition 5.5 to prove that the powerlocales P_{U} and P_{L}, and hence also the double powerlocale ℙ, are geometric. The argument makes essential use of the coverage theorems, by which frame presentations are transformed into suplattice or preframe presentations.

We deal first with the suplattice coverage theorem, which is Johnstone’s original form [Johnstone 82].

7.1. Theorem. [Suplattice coverage theorem] Let S be a meet semilattice, and let C ⊆ S × PS have the following properties. (If (x, U) ∈ C then we say that U covers x.)

• If U covers x and u ∈ U then u ≤ x.

• ( Meet stability) If U covers x and y ∈ S then {y ∧ u u ∈ U} covers y ∧ x.

Then

Fr⟨S (qua meet semilattice)|x ≤ ⋁ U (U covers x)⟩
≅ SupL⟨S (qua poset)|x ≤ ⋁ U (U covers x)⟩

Proof. [Johnstone 82] proved that the frame presented on the left can be represented concretely as the lattice of “C-ideals”. It was proved in [AbrVic 93] that this lattice could be given the suplattice presentation on the right. The arguments used there are constructive.

THE DOUBLE POWERLOCALE AND EXPONENTIATION  397

7.2. Definition. A site is an ordered GRD-system of the form (G (qua ∧-semilattice), R, D) equipped with the following structure and properties.

1. Factorizations of λ and ρ via the singleton embedding {−} : G → FG, λ(r) = {λ_{0}(r)} and ρ(d) = {ρ_{0}(d)}.

2. ρ_{0}(d) ≤ λ_{0}(π(d)).

3. Actions of G on R and D, denoted (g, r) ⟼ g · r and (g, d) ⟼ g · d.

4. The functions · : G × R → R and · : G × D → D are both monotone.

5. π(g · d) = g · π(d)

6. If π(d′) = g · r then there is some d such that π(d) = r and d′ ≤ g · d.

7. λ_{0}(g · r) = g ∧ λ_{0}(r)

8. ρ_{0}(g · r) = g ∧ ρ_{0}(r)

This is mostly just a formalization in terms of GRD-systems of the conditions used in Theorem 7.1, so it is not surprising that we now have the following. 7.3. Corollary. Let (G, R, D) be a site, and let X be presented by (G (qua ∧- semilattice), R, D). Then P_{L} X is presented by (G (qua poset), R, D). Proof. We define a coverage relation C ⊆ G × PG whose elements are the pairs

(λ_{0}(r), {ρ_{0}(d) π(d) = r})

for r ∈ R. The fact that it is a coverage comes from the structure of the site; in particular the G-action on R and D gives meet stability. Then ΩX is

Fr⟨G (qua ∧ -semilattice)|x ≤ ⋁ U (U covers x)⟩

Using Theorem 7.1 we see that

Ω P_{L} X ≅ Fr⟨ΩX (qua suplattice)⟩
≅ Fr⟨G (qua poset)|x ≤ ⋁ U (U covers x)⟩

and this is presented by (G (qua poset), R, D).

In the light of this, geometricity of the lower powerlocale reduces to showing that any presentation can be geometrically transformed into an equivalent site. First, however, we take the opportunity to prove a Lemma, probably well-known, that will be useful in various places.

7.4. Lemma.

1. Let P be a poset. Then FP/ ≤_{L} is a free join semilattice over P (qua poset).

2. Let P be a poset. Then FP/ ≤_{U} is a free meet semilattice over P (qua poset).

3. Let P be a meet semilattice. Then FP/ ≤_{L} is a free distributive lattice over P (qua meet semilattice).

Proof. 1. ∅ and ∪ in FP provide (nullary and binary) joins with respect to ≤_{L}. For instance, U ≤_{L} U ∪ V, and if U ≤_{L} W and V ≤_{L} W then U ∪ V ≤_{L} W. The singleton embedding of P in FP, x ↦ {x}, is monotone with respect to ≤_{L}: if x ≤ y then {x} ≤_{L} {y}.

Now let S be a join semilattice and f : P → S monotone. This extends uniquely to a semilattice homomorphism f_{1} : FP → S, U ⟼ ⋁{f(u) u ∈ U}, and this factors via FP/ ≤_{L}: if U ≤_{L} V then f_{1}(U) ≤ f_{1}(V).

2. This follows by duality from the fact that S ≤_{U} T iff T (≥)_{L}S. Hence a meet semilattice homorphism from FP/ ≤_{U} to S is equivalent to a join semilattice homomorphism from F(P^{op})/ ≤_{L} to S^{op}, which is equivalent to a monotone function from P^{op} to S^{op} and hence to a monotone function from P to S.

3. The top element is {⊤_{P} }, and binary meets are defined by

U ∧ V = {u ∧ v u ∈ U, v ∈ V }

We have U ∧ V ≤_{L} U and if W ≤_{L} U and W ≤_{L} V then W ≤_{L} U ∧ V. For distributivity we have

U ∧ (V ∪ W) ≤_{L} (U ∧ V) ∪ (U ∧ W)

Suppose S is a distributive lattice and f : P → S a meet semilattice homomorphism. Then the unique extension to a join semilattice homomorphism f_{2} : FP/ ≤_{L} → S is in fact a lattice homomorphism, for

f_{1}(U ∧ V) = f_{1}({u ∧ v u ∈ U, v ∈ V })
= ⋁{f(u) ∧ f(v) u ∈ U, v ∈ V }
= f_{1}(U) ∧ f_{1}(V)

If U ∈ FP then we shall write [U] for its image in FP/ ≤_{U} or FP/ ≤_{L} as appropriate.

7.5. Theorem. The lower powerlocale P_{L} is geometric.

1. If X is presented by an ordered GRD-system (G (qua poset), R, D), then P_{L} X is presented by a system (G′ (qua poset), R′, D′) where

G′ = FG/ ≤_{U}
R′ = G′ × R
λ(S, r) = {S ∧ λ(r)}
D′ = G′ × D
ρ(S, d) = {S ∧ ρ(d) ∧ λ(π(d))}
π = G′ × π

2. Ω ↓ takes [U] ⟼ ⋀ U, Ω ⨆ takes [U] ⟼ [{[U]}].

3. Let X_{i} be presented by (G_{i} (qua poset), R_{i}, D_{i}) (i = 1, 2). Let f : X_{1} → X_{2} be a map, and suppose ϕ ⊆ FG_{1} × G_{2} is such that, for g ∈ G_{2},

Ωf(g) = ⋁{⋀ S (S, g) ∈ ϕ}.

Let

ϕ′ = {({ ⋃_{(S,g)∈ϕ_{0}} S}, V) ϕ_{0} ∈ Fϕ, F snd ϕ_{0} = V } ⊆ FFG_{1} × FG_{2}.

Then P_{L} f is similarly described by ϕ′,

Ω P_{L} f([V]) = ⋁{ ⋀_{U∈U}[U] (U, V) ∈ ϕ′}.

Proof. 1. If U ∈ FG, let us write [U] for its image in G′.

We have

ΩX = Fr⟨G (qua poset)| ⋀ λ(r) ≤ ⋁_{π(d)=r} ⋀ ρ(d) (r ∈ R)⟩
≅ Fr⟨G′ (qua ∧ -semilattice)|

S ∧ [λ(r)] ≤ ⋁_{π(d)=r}(S ∧ [ρ(d)] ∧ [λ(r)]) (r ∈ R, S ∈ G′)⟩

This is shown by demonstrating the mutually inverse frame homomorphisms. α from left to right is defined by α(g) = [{g}], β from right to left by β([U]) = ⋀ U, using Lemma 7.4 (2).

We must still check that the relations are respected, but once that is done the two homomorphisms will be mutually inverse. On one side, β ∘ α(g) = β([{g}]) = g. On the other we have

α ∘ β([{g}]) = α(g) = [{g}]

after which α ∘ β = Id by Lemma 7.4.

Now we check that the relations are respected. From left to right, there is only one. We have

α(⋀ λ(r)) = ⋀_{g∈λ(r)}[{g}] = [ ⋃_{g∈λ(r)}{g}] = [λ(r)]
≤ ⋁_{π(d)=r}[ρ(d)] = ⋁_{π(d)=r} ⋀_{g∈ρ(d)}[{g}]
= α( ⋁_{π(d)=r} ⋀ ρ(d)).

Going from right to left, we have

β(S ∧ [λ(r)]) = β(S) ∧ ⋀ λ(r)
≤ β(S) ∧ ⋁_{π(d)=r} ⋀ ρ(d) ∧ ⋀ λ(r)
= ⋁_{π(d)=r}(β(S) ∧ ⋀ ρ(d) ∧ ⋀ λ(r))
= β( ⋁_{π(d)=r}(S ∧ [ρ(d)] ∧ [λ(r)])

The right-hand presentation corresponds to the GRD-system described, and moreover it is a site, with G′-actions given by

S · (T, r) = (S ∧ T, r)
S · (T, d) = (S ∧ T, d)

The result now follows from Corollary 7.3.

2. U ∈ FG represents ♢ ⋀_{g∈U} g ∈ Ω P_{L} X. Under Ω ↓, this maps to ⋀ U. Under Ω ⨆, it maps to ♢♢ ⋀_{g∈U} g, which corresponds to [{[U]}].

3. Under Ω P_{L} f, ♢ ⋀_{g∈V} g maps to

♢ ⋀_{g∈V} ⋁_{(S,g)∈ϕ} ⋀ S

If V ∈ FG, let us write

Φ(V) = {ϕ_{0} ∈ Fϕ ∀(S, g) ∈ ϕ_{0}. g ∈ V and ∀g ∈ V. ∃(S, g) ∈ ϕ_{0}}
= {ϕ_{0} ∈ Fϕ F snd(ϕ_{0}) = V }

We must therefore show that

⋀_{g∈V} ⋁_{(S,g)∈ϕ} ⋀ S = ⋁_{ϕ_{0}∈Φ(V)} ⋀_{(S,g)∈ϕ_{0}} ⋀ S

For ≥, suppose we have ϕ_{0} ∈ Φ(V), and we have h ∈ V. We can find (T, h) ∈ ϕ_{0} for some T, so

⋀_{(S,g)∈ϕ_{0}} ⋀ S ≤ ⋀ T ≤ ⋁_{(S,h)∈ϕ} ⋀ S

For ≤, we use induction on V (see [Vickers 99]). If V = ∅, then the LHS is true. For the RHS, the only possible ϕ_{0} is ∅ and it follows that the RHS also is true. For the induction step, suppose V = V′ ∪ {h}.

LHS = ⋀_{g∈V′} ⋁_{(S,g)∈ϕ} ⋀ S ∧ ⋁_{(T,h)∈ϕ} ⋀ T
= ⋁_{ϕ_{0}∈Φ(V′)} ⋀_{(S,g)∈ϕ_{0}} ⋀ S ∧ ⋁_{(T,h)∈ϕ} ⋀ T
= ⋁{  ⋀_{(S,g)∈ϕ_{0}∪{(T,h)}} ⋀ S ϕ_{0} ∈ Φ(V′), (T, h) ∈ ϕ}
≤ ⋁_{ϕ_{0}∈Φ(V)} ⋀_{(S,g)∈ϕ_{0}} ⋀ S

Hence

♢ ⋀_{g∈V} ⋁_{(S,g)∈ϕ} ⋀ S = ⋁_{ϕ_{0}∈Φ(V)} ♢ ⋀_{(S,g)∈ϕ_{0}} ⋀ S = ⋁_{ϕ_{0}∈Φ(V)} ♢ ⋀( ⋃_{(S,g)∈ϕ_{0}} S)

which gives us the result.

8. Geometricity of the upper powerlocale

Turning now to the upper powerlocale, we first define a preframe analogue of site.

8.1. Definition. An ordered GRD-system (G (qua ∨-semilattice), R, D) is a preframe site if it has the following structure and properties.

1. For each r in R, the set D_{r} = {d ∈ D π(d) = r} is directed under ≤.

2. For each d in D, ρ(d) ≤_{U} λ(π(d)).

3. Actions of G on R and D, denoted (a, r) ↦ a ∗ r and (a, d) ↦ a ∗ d.

4. The functions ∗ : G × R → R and ∗ : G × D → D are both monotone.

5. π(a ∗ d) = a ∗ π(d).

6. If π(d′) = g ∗ r then there is some d such that π(d) = r and d′ ≤ g ∗ d.

7. λ(a ∗ r) ≡_{U} {a ∨ b b ∈ λ(r)}.

8. ρ(a ∗ d) ≡_{U} {a ∨ b b ∈ ρ(d)}.

Conditions 1 and 2 here say that the relations are all of the form

⋀ S ≤ ⋁_{i}^{↑} ⋀ T_{i}

with a directed join on the right, such that each ⋀ T_{i} ≤ ⋀ S. Conditions 3-8 express a join stability property, namely that if we have such a relation in R, and a ∈ G, then we also have the relation

⋀{a ∨ b b ∈ S} ≤ ⋁_{i}^{↑} ⋀{a ∨ b b ∈ T_{i}}

8.2. Theorem. [Preframe coverage theorem] Let (G, R, D) be a preframe site. Then

Fr⟨G (qua join semilattice)| ⋀ λ(r) ≤ ⋁_{π(d)=r}^{↑} ⋀ ρ(d) (r ∈ R)⟩
≅ PreFr⟨G (qua poset)| ⋀ λ(r) ≤ ⋁_{π(d)=r}^{↑} ⋀ ρ(d) (r ∈ R)⟩

Proof. [JoVic 91] The first task is to show that the preframe presented on the right actually exists. Once that is done, binary joins can be defined as preframe bilinear maps, and proved to be joins.

8.3. Corollary. Let (G, R, D) be a preframe site, and let X be presented by (G (qua ∨-semilattice), R, D). Then P_{U} X is presented by (G (qua poset), R, D).

We shall now show that the upper powerlocale P_{U} is geometric. Just as for P_{L}, the strategy is to show how to manipulate an arbitrary presentation into an equivalent preframe site. However, in doing so we shall also need to use finite distributivity and we must first say something about the geometric nature of that.

Let X be a distributive lattice and V a finite set of finite subsets of X. As ever, “finite” here means Kuratowski finite, so V ∈ FFX. We are interested in the problem of writing the join of meets

⋁_{V ∈V} ⋀ V

as a meet of joins. If one imagines writing this out, one finds that each of the joins has a disjunct from each V in V, so

⋁_{V ∈V} ⋀ V = ⋀{ ⋁_{V ∈V} γ(V)|γ a choice function for V}

A choice function for V is a function γ : V → ⋃ V such that γ(V) ∈ V for every V. Since V is finite, the graph of γ must be a finite subset of V× ⋃ V, but unfortunately the set of such γ’s is not a geometrically definable subset of F(V× ⋃ V). This is because the single-valuedness property of a function, ∀V, v, v′. (V γv ∧ V γv′ → v = v′), is not geometric. (To make it so we should need decidable equality on X, when the property can be expressed as ∀(V, v) ∈ γ. ∀(V′, v′) ∈ γ. (V ≠ V′ ∨ v = v′).) However, it turns out that single-valuedness is not needed for our applications. We can make do with choice relations that are total but not necessarily single-valued.

8.4. Definition. Let X be a set and V ∈ FFX. A choice for V is some γ ∈ F(V× ⋃ V) satisfying

• ∀V ∈ V. ∃v ∈ V. (V, v) ∈ γ

• ∀(V, v) ∈ γ. v ∈ V

8.5. Definition. We write Ch(V) for the set of choices of V, and Im γ for the image of γ, i.e. its direct image under the second projection to ⋃ V (note that Im γ is finite).

8.6. Proposition. Let X be a set and V ∈ FFX. Then Ch(V) is finite.

Proof. We use the “F-recursion” of [Vickers 99] to define a function Ch : FFX → FF(FX×X) and show that γ ∈ F(FX×X) is in Ch(V) iff it is a choice of V as defined above.

First, Ch(∅) = {∅}. ∅ is, vacuously, a choice of ∅, and it is the only finite subset of ∅× ⋃ ∅.

Next,

Ch(V ∪ {U}) = {γ ∪ ({U} × S) γ ∈ Ch(V) and S ∈ F^{+}U}

(F^{+}U denotes the set of nonempty finite subsets of U – note that for finite sets, emptiness is decidable.) There are two proof obligations to be discharged in showing that this definition is good. For W ∈ FF(FX×X) and U ∈ FX let us write

Φ(W, U) = {γ ∪ ({U} × S) γ ∈ W and S ∈ F^{+}U}

so we are attempting to define Ch to satisfy

Ch(V ∪ {U}) = Φ(Ch V, U)

Then we must show

Φ(Φ(W, U), V) = Φ(Φ(W, V), U)
Φ(Φ(W, U), U) = Φ(W, U)

Both of these are easy and we deduce by F-recursion that Ch is well-defined. Now for correctness, we can suppose by induction that Ch(V) is correct (i.e. the set of choices of V). Then clearly all the elements of Ch(V ∪ {U}) are choices of V ∪ {U}. Conversely, let γ be a choice of V ∪ {U}, and write γ = γ_{1} ∪ γ_{2} where the γ_{i}s are both finite, for every (V, v) in γ_{1} we have V in V, and for every (V, v) in γ_{2} we have V = U. (If U ∈ V then γ_{1} and γ_{2} are not uniquely defined. Because this possibilitiy cannot be eliminated geometrically, the reasoning is slightly more elaborate than one might have expected.) We have ∀V ∈ V. ∃v ∈ V. (V, v) ∈ γ, and so there is a finite total relation R from V to ⋃ V contained in γ. Replacing γ_{1} by γ_{1} ∪ R we can suppose that γ_{1} is total on V. We also have some u ∈ U such that (U, u) ∈ γ, so replacing γ_{2} by γ_{2} ∪ {(U, u)} we can suppose that γ_{2} is of the form {U} × S for some finite non-empty set S. Hence γ ∈ Ch(V ∪ {U}).

8.7. Theorem. Let L be a distributive lattice and let V ∈ FFL. Then

⋁_{V ∈V} ⋀ V = ⋀_{γ∈Ch(V)} ⋁ Im γ.

Proof. By F-induction on V. (See [Vickers 99]. Note that this is not induction on the cardinality of V, which in general does not exist. Rather, it is is induction on the length of an enumeration of V.) If V is empty, then the LHS is ⊥_{L} and the RHS is ⋀_{γ∈{∅}} ⋁ ∅ = ⊥_{L}. For the induction step,

⋁_{V′∈{V }∪V} ⋀ V′ = ⋀ V ∨ ⋁_{V′∈V} ⋀ V′ = ⋀ V ∨ ⋀_{γ′∈Ch(V)} ⋁ Im γ′

= ⋀_{v∈V,γ′∈Ch(V)}(v ∨ ⋁ Im γ′) = ⋀_{γ∈Ch(V)} ⋁ Im γ

Of course, there is a dual result in which meets and joins are interchanged.

8.8. Theorem. The upper powerlocale P_{U} is geometric.

1. If X is presented by an ordered GRD-system (G (qua poset), R, D), then P_{U} X is presented by a system (G′ (qua poset), R′, D′) where

G′ = FG/ ≤_{L}
R′ = G′ × R
λ(S, r) = {S ∨ [{g}] g ∈ λ(r)}
D′ = {(S, D_{0}, r) ∈ G′ × FD × R|∀d ∈ D_{0}. π(d) = r}/(≤ × ≤_{L} × ≤)
ρ(S, D_{0}, r) = {(S ∨ [Im γ]) γ ∈ Ch{λ(r) ∪ ρ(d)|d ∈ D_{0}}}
π(S, D_{0}, r) = (S, r)

2. Ω ↑ takes [U] ⟼ ⋁ U, Ω⊓ takes [U] ⟼ [{[U]}].

3. Let X_{i} be presented by (G_{i} (qua poset), R_{i}, D_{i}) (i = 1, 2). Let f : X_{1} → X_{2} be a map, and suppose ϕ ⊆ FG_{1} × G_{2} is such that, for g ∈ G_{2},

Ωf(g) = ⋁{⋀ S (S, g) ∈ ϕ}.

Let

ϕ′ = {({Im γ γ ∈ Ch({S (S, g) ∈ ϕ_{0}})}, V)|ϕ_{0} ∈ Fϕ, F snd ϕ_{0} ⊆ V }
⊆ FFG_{1} × FG_{2}

Then P_{U} f is similarly described by ϕ′,

P_{U} f([V]) = ⋁{ ⋀_{U∈U}[U] (U, V) ∈ ϕ′}

Proof. 1. Note that (G′ (qua ∨ -semilattice), R′, D′) is a preframe site. To show ρ is well-defined, suppose S ≤ S′, D_{0} ≤_{L} D′_{0} and r ≤ r′. We must show that ρ(S, D_{0}, r) ≤_{U} ρ(S′, D′_{0}, r′). Suppose

γ′ ∈ Ch{λ(r′) ∪ ρ(d′)|d′ ∈ D′_{0}}.

For every d ∈ D_{0} we can find d′ ∈ D′_{0} with d ≤ d′. Then

λ(r) ∪ ρ(d) ≤_{U} λ(r′) ∪ ρ(d′).

We can find g′ ∈ λ(r′) ∪ ρ(d′) with (d′, g′) ∈ γ′ and then g ∈ λ(r) ∪ ρ(d) with g ≤ g′. It follows that there is some γ ∈ Ch{λ(r) ∪ ρ(d) d ∈ D_{0}} such that if (d, g) ∈ γ, then there is some (d′, g′) ∈ γ′ such that d ≤ d′ and g ≤ g′. Then S ∨ Im γ ≤ S′ ∨ Im γ′, because Im γ ≤_{L} Im γ′.

To show condition 2 in Definition 8.1 we must show ρ(S, D_{0}, r) ≤_{U} λ(S, r). If g ∈ λ(r), so S ∨ [{g}] ∈ λ(S, r), then D_{0} × {g} is a constant choice for {λ(r) ∪ ρ(d) d ∈ D_{0}} and its image is {g}. Hence S ∨ [{g}] ∈ ρ(S, D_{0}, r).

The G′-actions are given by

S ∗ (T, r) = (S ∨ T, r)
S ∗ (T, D_{0}, r) = (S ∨ T, D_{0}, r)

Once we have shown that it is equivalent to (G (qua poset), R, D), we can apply Corollary 8.3.

We have

ΩX = Fr⟨G (qua poset)| ⋀λ(r) ≤ ⋁_{π(d)=r} ⋀ ρ(d) (r ∈ R)⟩
≅ Fr⟨G (qua poset)| ⋀λ(r) ≤ ⋁_{π(d)=r} ⋀(λ(r) ∪ ρ(d)) (r ∈ R)⟩
≅ Fr⟨G (qua poset)|

⋀ λ(r) ≤ ⋁_{D_{0}∈F_{r}D}^{↑} ⋁_{d∈D_{0}} ⋀(λ(r) ∪ ρ(d)) (r ∈ R)⟩

where

F_{r}D = {D_{0} ∈ FD ∀d ∈ D_{0}. π(d) = r}

To handle the distributivity, let us write

U(r, D_{0}) = {λ(r) ∪ ρ(d) d ∈ D_{0}}

Then

ΩX ≅ Fr⟨G (qua poset)|
⋀ λ(r) ≤ ⋁_{D_{0}∈F_{r}D}^{↑} ⋀{⋁ Im γ γ ∈ Ch U(r, D_{0})} (r ∈ R)⟩
≅ Fr⟨G (qua poset)|
⋀{⋁ V ∨ g g ∈ λ(r)}
≤ ⋁_{D_{0}∈F_{r}D}^{↑} ⋀{⋁ V ∨ ⋁ Im γ|γ ∈ Ch U(r, D_{0})}
(r ∈ R, V ∈ FG)⟩
≅ Fr⟨G′ (qua ∨ -semilattice)|
⋀{(S ∨ [{g}]) g ∈ λ(r)}
≤ ⋁_{D_{0}∈F_{r}D}^{↑} ⋀{S ∨ [Im γ]|γ ∈ Ch U(r, D_{0})}
(r ∈ R, S ∈ G′)⟩

This is what is presented by the preframe site

(G′ (qua ∨-semilattice), R′, D′)

and we are done.

2. V ∈ FG represents □ ⋁_{g∈V} g ∈ Ω P_{U} X. Under Ω ↑, this maps to ⋁ V. Under Ω⊓, it maps to □□ ⋁_{g∈V} g, which corresponds to [{[V]}].

3. For V ∈ FG_{2}, let us write

Ψ(V) = {ϕ_{0} ∈ Fϕ F snd(ϕ_{0}) ⊆ V }

Under Ω P_{U} f, □ ⋁_{h∈V} h maps to

□ ⋁_{h∈V} ⋁_{(S,h)∈ϕ} ⋀ S = □ ⋁_{ϕ_{0}∈Ψ(V)}^{↑} ⋁_{(S,g)∈ϕ_{0}} ⋀ S

= ⋁_{ϕ_{0}∈Ψ(V)}^{↑} □ ⋀_{γ∈Ch({S(S,g)∈ϕ_{0}})} ⋁ Im γ

= ⋁_{ϕ_{0}∈Ψ(V)}^{↑} ⋀_{γ∈Ch({S(S,g)∈ϕ_{0}})} □ ⋁ Im γ

9. Geometricity of the double powerlocale

By combining Theorems 7.5 and 8.8 we already have :

9.1. Theorem. The double powerlocale is geometric.

However, we shall gain more useful information by considering presentations for which the generators form a distributive lattice and all the relations are of the form

g ≤ ⋁_{i}^{↑} h_{i}

with every h_{i} ≤ g.

9.2. Definition. An ordered GRD-system (G (qua DL), R, D) (G being a distributive lattice, i.e. DL) is a DL-site iff it is equipped with structure and properties to make (G (qua ∧ -semilattice), R, D) a site and (G (qua ∨ -semilattice), R, D) a preframe site.

9.3. Theorem. Suppose a locale X is presented by a DL-site (G (qua DL), R, D). Then ℙX is presented by (G (qua poset), R, D).

Proof. Consider the relations expressing preservation of finite joins in G:

⊥_{G} ≤ ⋁ ∅
(a ∨ b) ≤ (a) ∨ (b)

By distributivity these are meet-stable. It follows that if we add them to R and D to give new sets R′ and D′, then (G (qua ∧-semilattice), R′, D′) is a site, equivalent to (G (qua DL), R, D). Hence by Theorem 7.3, P_{L} X is presented by (G (qua poset), R′, D′), which is equivalent to (G (qua ∨-semilattice), R, D). This is a preframe site, and so by Theorem 8.3 we have that ℙX ≅ P_{U} P_{L} X is presented by (G (qua poset), R, D).

We now proceed to show that every presentation can be transformed into a DL-site.

9.4. Lemma. Let (G (qua ∧-semilattice), R, D) be a site. Then it is equivalent to a DL-site (G′ (qua DL), R′, D′) where

G′ = FG/ ≤_{L}
R′ = G′ × FR/ ≤_{L}
λ_{0}(S, U) = S ∨ [{λ_{0}(r) r ∈ U}]
D′ = {(S, D_{0}, U) ∈ G′ × FD × FR|Fπ(D_{0}) ⊆ U}/(≤ × ≤_{L} × ≤_{L})
π(S, D_{0}, U) = (S, U)
ρ_{0}(S, D_{0}, U) = S ∨ [{ρ_{0}(d) d ∈ D_{0}}]
T ∗ (S, U) = (T ∨ S, U)
T ∗ (S, D_{0}, U) = (T ∨ S, D_{0}, U)
T · (S, U) = (T ∧ S, {t · r t ∈ T, r ∈ U})
T · (S, D_{0}, U) = (T ∧ S, {t · d t ∈ T, d ∈ D_{0}}, {t · r t ∈ T, r ∈ U})

(Note: in expressions such as {t · r t ∈ T, r ∈ U} we have treated T and U as though they were actual sets rather than as sets modulo ≤_{L}. The well-definedness of the expressions is easily checked; for instance, if T ≤_{L} T′ then {t · r t ∈ T, r ∈ U} ≤_{L} {t · r t ∈ T′, r ∈ U}.)

Proof. We must show that

Fr⟨G (qua ∧ -semilattice)|λ_{0}(r) ≤ ⋁_{π(d)=r} ρ_{0}(d) (r ∈ R, S ∈ G′)⟩

is isomorphic to

Fr⟨FG/ ≤ L (qua DL)|

⋁ S ∨ ⋁_{r∈U} λ_{0}(r) ≤ ⋁^{↑}{⋁ S ∨ ⋁_{d∈D_{0}} ρ_{0}(d) Fπ(D_{0}) ⊆ U} (U ∈ FR, S ∈ FG)⟩

This is routinely proved by constructing mutually inverse homomorphisms, much as in Theorem 7.5.

It is also necessary to show that the structure described is indeed that of a DL-site. The trickiest part is ·. For instance, we have

λ_{0}(T · (S, U)) = (T ∧ S) ∨ ⋁{λ_{0}(t · u) t ∈ T, u ∈ U}
= (T ∧ S) ∨ ⋁{t ∧ λ_{0}(u) t ∈ T, u ∈ U}
= (T ∧ S) ∨ (T ∧ ⋁{λ_{0}(u) u ∈ U})
= T ∧ λ_{0}(S, U)

For condition 6 for a site, suppose π(S′, D′_{0}, U′) = T · (S, U), so S′ = T ∧ S and U′ = {t · r t ∈ T, r ∈ U}. For each d′ ∈ D′_{0}, we have π(d′) ∈ U′ and so we can find t ∈ T and r ∈ U such that π(d′) = t · r, and then d such that π(d) = r and d′ ≤ t · d. Hence we can find D_{0} ∈ FD such that Fπ(D_{0}) ⊆ U and D′_{0} ≤_{L} {t · d t ∈ T, d ∈ D_{0}}. Then π(S, D_{0}, U) = (S, U) and (S′, D′_{0}, U′) ≤ T · (S, D_{0}, U).

9.5. Theorem. Every presentation can be geometrically transformed into an equivalent one given by a DL-site.

Proof. By Theorem 7.5, any presentation is equivalent to one given by a site; and then Lemma 9.4 it is equivalent to one given by a DL-site.

10. Geometricity of exponentiation of locales

We use the ordinary categorical definition of exponentiation.

10.1. Definition. Let X and Y be locales. Then the exponential Y^{X} is a locale equipped with a map ev : Y^{X} × X → Y, the evaluation map, such that the two functors Loc(−, Y^{X}) and Loc(− × X, Y) from Loc to Set are naturally isomorphic under the transformation g ↦ (g × Id_{X}); ev.

If f : Z × X → Y then we write ^{⌜}f^{⌝} : Z → Y^{X} for its corresponding exponential transpose.

This is all completely standard. Note, however, that the natural isomorphism is necessarily an order isomorphism, with respect to the order enrichment ⊑ (the specialization order) on Loc. This is because for any locales Z and W, a pair of maps f, g : Z → W with f ⊑ g is equivalent to a map from 𝕊 × Z → W.

10.2. Proposition. Let X, Y and Z be locales. Then Z is an exponential Y^{X} iff there is a geometric bijection between points of Z and maps from X to Y.

By “geometric bijection”, we mean a bijection at every stage that is preserved by pullback along maps.

Proof. ⇒: Let ev : Z × X → Y be the evaluation map. Consider stage W. Points of Z over W are equivalent to global maps z : W → Z, and maps X → Y over W are equivalent to global maps W ×X → Y. By the definition of exponential there is a bijection between these, under which z corresponds to y = (z × Id_{X}); ev. To show geometricity, suppose f : W′ → W is a map. Under pullback along f, we find z and y become f; z and (f × Id_{X}); y, which still correspond under the bijection at W′.

⇐: At stage Z, let the generic point Id_{Z} correspond to a map ev : Z × X → Y. At any stage W, geometricity tells us that maps z : W → Z correspond to (z × Id_{X}); ev as required for the exponential.

10.3. Proposition. Exponentiation – when it exists – is preserved by pullback.

Proof. This essentially follows from the previous proposition. Suppose Z is an exponential Y^{X} at stage W (X, Y and Z are locales over W), and suppose f : W′ → W. For stages previous to W′, i.e. maps W′′ → W′, we have the geometric bijection between points of Z and maps X → Y, but this amounts to a geometric bijection between points of f^{∗}Z and maps f^{∗}X → f^{∗}Y. Hence f^{∗}Z is an exponential (f^{∗}Y)^{(f^{∗}X)} over W′.

The standard account ([Hyland 81]; or see [Johnstone 82] for a slightly different development) says –

• If 𝕊^{X} exists then ΩX is a continuous lattice.

• If ΩX is a continuous lattice then Y^{X} exists for every locale Y.

We shall not assume these results, but our geometric development of ℙ will prove them along the way.

11. The first main result

In this section we shall prove the following.

11.1. Theorem. Let X be a locale for which the exponential 𝕊^{X} exists. Then 𝕊^{𝕊^{X}} also exists, and is homeomorphic to ℙX.

Hence 𝕊^{(−)} is a kind of partial square root for ℙ = P_{U} ∘ P_{L}.

Throughout the section (and the next section too), let X be a locale for which the exponential 𝕊^{X} exists. We suppose further that (G_{X} (qua DL), R_{X}, D_{X}) and (G_{𝕊^{X}} (qua DL), R_{𝕊^{X}}, D_{𝕊^{X}}) are DL-sites presenting X and 𝕊^{X}.

11.2. Definition. We write In : X × 𝕊^{X} → 𝕊 for the reverse of ev : 𝕊^{X} × X → 𝕊. We also write In for the corresponding open of X × 𝕊^{X} (an element of Ω(X × 𝕊^{X})) or for the open sublocale In ↪ X × 𝕊^{X}.

Since G_{X} and G_{𝕊^{X}} are bases for X and 𝕊^{X}, the opens b × V (b ∈ G_{X}, V ∈ G_{𝕊^{X}}) provide a basis for X × 𝕊^{X}. Hence there is a subset In_{0} of G_{X} × G_{𝕊^{X}} such that In = ⋁{b × V |⟨b, V ⟩ ∈ In_{0}}.

11.3. Definition. Let W ⊆ G_{X} × G_{𝕊^{X}}. We say W is a finitely bilinear ideal iff

1. W is lower closed under ≤ × ≤.

2. If b ∈ G_{X}, V ∈ FG_{𝕊^{X}}, and for every V ∈ V we have ⟨b, V ⟩ ∈ W, then ⟨b, ⋁ V⟩ ∈ W.

3. If U ∈ FG_{X}, V ∈ G_{𝕊^{X}}, and for every b ∈ U we have ⟨b, V ⟩ ∈ W, then ⟨⋁ U, V ⟩ ∈ W.

11.4. Lemma. Given W ⊆ G_{X} × G_{𝕊^{X}}, we can construct, intuitionistically, a finitely bilinear ideal \overline{W} such that

⋁\{b × V ⟨b, V ⟩ ∈ \overline{W} \} = ⋁\{b × V ⟨b, V ⟩ ∈ W \}

Proof. \overline{W} is \{⟨b, V ⟩ ∈ G_{X} × G_{𝕊^{X}}|b × V ≤ ⋁\{b′ × V′ ⟨b′, V′⟩ ∈ W \}\}.

(For present purposes, the intuitionistic construction (valid in any category of sheaves) is enough, for the property of being a finitely bilinear ideal with the required properties is geometric. However, we conjecture that \overline{W} can be constructed geometrically from W.)

It follows that, without loss of generality, we can assume that In_{0} is a finitely bilinear ideal.

The map In can be understood as an open in three ways. It is an open of X × 𝕊^{X}, but also over 𝕊^{X} it is an open of X (which is how we shall often view it in this section), while over X it is an open of 𝕊^{X} (which is more the viewpoint of the next section). Intuitionistic reasoning (valid in toposes) allows us to exploit these three viewpoints, but it is the more stringent geometric reasoning that allows us to move continuously between them. For instance, working over 𝕊^{X} we view In as an open of X and can therefore find an open ⊠ In of ℙX. But that is ℙX constructed working over 𝕊^{X}, and it is the detailed geometricity arguments that allow us to view ⊠ In as a global open of ℙX × 𝕊^{X}. We shall look at this more closely in due course.

If ^{⌜}a^{⌝} is a point of 𝕊^{X}, then its exponential transpose a : X → 𝕊 has a(x) = In⟨x,^{⌜}a^{⌝}⟩ for each point x of X, and so we see that x ⊨ a iff ⟨x,^{⌜}a^{⌝}⟩ ⊨ In.

11.5. Proposition. Let a and U be opens of X and 𝕊^{X} respectively. Then a×U ≤ In iff ^{⌜}a^{⌝} is a lower bound of U.

Proof. ⇒: Let ^{⌜}b^{⌝} be a point of U ↪ 𝕊^{X}. If x is a point of a, then ⟨x,^{⌜}b^{⌝}⟩ ⊨ a×U ≤ In and so x ⊨ b. We deduce that a ≤ b, and so ^{⌜}a^{⌝} ⊑ ^{⌜}b^{⌝}.

⇐: Let ⟨x,^{⌜}b^{⌝}⟩ be a point of a × U. Since ^{⌜}b^{⌝} ⊨ U we have ^{⌜}a^{⌝} ⊑ ^{⌜}b^{⌝}, and so a ≤ b. Since x ⊨ a we deduce x ⊨ b, and so ⟨x,^{⌜}b^{⌝}⟩ ⊨ In. Hence a × U ≤ In.

It is perhaps worth pausing here to examine more closely how this very spatial argument can have any hope of yielding a valid result for locales.

First, note that the proposition is intended to be true at any stage Y – we shall certainly need this in the subsequent development. Viewed globally, the proposition then concerns opens a and U of Y × X and Y × 𝕊^{X}, and the left hand condition says that, as opens of Y × X × 𝕊^{X}, we have a ×_{Y} U ≤ Y × In. The right hand condition is a little more subtle, and we shall discuss it shortly.

Next, it suffices to prove the proposition globally, with Y = 1 – just as it appears to be stated –, as long as we reason intuitionistically. This uses the geometricity of 𝕊^{X} and its gadgetry (Proposition 10.3), which implies that

(Y × 𝕊^{X}) ×_{Y} (Y × X) ≅ Y × 𝕊^{X} × X ⟶^{Y ×ev} Y × 𝕊

makes Y × 𝕊^{X} the exponential (Y × 𝕊)^{(Y ×X)} over Y. It follows that the ambient assumptions about existence of 𝕊^{X} also hold over Y, so what we prove globally about X and 𝕊^{X} also holds (as long as we reason intuitionistically) about Y × X and Y × 𝕊^{X} over Y.

Next we consider what it means to say that ^{⌜}a^{⌝} is a lower bound of U. Since U is an open sublocale of 𝕊^{X}, any point of U is also a point of 𝕊^{X} and we ask for all these to be greater than ^{⌜}a^{⌝}. The catch, however, is that a point of U may be at some non-global stage, and then corresponds to a point of 𝕊^{X} at that stage. This must be compared not directly with ^{⌜}a^{⌝}, but with a pullback of it.

Working over U, we have a point of 𝕊^{X} (given by the inclusion U ↪ 𝕊^{X}) and hence an open b of X. It is the generic open of X in U, and for any point u of U the corresponding open of X is u^{∗}(b). We can therefore say that ^{⌜}a^{⌝} is a lower bound of U iff a ≤ b over U. Reviewing this globally we see that a and b correspond to two opens of X × U and hence of X × 𝕊^{X}. a corresponds to a × U, and b to In: hence we obtain the result.

We now move on to showing that each point of 𝕊^{X} is a directed join of global points below it (in fact, way below it). However, first we prove a lemma.

11.6. Lemma. Let b and c be opens of X and 1 (so c is a point of 𝕊, or a proposition). b × c is an open of X × 1 ≅ X and so gives a point ^{⌜}b × c^{⌝} of 𝕊^{X}. Then

⌜b × c^{⌝} = ⨆^{↑}({^{⌜}∅^{⌝}} ∪ {^{⌜}b^{⌝}|c})

Proof. Consider exponential transposes. If x is a point of X, then

⟨x, ⨆^{↑}({^{⌜}∅^{⌝}} ∪ {^{⌜}b^{⌝} c})⟩ = ⨆^{↑}({⟨x,^{⌜}∅^{⌝}⟩} ∪ {⟨x,^{⌜}b^{⌝}⟩|c})

and so

⟨x, ⨆^{↑}({^{⌜}∅^{⌝}} ∪ {^{⌜}b^{⌝} c})⟩ ⊨ In ⇔ x ⊨ ∅ or (c and x ⊨ b)
⇔ ⟨x,^{⌜}b × c^{⌝}⟩ ⊨ In

Our main tool is the following. It says in effect that the generic open of X (the generic point of 𝕊^{X}) is a directed join of global points that are in fact way below it. Clearly this is a generalization of the known fact that ΩX is a continuous lattice, so that every global open of X is a directed join of globals way below it.

11.7. Theorem. If a is an open of X then

a = ⋁^{↑}{b ∃V. (⟨b, V ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ V)}

Proof. Note that the join is directed. Suppose ⟨b_{i}, V_{i}⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ V_{i} holds for i in some finite indexing set. Let V = ⋀_{i} V_{i}. Then ^{⌜}a^{⌝} ⊨ V holds. Also ⟨b_{i}, V ⟩ ∈ In_{0}, so if b = ⋁_{i} b_{i} then ⟨b, V ⟩ ∈ In_{0} and b is an upper bound for the b_{i}’s in the set.

Now for any point x of X, we have

x ⊨ a ⇔ ⟨x,^{⌜}a^{⌝}⟩ ⊨ In = ⋁{b × V ⟨b, V ⟩ ∈ In_{0}}
⇔ ∃⟨b, V ⟩ ∈ In_{0} . (x ⊨ b and ^{⌜}a^{⌝} ⊨ V)
⇔ x ⊨ ⋁^{↑}{b ∃V. (⟨b, V ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ V)}

Again, geometricity plays an important role. The result is to hold at any stage Y, but geometricity of exponentiation (Proposition 10.3) allows us to assume without loss of generality that Y = 1. After that we use Proposition 2.2.

11.8. Corollary. If ^{⌜}a^{⌝} is a point of 𝕊^{X} then

⌜a^{⌝} = ⨆^{↑}{^{⌜}b^{⌝}|∃V. (⟨b, V ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ V)}

We now turn to the role of ℙX.

11.9. Lemma.

1. If e is a point of ℙX then there is an open U(e) of 𝕊^{X} defined by

⌜a^{⌝} ⊨ U(e) iff e ⊨ ⊠a.

2. If U is an open of 𝕊^{X} then there is a point ^{⌜}U^{⌝} of ℙX defined by

⌜U^{⌝} ⊨ ⊠b iff ^{⌜}b^{⌝} ⊨ U

for b ∈ G_{X}. In fact this holds for every open b of X.

3. (1) and (2) define a geometric bijection between points of ℙX and opens of 𝕊^{X}.

Proof. (1): Obvious – but relies heavily on the geometricity of the constructions of a from ^{⌜}a^{⌝} and of ⊠a from a.

(2): We must show that this definition of ^{⌜}U^{⌝} respects the relations used in presenting ℙX (Theorem 9.3). Each relation is of the form b ≤ ⋁_{i}^{↑} c_{i}, where the join is globally directed. We know, then, that ^{⌜}b^{⌝} ⊑ ⨆_{i}^{↑}(^{⌜}c_{i}^{⌝}), so it follows that if ^{⌜}b^{⌝} ⊨ U then ^{⌜}c_{i}^{⌝} ⊨ U for some i.

The general result holds because, by Theorem 11.7, every open of X is a directed join of generating global opens from G_{X}.

(3): Suppose U is an open of 𝕊^{X}. If ^{⌜}a^{⌝} is any point of 𝕊^{X} then we have

⌜a^{⌝} ⊨ U(^{⌜}U^{⌝}) ⇔ ^{⌜}U^{⌝} ⊨ ⊠a ⇔ ^{⌜}a^{⌝} ⊨ U

and so U(^{⌜}U^{⌝}) = U.

Now suppose e is a point of ℙX. For any b ∈ G_{X} we then have

⌜U(e)^{⌝} ⊨ ⊠b ⇔ ^{⌜}b^{⌝} ⊨ U(e) ⇔ e ⊨ ⊠b

and so ^{⌜}U(e)^{⌝} = e.

Applying Proposition 10.2, we have now proved Theorem 11.1. Moreover, the construction in Proposition 10.2 gives us –

11.10. Proposition. The evaluation map ev : ℙX × 𝕊^{X} → 𝕊 is got by working over 𝕊^{X}. There In : X × 𝕊^{X} → 𝕊 corresponds to an open of X. This gives an open ⊠ In of ℙX, and ev is the corresponding global open of ℙX × 𝕊^{X}.

Note how geometricity resolves an apparent ambiguity here: is this ℙ calculated over 𝕊^{X}, or is it the global ℙX pulled back to a locale ℙX × 𝕊^{X} over 𝕊^{X}? However, the geometricity of ℙ (Theorem 9.1) gives us a canonical homeomorphism.

11.11. Proposition. As an open of ℙX × 𝕊^{X},

ev = ⋁{⊠b × V ⟨b, V ⟩ ∈ In_{0}}

Proof. We use Theorem 11.8. Working over 𝕊^{X} we have that In is an open of X, and the corresponding point ^{⌜} In^{⌝} of 𝕊^{X} is the generic point. Hence

In = ⋁^{↑}{b ∃V. (⟨b, V ⟩ ∈ In_{0} and V)}

and

ev = ⊠ In = ⋁^{↑}{⊠b ∃V. (⟨b, V ⟩ ∈ In_{0} and V)}

because ⊠ preserves internal directed joins. By geometricity of ℙ and its gadgetry we see that the open ⊠b of ℙX over 𝕊^{X} corresponds to the open ⊠b × 𝕊^{X} of ℙX × 𝕊^{X} globally, so externally we get

ev = ⋁{(⊠b × 𝕊^{X}) ∧ (X × V)|⟨b, V ⟩ ∈ In_{0}}

which gives us the result.

12. 𝕊^{X} as ℙ-algebra

We continue our examination of a locale X for which 𝕊^{X} exists. We shall see that 𝕊^{X} inherits a ℙ-algebra structure from 𝕊, calculated elementwise. Moreover, the ℙ-algebra homomorphisms from 𝕊^{X} to 𝕊 are equivalent to points of X. Since the global points of 𝕊^{X} and of 𝕊 are the elements of ΩX and of Ω, this supports the contention that a ℙ-algebra is a kind of localic frame and that the ℙ-algebra structure on 𝕊^{X} (where the exponential exists) is the localic analogue of the frame structure on ΩX.

In this section we consider In not so much as an open of X over 𝕊^{X}, but as an open of 𝕊^{X} over X.

12.1. Proposition. Let x be a point of X. Under the homeomorphism ℙX ≅ 𝕊^{𝕊^{X}}, the point ↕ x of ℙX corresponds to an open In_{x} = U(↕ x) of 𝕊^{X} defined by

⌜a^{⌝} ⊨ In_{x} iff ⟨x,^{⌜} a^{⌝}⟩ ⊨ In (i.e. x ⊨ a)

Proof. By Lemma 11.9,

⌜a^{⌝} ⊨ U(↕ x) ⇔ ↕ x ⊨ ⊠a ⇔ x ⊨ a.

The construction x ↦ In_{x} is analogous to the embedding of a vector space in its double dual.

12.2. Definition. The map α : ℙ(𝕊^{X}) → 𝕊^{X} is defined by

⟨x, α(e)⟩ ⊨ In iff e ⊨ ⊠ In_{x}

12.3. Lemma. α^{∗} In_{x} = ⊠ In_{x}.

Proof.

e ⊨ α^{∗} In_{x} ⇔ α(e) ⊨ In_{x} ⇔ ⟨x, α(e)⟩ ⊨ In ⇔ e ⊨ ⊠ In_{x}

12.4. Theorem. α : ℙ(𝕊^{X}) → 𝕊^{X} makes 𝕊^{X} a ℙ-algebra.

Proof. To show ↕; α = Id_{𝕊^{X}} we show

⟨x, α∘ ↕ (^{⌜}a^{⌝})⟩ ⊨ In ⇔ ↕ (^{⌜}a^{⌝}) ⊨ ⊠ In_{x} ⇔ ^{⌜}a^{⌝} ⊨ In_{x} ⇔ ⟨x,^{⌜}a^{⌝}⟩ ⊨ In

so α∘ ↕ (^{⌜}a^{⌝}) = ^{⌜}a^{⌝}.

Similarly, for ℙα; α = H; α.

⟨x, α ∘ ℙα(ζ)⟩ ⊨ In ⇔ ℙα(ζ)) ⊨ ⊠ In_{x}
⇔ ζ ⊨ ⊠ ⊠ In_{x} (using Lemma 12.3)
⇔ H(ζ) ⊨ ⊠ In_{x} ⇔ ⟨x, α ∘ H(ζ)⟩ ⊨ In

12.5. Proposition. If x is a point of X, then the map In_{x} : 𝕊^{X} → 𝕊 is a ℙ-algebra homomorphism.

Proof. By definition of α, the composite α; In_{x} corresponds to the open ⊠ In_{x} of ℙ(𝕊^{X}), and this is just ℙ In_{x}; ⊠{⊤}. Since ⊠{⊤} is the ℙ-algebra structure map for 𝕊, this is enough to show the result.

12.6. Theorem. The transformation x ⟼ In_{x} gives a bijection between points x of X and ℙ-algebra homomorphisms from 𝕊^{X} to 𝕊.

Proof. By Theorem 11.1 we have a bijection between points ^{⌜}U^{⌝} of ℙX and opens U of 𝕊^{X}, and from Proposition 12.1 we see that if ^{⌜}U^{⌝} can be expressed as ↕ (x) (x then is unique, since ↕ is an inclusion) then U = In_{x}. Therefore, it suffices to show that ^{⌜}U^{⌝} is in the image of ↕ iff U : 𝕊^{X} → 𝕊 is a ℙ-algebra homomorphism and the ⇒ direction has already been done.

Suppose, then, that U is an open of 𝕊^{X} such that U : 𝕊^{X} → 𝕊 is a ℙ-algebra homomorphism. The point ^{⌜}U^{⌝} of ℙX is defined by

⌜U^{⌝} ⊨ ⊠b iff ^{⌜}b^{⌝} ⊨ U

for b ∈ G_{X}. We show that ^{⌜}U^{⌝} is in the image of ↕. If ^{⌜}U^{⌝} =↕ (x) then x must be defined by

x ⊨ b iff ^{⌜}b^{⌝} ⊨ U

and so what we are required to show is that this respects the lattice structure of G_{X}. This is clear, because from the presentation of X we know that the map G_{X} → 𝕊^{X}, b ↦ ^{⌜}b^{⌝}, is a (localic) lattice homomorphism, and so also is U : 𝕊^{X} → 𝕊 because it is a ℙ-homomorphism.

12.7. Theorem. Let X be a locale for which 𝕊^{X} exists, and let W be a locale such that ℙW is homeomorphic to 𝕊^{X}. Then 𝕊^{W} exists and is homeomorphic to X.

Proof. Opens of W, maps W → 𝕊, are equivalent to ℙ-algebra homomorphisms ℙW → 𝕊. The exponential 𝕊^{X} is also a ℙ-algebra, and so, by Corollary 4.6, its homeomorphism with ℙW is a ℙ-algebra isomorphism. Thus the ℙ-algebra homomorphisms ℙW → 𝕊 are in bijection with the ℙ-algebra homomorphisms 𝕊^{X} → 𝕊, and by Theorem 12.6 these are in bijection with the points of X. Hence X serves as an exponential 𝕊^{W}.

13. Characterizing exponentiability

We have mostly been studying the consequences of the existence of 𝕊^{X}, and where (in Theorem 12.7) we gave a sufficient condition, it relied on the existence already established of another exponential. In order to get off the ground we must find some locales X for which 𝕊^{X} is known to exist. It suffices to use the continuous dcpos.

We shall give a somewhat indirect proof of what is, after all, a well-known result: that continuous dcpos are exponentiable as locales. When continuous dcpos are understood particularly as ideal completions of continuous information systems, it can be deduced from the following Theorem, which is intuitionistically valid.

13.1. Theorem. Let P be a continuous information system. Then Ω Idl(P) is isomorphic to the lattice of rounded upper subsets of P.

Proof. [Vickers 93] Note that the result is not geometric, as it is not even stated geometrically.

However, to avoid the explicit use of frames we shall give a geometric proof. We first prove a special case.

13.2. Definition. [Smyth 77] An R-structure is a continuous information system P in which, for every s ∈ P, ↓ s = {t ∈ P t < s} is an ideal.

13.3. Lemma. Let P be an R-structure, let X = Idl P and let Y = Idl(FP, (<_{U})^{op}). Then Y serves as the exponential 𝕊^{X}.

Proof. If a is an open of X, then we can define a point J(a) of Y by

J(a) = {S ∈ FP ∀s ∈ S. ↓ s ⊨ a}.

Since

↓ s = ⨆_{s′<s}^{↑} ↓ s′,

we find that if ↓ s ⊨ a then ↓ s′ ⊨ a for some s′ < s. It follows that if S ∈ J(a) then S′ ∈ J(a) for some S′ <_{U} S (J(a) is rounded). If S_{i} ∈ J(a) (1 ≤ i ≤ n) then we can find S′_{i} ∈ J(a) with S′_{i} <_{U} S_{i}. Taking S = ⋃_{i} S′_{i}, we get that S ∈ J(a) and S <_{U} S_{i}. After this it is easy to conclude that J(a) is an ideal.

Now suppose J is a point of Y. We can define an open a(J) of X by

I ⊨ a(J) iff ∃s ∈ I. {s} ∈ J

Starting from J, we have J = J(a(J)). For

S ∈ J(a(J)) ⇔ ∀s ∈ S. {s} ∈ J
⇔ ∃S′ ∈ J. ∀s ∈ S. S′ <_{U} {s}
⇔ ∃S′ ∈ J. S′ <_{U} S ⇔ S ∈ J

Starting from a, we have a = a(J(a)). For if I is a point of X then I = ⨆_{s∈I}^{↑} ↓ s and so

I ⊨ a(J(a)) ⇔ ∃s ∈ I. ↓ s ⊨ a ⇔ I ⊨ a

Since all these constructions are geometric, we can now call on Proposition 10.2.

13.4. Theorem. Let P be a continuous information system, let W = Idl P and let X = Idl(FP, (<_{U})^{op}). Then X serves as the exponential 𝕊^{W}.

Proof. (FP, (<_{U})^{op}) is an R-structure. For suppose S <_{U} T_{i} (1 ≤ i ≤ n). For each i we can find T′_{i} with S <_{U} T′_{i} <_{U} T_{i}, and then S <_{U} ⋃_{i} T′_{i} <_{U} T_{i}. It follows by Lemma 13.3 that 𝕊^{X} exists and is Idl(FFP, ≺), where

U ≺ V iff ∀U ∈ U. ∃V ∈ V. U <_{U} V

By Theorem 3.11 we see that this is P_{L}(P_{U}(Idl X)), i.e. ℙ(Idl X), and it remains to apply Theorem 12.7.

13.5. Theorem. Let X be a locale for which 𝕊^{X} exists, with lattices of generators G_{X} and G_{𝕊^{X}} and so on as in Section 11. We define the relation < on G_{X} by

b < a iff ∃V. (⟨b, V ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ V).

Then < makes G_{X} a continuous information system, and 𝕊^{X} is homeomorphic to Idl(G_{X}).

Proof. First we must show that < is transitive and interpolative. It will be helpful later to generalize b < a slightly, to allow a to be an arbitrary open of X. We therefore define

I_{a} = {b ∈ G_{X} ∃V. (⟨b, V ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ V)

so that, when a and b are both in G_{X}, we have b < a iff b ∈ I_{a}. I_{a} is lower closed with respect to <, for suppose c < b ∈ I_{a}, with ⟨c, W ⟩, ⟨b, V ⟩ ∈ In_{0}, ^{⌜}b^{⌝} ⊨ W and ^{⌜}a^{⌝} ⊨ V. By Proposition 11.5, ^{⌜}c^{⌝} is a lower bound of W and so c ≤ b. Hence ⟨c, V ⟩ ∈ In_{0} and we have c ∈ I_{a}. It follows that < is transitive. Next we show that I_{a} is rounded with respect to <. Suppose c ∈ I_{a}, with ⟨c, W ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ W. By Theorem 11.8 we know that ⌜a^{⌝} = ⨆^{↑}{^{⌜}b^{⌝}|b ∈ I_{a}}, so it follows that we have some b ∈ I_{a} with ^{⌜}b^{⌝} ⊨ W, so c < b. It follows that < is interpolative.

In fact, I_{a} is an ideal with respect to <, as we now show. Suppose c_{i} ∈ I_{a} for i in some finite indexing set, with ⟨c_{i}, W_{i}⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ W_{i}. Then ^{⌜}a^{⌝} ⊨ ⋀_{i} W_{i}, ⟨c_{i}, ⋀_{i} W_{i}⟩ ∈ In_{0} and so ⟨⋁_{i} c_{i}, ⋀_{i} W_{i}⟩ ∈ In_{0}. It follows that ⋁_{i} c_{i} ∈ I_{a}. Now let us find b such that ⋁_{i} c_{i} < b ∈ I_{a}, with ⟨⋁_{i} c_{i}, V ⟩ ∈ In_{0} and ^{⌜}b^{⌝} ⊨ V. We have ⟨c_{i}, V ⟩ ∈ In_{0} and it follows that c_{i} < b.

We have now shown that for each open a we can define an ideal I_{a} such that a is the directed join of the opens in I_{a}. It remains only to show that if I is an ideal and a is the join of its elements, then I = I_{a}. First, if c ∈ I, then we can find b such that c < b ∈ I. We have b ≤ a, and it follows that c ∈ I_{b} ⊆ I_{a}. For the converse, suppose c ∈ I_{a} with ⟨c, W ⟩ ∈ In_{0} and ^{⌜}a^{⌝} ⊨ W. By Scott openness of W, and the fact that a is a directed join of the elements of I, it follows that there is some b ∈ I such that ^{⌜}b^{⌝} ⊨ W. Then c < b, so c ∈ I.

The geometricity of this argument suffices to show that 𝕊^{X} is homeomorphic to Idl(G_{X}).

13.6. Corollary. Let X be a locale for which 𝕊^{X} exists. Then ΩX is a continuous lattice, and Ω𝕊^{X} is the Scott topology on ΩX. Its way below relation ≪ satisfies

b ≪ a iff ∃V ∈ Ω𝕊^{X}. (b × V ≤ In and ^{⌜}a^{⌝} ⊨ V)

We can now characterize those locales X for which 𝕊^{X} exists. Note that the characterization does not require a universal quantification over all locales, but simply the existence of certain structure and properties. In this respect it is like the well known characterization by local compactness, that ΩX is a continuous lattice. However, we use structure and properties that are geometric.

13.7. Theorem. Let W be a locale. Then 𝕊^{W} exists iff there is a continuous information system X such that ℙW is homeomorphic to Idl(FX, (<_{U})^{op}), and in that case 𝕊^{W} is homeomorphic to Idl(X).

Proof. ⇐: Use Theorem 12.7.

⇒: Let X be the information system (G_{W} , <) defined as in Theorem 13.5. Then 𝕊^{W} is homeomorphic to Idl(X) and so

ℙW ≅ 𝕊^{𝕊^{W}} ≅ 𝕊^{Idl(X)} ≅ Idl(FX, (<_{U})^{op})

To round off this section, we give a geometric proof to show how exponentiability of X can be deduced from the existence of 𝕊^{X}.

13.8. Lemma. Any discrete locale is exponentiable.

Proof. Let S be a discrete locale (i.e. a set). Let Y be an arbitrary locale, with presentation (G, R, D), and let Y′ be presented by (G × S, R × S, D × S) with

π(⟨d, s⟩) = ⟨π(d), s⟩
λ(⟨r, s⟩) = {⟨g, s⟩ g ∈ λ(r)}
ρ(⟨d, s⟩) = {⟨g, s⟩ g ∈ ρ(d)}

If f : S → Y then we can define a point f′ of Y′ by

f′ ⊨ ⟨g, s⟩ iff f(s) ⊨ g

and, conversely, for any point f′ of Y′ the same equation defines a map f : S → Y. This defines a geometric bijection between points of Y′ and maps S → Y.

13.9. Theorem. Let X be a locale for which 𝕊^{X} exists. Then X is exponentiable.

Proof. Let Y be a locale, presented by (G, R, D). Since 𝕊^{X} exists, we see by the lemma that (𝕊^{X})^{G} does too, and we then have

(𝕊^{G})^{X} ≅ 𝕊^{X×G} ≅ (𝕊^{X})^{G}

and, similarly,

(𝕊^{R})^{X} ≅ 𝕊^{X×R} ≅ (𝕊^{X})^{R}

Consider two maps ϕ_{λ}, ϕ_{ρ} : 𝕊^{G} → 𝕊^{R} defined as follows. ϕ_{λ} is the exponential transpose of the open ϕ′_{λ} of 𝕊^{G} × R,

⟨^{⌜}a^{⌝}, r⟩ ⊨ ϕ′_{λ} iff ∀g ∈ λ(r). g ⊨ a

ϕ′_{ρ} is the exponential transpose of the open ϕ′_{ρ} of 𝕊^{G} × R,

⟨^{⌜}a^{⌝}, r⟩ ⊨ ϕ′_{ρ} iff ∃d. (π(d) = r and ∀g ∈ ρ(d). g ⊨ a)

¿From these we define two maps ψ_{λ} and ψ_{ρ} from (𝕊^{G})^{X} to (𝕊^{R})^{X}, by ψ_{λ} = ϕ_{λ}^{X} and ψ_{ρ} = ϕ_{ρ}^{X}.

Let E ↪ (𝕊^{G})^{X} be the inserter from ψ_{λ} to ψ_{ρ}, i.e. the greatest sublocale restricted to which we have ψ_{λ} ⊑ ψ_{ρ}. Then E is the exponential Y^{X}. For if f : X → Y then we can define an open f′ of X × G (corresponding to a point of 𝕊^{X×G}) by

⟨x, g⟩ ⊨ f′ iff f(x) ⊨ g

and the relations for Y, holding for each point f(x), tell us that f′ is in E. Conversely, if f′ is an open of X ×G that happens to be in E then the same definition in reverse defines a point f(x) of Y for each x.

This gives a geometric bijection between points of E and maps X → Y.

14. Conclusion

The technical results proved here seem rather specialized. We have taken the upper and lower powerlocales, known principally from computer science, and composed them to give a hitherto unstudied “double powerlocale” ℙ. This is then related to exponentiation by the homeomorphism ℙX ≅ 𝕊^{𝕊^{X}}, provided 𝕊^{X} exists.

ℙ is the functor part of a monad on Loc, and its algebras bear some analogies with frames, but carried by locales instead of sets. Following through this analogy, we find that 𝕊^{X} inherits ℙ-algebra structure from 𝕊 ≅ ℙ∅, and ℙ-algebra homomorphisms from 𝕊^{X} to 𝕊 are equivalent to points of X. We deduce that if 𝕊^{X} ≅ ℙW then X ≅ 𝕊^{W}. An intriguing direction of further study is that of (ℙ-alg)^{op} as a category Coloc of “localic locales” or colocales.

In addition to investigating ℙ we have also taken the opportunity to develop techniques of geometricity – that is, structure and properties preserved by pullback along maps (geometric morphisms). It is these techniques that make possible a much more spatial development of locale theory using points of locales. For these points must be generalized points, i.e. arbitrary maps targeted on the locale. It is the geometricity that allows us to cope continuously with the variation of source. Of particular importance is the geometricity of the powerlocale constructions themselves. The treatment relies on the fact that though frames are not geometric representations of the locales (because frame structure is not preserved by inverse image functors), frame presentations are geometric.

Our primary application of the long section of geometricity results is thus to justify a spatial treatment of locales. However, an additional hope is that they might contribute to the foundations of constructive topology. In particular, we have in mind the formal topologies of [Sambin 87]. He follows Martin-Löf’s school of constructive type theory in rejecting impredicative arguments, and this includes many arguments that are valid in (the categories of sheaves over) toposes. (On the other hand, that school admits more of the axiom choice than is valid in toposes.) This leads to a rather fundamental contrast between formal topology and locale theory as conducted in toposes: although they both treat opens as more fundamental than points, formal topology cannot admit the frames as algebras carried by sets. In effect various kinds of formal topology are various ways of presenting frames (sometimes with extra structure, such as positivity predicates when presenting open locales). Since our geometricity requirements lead us also to reject the frames, and to develop ways of handling locales without the frames, we hope that our methods will also find application in formal topology and help to find common ground between the two approaches to constructive topology.

References

[AbrVic 93] Abramsky, S., and Vickers, S.J. “Quantales, Observational Logic and Process Semantics”. Mathematical Structures in Computer Science 3 (1993), 161-227.

[Beck 69] Beck, J. “Distributive laws”, in Springer Lecture Notes in Mathematics 80 (1969), 119-140.

[FoScott 79] Fourman, M.P., and Scott, D.S. “Sheaves and Logic”, in Applications of Sheaves – Proceedings of Durham Symposium, 1977 (Springer Lecture Notes in Mathematics 753, 1979), 302-410.

[Hyland 81] Hyland, J.M.E. “Function spaces in the category of locales”, in Banaschewski and Hoffmann (eds) Continuous lattices (Springer Lecture Notes in Mathematics 871, 1981), 264-281.

[Johnstone 77] Johnstone, P.T. Topos Theory. Academic Press, London, 1977.

[Johnstone 82] Johnstone, P.T. Stone Spaces, Cambridge Studies in Advanced Mathematics 3. Cambridge University Press, 1982.

[JoVic 91] Johnstone, P.T., and Vickers, S.J. “Preframe presentations present”, in Carboni, Pedicchio and Rosolini (eds) Category Theory – Proceedings, Como, 1990 (Springer Lecture Notes in Mathematics 1488, 1991), 193-212.

[JoyTie 84] Joyal, A. and Tierney, M. An Extension of the Galois Theory of Grothendieck, Memoirs of the American Mathematical Society 309, 1984.

[Kock 95] Kock, A. “Monads for which structures are adjoint to units”, Journal of Pure and Applied Algebra 104 (1995), 41-59.

[MRW] Marmolejo, F., Rosebrugh, R.D., and Wood, R.J. “A basic distributive law”. To appear in Journal of Pure and Applied Algebra.

[Sambin 87] Sambin, G., “Intuitionistic formal spaces – a first communication”, in Skordev (ed) Mathematical logic and its applications, Plenum, 1987, 187-204.

[Smyth 77] Smyth, M. “Effectively given domains”, Theoretical Computer Science 5 (1977), 257-274.

[Taylor 01] Taylor, P. “Sober spaces and continuations”, in preparation. Draft available at http://www.dcs.qmul.ac.uk/˜ pt/ASD/.

[Vickers 89] Vickers, S.J. Topology via Logic, Cambridge University Press, 1989.

[Vickers 93] Vickers, S.J. “Information systems for continuous posets”. Theoretical Computer Science 114 (1993), 201–229.

[Vickers 95] Vickers, S.J. “Locales are not pointless”, in Hankin, Mackie and Nagarajan (eds) Theory and Formal Methods of Computing 1994 (Imperial College Press, 1995) 199-216.

[Vickers 97] Vickers, S.J. “Constructive points of powerlocales”. Math. Proc. Cam. Phil. Soc. 122 (1997), 207-222.

[Vickers 99] Vickers, S.J. “Topical categories of domains”. Mathematical Structures in Computer Science 9 (1999), 569–616.

[Vickers 01] Vickers, S.J. “Strongly Algebraic = SFP (Topically)”. To appear in Mathematical Structures in Computer Science.

School of Computer Science, The University of Birmingham, Birmingham, B15 2TT, UK

Email: s.j.vickers@cs.bham.ac.uk

This article may be accessed via WWW at http://www.tac.mta.ca/tac/ or by anony-

mous ftp at ftp://ftp.tac.mta.ca/pub/tac/html/volumes/12/13/12-13.{dvi,ps}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods.

Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication.

The method of distribution of the journal is via the Internet tools WWW/ftp. The journal is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive (by e-mail) abstracts of articles as they are published. Full text of published articles is available in .dvi, Postscript and PDF. Details will be e-mailed to new subscribers. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh,

rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e is the preferred flavour. TEX source of articles for publication should be submitted by e-mail directly to an appropriate Editor. They are listed below. Please obtain detailed information on submission format and style files from the journal’s WWW server at http://www.tac.mta.ca/tac/. You may also write to tac@mta.ca to receive details by e-mail.

Editorial board.

Michael Barr, McGill University: barr@barrs.org, Associate Managing Editor Lawrence Breen, Université Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of Wales Bangor: r.brown@bangor.ac.uk Jean-Luc Brylinski, Pennsylvania State University: jlb@math.psu.edu Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Palo Alto Research Center: paiva@parc.xerox.com Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk G. Max Kelly, University of Sydney: maxk@maths.usyd.edu.au Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca, Managing Editor Jiri Rosicky, Masaryk University: rosicky@math.muni.cz James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca