Exponentiable locales I: every exponentiable locale is continuous

It seems like I have an obsession about Cartesian-closed categories and exponentiable objects these days, if you consider that my latest post was on that very topic as well.

The exponentiable objects of Top are exactly the core-compact spaces. If X is exponentiable, then the exponential Y^X is the space of all continuous maps from X to Y for a unique topology, which I call the core-open topology, and also coincides with the so-called Isbell topology (when X is core-compact). This is all explained in Section 5.4 of the book.

Considering that the category Loc of locales is related to Top by Stone duality, and that the Stone duals of core-compact spaces (or, equivalently, of locally compact spaces) are the continuous frames, one might bet that the exponentiable locales are exactly the continuous frames. If you did that bet, you would win it! This was proved by Martin Hyland in 1979 [1], and I will attempt to explain how this is proved. In this post, I will only give one direction of the proof; the other half will have to wait for another time.

Exponentiable objects, and exponentials

Let me explain what exponentiable objects and exponentials are in a category C. I have already done that, but I hate to refer to other pages. Instead, let me unashamedly copy what I wrote last month on the subject.

Given any two objects X and Y in a category with finite products, the exponential Y^X, if it exists, is an object, together with:

• a morphism App : Y^X × X → Y (application, sometimes called evaluation);
• an operation Λ (currification, sometimes called abstraction), such that Λ(h) is a morphism from Z to Y^X for every morphism h : Z × X → Y;
• satisfying the equations:
  • (β) App o (Λ(f) × id_X) = f for every morphism f : Z × X → Y,
  • (η) Λ(App) = id_Y^X
  • (σ) Λ(f) o g = Λ(f o (g × id_X)) for all morphisms f : Z × X → Y and g : Z′ → Z.

This is discussed in Section 5.5.3 of the book. In Set, every object is exponentiable, Y^X is the set of all functions from X to Y, App is the application map (f, x) ↦ f(x), and Λ(f) maps every point z in Z to the function x ↦ f(z, x).

An object X is exponentiable if and only if the exponential Y^X exists for every object Y. Equivalently, X is exponentiable if and only if the functor _ × X has a right adjoint (and that right adjoint is the functor _^X).

Frames and locales

I have already produced a few posts on frames and locales. In brief, a frame is a complete lattice in which binary meets (infima) distribute over arbitrary joins (suprema). Frame morphisms are those maps that preserve finite infima and arbitrary joins. They form a category Frm. It is customary to call Loc the dual category Frm^op, and to call its objects (which are just frames—but the morphism are reversed!) locales.

The point (if I may say so) is that Top and Loc are related by Stone duality: an adjunction O ⊣ pt between topological spaces and locales, which restricts to an equivalence of categories between sober spaces and spatial locales; a locale is spatial if and only if it is of the form OX for some space X (up to frame isomorphism). See Section 8.1 of the book, for example, or the book by Jorge Picado and Aleš Pultr [2] for more information on locales.

As Picado and Pultr do, I prefer to reason with frames, but exponentials in Loc are best explained with locales, so brace yourself: we are going to juggle between the two viewpoints constantly, and you will have to keep in mind in which directions all those arrows are meant to go! But I will try and be as explicit as I can at each instant.

Products in locales are a bit complicated. In the book, I use the frame of Galois connections Gal(L, L’) between two frames L and L’, and that serves as the locale product L ×_loc L’ of L and L’. In this post, I will rather use C-ideals.

A C-ideal on a pair of frames L, L’ is a downwards closed set D of rectangles u ⊗ v (I will defined what they are below) that is closed under C-suprema (for “suprema taken componentwise”), namely such that:

• for every u ∈ L, for every family of elements (v_i)_{i ∈ I} with some supremum v in L’, such that each rectangle u ⊗ v_i is in D, then u ⊗ v is also in D, and
• for every v ∈ L’, for every family of elements (u_i)_{i ∈ I} with some supremum u in L, such that each rectangle u_i ⊗ v is in D, then u ⊗ v is also in D.

A rectangle u ⊗ v is really a Galois connection (see this post, for example; the definition of C-ideal was taken from there), but we do not need to know that. It turns out that ⊥ ⊗ v = u ⊗ ⊥ is the least rectangle (much like the open rectangles ∅ × V and U × ∅ are both empty), but apart from that, u ⊗ v really behaves just like a pair of elements u in L (other than its bottom element ⊥) and v in L’ (other than its own bottom element, still written ⊥). In particular, when u, u’≠⊥ and v, v’≠⊥, we have u ⊗ v ≤ u’ ⊗ v’ if and only if u≤u’ and v≤v’. Hence we really should read u ⊗ v as the pair of the two elements u and v if they are both different from ⊥, and as being equal to ⊥ otherwise (where I continue to use ⊥ as a notation for the bottom element, this time in the collection of rectangles).

Let us notice that, for every u, u ⊗ _ preserves all suprema and finite infima. We will use that observation later. This is proved by looking at the case u=⊥, which is trivial since then u ⊗ _ is a constant function, and by looking at the case u≠⊥, where this follows from the fact that u ⊗ v ≤ u’ ⊗ v’ if and only if u≤u’ and v≤v’.

Also, just to be sure you know: no C-ideal is ever empty. This is because it is closed under C-suprema of empty families. Hence the bottom rectangle ⊥ is in every C-ideal.

The infimum of two C-ideals (or of any family of C-ideals) is just their intersection. Suprema are more complicated, see Exercise 8.4.27 in the book: we have to take unions, and then take the smallest C-ideal containing the union, typically by adding all missing C-suprema, and iterating transfinitely.

I will write L ×_loc L’ for the collection of C-ideals on L and L’, ordered by inclusion. This is (an isomorphic copy) of their product in Loc. We have:

• first projection π₁ : L ×_loc L’ → L (in Loc, so π₁ is a frame homomorphism from L to L ×_loc L’) maps every u in L to ↓(u ⊗ ⊤);
• similarly, second projection π₂ maps every v in L’ to ↓(⊤ ⊗ v);
• the pairing 〈f, g〉 : L” → L × L’ of two locale morphisms f : L” → L and g: L” → L’ in Loc (namely, of two frame homomorphisms f : L → L” and g: L’ → L”) is the frame homomorphism from L ×_loc L’ to L” that sends every C-ideal D to ⋁ {f(u) ⋀ g(v) | u ⊗ v ∈ D};
• as a consequence, given any two locale morphisms f : M → L and g : M’ → L’, their product f ×_loc g, namely 〈f o π₁, g o π₂〉 : M ×_loc M’ → N ×_loc N’ (where composition is taken in Loc, hence works the other way around as in Frm) maps every C-ideal D on N and N’ to the supremum of the C-ideals ↓(f(u) ⊗ ⊤) ∩ ↓(⊤ ⊗ g(v)) = ↓(f(u) ⊗ g(v)), where u ⊗ v ranges over D. This is just the union of those C-ideals, since that union is already closed under C-suprema; in other words, f ×_loc g maps D to ↓{f(u) ⊗ g(v) | u ⊗ v ∈ D}.

For completeness, let me make explicit the terminal object in Loc:

• the terminal object in Loc is O1, where 1 is the terminal object in Top; namely, 1≝{*}, with only two open subsets, ∅ and 1;
• the unique locale morphism !_L : L → O1 in Loc (namely, the unique frame homomorphism from O1 to the frame L) maps the bottom element ∅ of O1 to the bottom element ⊥ of L and the top element 1 of O1 to the top element ⊤ of L.

Finally, let me transpose the notion of exponentials here. Given three frames L, L’ and Ω, if the exponential object L^Ω exists in Loc, then the locale morphisms from L’ to L^Ω are in one-to-one-correspondence with those from L’ ×_loc Ω to L; in one direction, Λ sends every locale morphism from L’ ×_loc Ω to L to one from L’ to L^Ω, and its inverse sends any locale morphism h : L’ → L^Ω to App o (h ×_loc id_Ω) : L’ ×_loc Ω → L. This is with any exponentiable object in any category with finite products, and can be checked by using the equations (β), (η) and (σ).

In other words, and writing [Ω₁ →_frm Ω₂] for the poset of all frame homomorphisms from a frame Ω₁ to a frame Ω₂, ordered by the pointwise ordering, Λ is a bijection from [L →_frm L’ ×_loc Ω] onto [L^Ω →_frm L’]. We have more: Λ must preserve and reflect the ordering; this is a generalization of an argument that forms half of sublemma 2.1 in [1]; to be precise, that sublemma contains an implicit proof of the following proposition in the special case where L=OS and L’=O1. (I will introduce OS not too far away below.)

Proposition A. If the exponential object L^Ω exists in Loc, then for every frame L’, Λ is an order-isomorphism from [L →_frm L’ ×_loc Ω] onto [L^Ω →_frm L’].

Proof. This is somewhat longish if we do it in detail; I was surprised that it had to be so long, by the way. I could sweep some verifications under the rug, but I hate to do so. In order to ease reading, I will cut up the argument in six steps. The first one consists in showing that the inverse App o (_ ×_loc id_Ω) of Λ is monotonic, and is pretty immediate. The remaining five steps will be devoted to showing that Λ itself is monotonic.

Step 1: the inverse of Λ is monotonic. Frm is enriched over the category Pos of posets and monotonic maps. In other words, every hom-set [Ω₁ →_frm Ω₂] is ordered, and composition is monotonic in both morphisms being composed. Looking at the explicit description of products f ×_loc g in Loc given above, we see that the product operation ×_loc on morphisms is also monotonic. Hence the inverse of Λ, which maps h to App o (h ×_loc id_Ω) (with composition taken in Loc), is monotonic.

Step 2: Λ is monotonic, basic ideas. In order to show that Λ is monotonic, we will need to use Sierpiński space S. The space S is the two-element space {0, 1}, ordered by 0<1, and with the Alexandroff or equivalently the Scott topology on it; namely, its open sets are the empty set, {1}, and {0, 1}, but not {0}. The general idea of the argument can be grasped by looking at the analogous case of Top. Imagine we have two continuous maps f and g from a space X × Y to a space Z, with f≤g. In order to show that Λ(f) ≤ Λ(g) without knowing how Λ operates, we would define a continuous map h : S × (X × Y) → Z by h(0,c)≝f(c) and h(1,c)≝g(c) for every c in X × Y; in this way, h o 〈false o !_{X × Y}, id_{X × Y}〉 = f and h o 〈true o !_{X × Y}, id_{X × Y}〉 = g, where true : 1 → S is the constant map with value 1, false : 1 → S is the constant map with value 0, and !_{X × Y} is the unique map from X × Y to 1. Then, using Equation (σ), we realize that Λ(f) = Λ(h o 〈false o !_{X × Y}, id_{X × Y}〉) must be equal to Λ(h) o false o !_{X × Y}, and similarly that Λ(g) = Λ(h) o true o !_{X × Y}. Since false≤true and composition is monotonic, this entails the desired inequality Λ(f) ≤ Λ(g). We adapt this argument to the case of locales right away.

Step 3: true, false, and the analogue of h. The role of the two maps true and false will be played by their localic analogues True≝O(true) and False≝O(false). As morphisms in Loc, they go from O1 to OS, hence they are frame homomorphisms from OS to O1. There are three elements in OS, which are ∅, {1}, and S. Any frame homomorphism from OS to O1 must map ∅ to ∅ and S to 1. Additionally, True maps {1} to 1, and False maps {1} to ∅. Let us notice that, similarly to the fact that false≤true, we have False≤True.

Defining the analogue of h is slightly trickier. Let us look back at how we defined h above. For every open subset V of Y, h^–1(V) is equal to (S × f^–1(V)) ∪ ({1} × g^–1(V)), using the fact that f≤g. Analogously, we assume two locale morphisms F, G : L’ ×_loc Ω → L with F≤G (as elements of [L →_frm L’ ×_loc Ω]), and we define H : OS ×_loc (L’ ×_loc Ω) → L, namely as a frame homomorphism from L to OS ×_loc (L’ ×_loc Ω) by:

For every v in L, H(v) ≝ ↓{S ⊗ F(v), {1} ⊗ G(v)}.

Step 4: H(v) is well-defined for every v. We check that ↓{S ⊗ F(v), {1} ⊗ G(v)} is a C-ideal. Crucially, this requires F(v)≤G(v), a fact that we will use near the end of the argument.

• Let us assume a family of open rectangles a_i ⊗ b, where some of them are below S ⊗ F(v) (say, those such that i ranges over a subset I of the indices), and the others (say, where i ranges over the complement J of I) are below {1} ⊗ G(v). For the purposes of taking suprema, the open rectangles equal to ⊥ play no role, so we may as well assume that a_i≠⊥ for every index i, and that b≠⊥.
  If I is empty, then sup_i (a_i ⊗ b), where i ranges over all indices, is a supremum of rectangles all below {1} ⊗ G(v), hence is below {1} ⊗ G(v) as well. If I is non-empty, then we pick some i in I, and from a_i ⊗ b ≤ S ⊗ F(v) (and the fact that a_i≠⊥), we deduce that b ≤ F(v). Hence we are taking a supremum of rectangles that are all below S ⊗ F(v), whether i is in I or in J — the point is that the rectangles a_i ⊗ b with i in J still have the same second component b, and b ≤ F(v).
• Let us assume a family of open rectangles a ⊗ b_i, some below S ⊗ F(v) (as before, when i is in some set I of indices), some below {1} ⊗ G(v) (where i ranges over a disjoint set J). As above, we assume that neither a nor any b_i is equal to ⊥. If J is empty, then sup_i (a_i ⊗ b) is a supremum of elements all below S ⊗ F(v), hence is itself below S ⊗ F(v). Otherwise, we pick a j in J, and from a ⊗ b_j ≤ {1} ⊗ G(v) we obtain that a ≤ {1}. It follows that for every i in I, a ⊗ b_i is not only below S ⊗ F(v), but even below {1} ⊗ F(v). Since F(v) ≤ G(v), it is below {1} ⊗ G(v). The rectangles a ⊗ b_i with i in J are also below {1} ⊗ G(v), by assumption, so sup_i (a_i ⊗ b) ≤ {1} ⊗ G(v).

Step 5: H is a frame homomorphism. H(v) is simply the supremum of ↓(S ⊗ F(v)) and of ↓({1} ⊗ G(v)); since F and G preserve all suprema, and since S ⊗ _ and {1} ⊗ _ do, too, H preserves all suprema.

H maps ⊤ to ↓{S ⊗ ⊤, {1} ⊗ ⊤} = ↓(S ⊗ ⊤), which is the top element of OS ×_loc (L’ ×_loc Ω).

In order to show that H is a frame homomorphism, it remains to show that H(v ⋀ w) = H(v) ⋀ H(w), for all v, w in L’ ×_loc Ω. Since H preserves suprema, it is monotonic, so H(v ⋀ w) ≤ H(v) ⋀ H(w). We therefore concentrate on the reverse inequality. H(v) ⋀ H(w) is the intersection of ↓{S ⊗ F(v), {1} ⊗ G(v)} and of ↓{S ⊗ F(w), {1} ⊗ G(w)}. We consider any rectangle in that intersection, and we need to show that it is in H(v ⋀ w) = ↓{S ⊗ F(v ⋀ w), {1} ⊗ G(v ⋀ w)}:

• any rectangle below S ⊗ F(v) and S ⊗ F(w) is below their infimum, which is S ⊗ F(v ⋀ w), since F and S ⊗ _ both preserve binary infima;
• any rectangle below {1} ⊗ G(v) and below {1} ⊗ G(w) will similarly be below {1} ⊗ G(v ⋀ w);
• any rectangle a ⊗ b below S ⊗ F(v) and {1} ⊗ G(w) must be such that a≤{1} and b≤F(v); then b≤G(v) since F≤G, so a ⊗ b is below {1} ⊗ G(v); since it is below {1} ⊗ G(w) by assumption, it is also below their infimum, which is {1} ⊗ G(v ⋀ w);
• any rectangle a ⊗ b below {1} ⊗ G(v) and S ⊗ F(w) must be below {1} ⊗ G(v ⋀ w), by the same argument.

Step 6: replaying the topological argument in Loc. In step 2, I had argued that h o 〈false o !_{X × Y}, id_{X × Y}〉 = f. Similarly, let us show that H o 〈False o !_{L’ ×loc Ω}, id_{L’ ×loc Ω}〉 = F, where composition is in Loc (hence works the other way around as in Frm, as usual). We compute the image of an arbitrary element v of L under the map on the left hand side. We first apply H (composition is the other way around in Frm!), and we obtain ↓{S ⊗ F(v), {1} ⊗ G(v)}. Next, we apply a pairing 〈A, B〉 of two frame homomorphisms A ≝ False o !_{L’ ×loc Ω} and B ≝ id_{L’ ×loc Ω}, and this gives us (A(S) ⋀ B(F(v))) ⋁ (A({1}) ⋀ B(G(v))). Since B is the identity map, this simplifies to (A(S) ⋀ F(v)) ⋁ (A({1}) ⋀ G(v)). Since A is a frame homorphism, A(S) = ⊤. Since False ({1}) = ∅, and !_{L’ ×loc Ω} is a frame homomorphism, A({1}) = ⊥. Therefore (A(S) ⋀ F(v)) ⋁ (A({1}) ⋀ G(v)) = (⊤ ⋀ F(v)) ⋁ ⊥ = F(v).

We show that H o 〈True o !_{L’ ×loc Ω}, id_{L’ ×loc Ω}〉 = G in a similar way. Explicitly (but in brief!), v is now first mapped by H to ↓{S ⊗ F(v), {1} ⊗ G(v)}, as above, and we apply a pairing 〈A, B〉 to that where now A ≝ True o !_{L’ ×loc Ω} (and B is id_{L’ ×loc Ω}, unchanged from above). This produces (A(S) ⋀ F(v)) ⋁ (A({1}) ⋀ G(v)), and A(S) = ⊤, as above, but now A({1}) = ⊤; so (A(S) ⋀ F(v)) ⋁ (A({1}) ⋀ G(v)) = F(v)) ⋁ G(v), which is equal to G(v), since F≤G.

We are almost finished. Using Equation (σ), Λ(F) = Λ(H o 〈False o !_{L’ ×loc Ω}, id_{L’ ×loc Ω}〉) is equal to Λ(H) o False o !_{L’ ×loc Ω}, and similarly Λ(G) = Λ(H) o True o !_{L’ ×loc Ω}. Since False≤True and composition is monotonic, it follows that Λ(F) ≤ Λ(G). ☐

pt(OS^Ω) ≅ Ω

In order to show that the exponentiable topological spaces are the core-compact spaces, the usual proof of the exponential ⇒ core-compact direction consists in observing that if X is an exponentiable topological space, then Y^X exists for every space Y, and in particular for Sierpiński space S. Next, S^X must be the space of all continuous maps from X to S, with some topology, and that is exactly the set of characteristic functions of open subsets of X. This is exactly the observation that Hyland makes in the localic context: the role of S is played by its associated locale OS (of open subsets of S, namely ∅, {1}, and {0,1}), and then, for every exponentiable frame Ω, the points of OS^Ω are in one-to-one correspondence with the elements of Ω. This is even an order-isomorphism; we will show this below, as a consequence of Proposition A.

For any frame L, a point of L is a completely prime filter of L, and pt(L) denotes the set of all points of L. It is customary to equip pt(L) with the topology whose open sets are O_u ≝ {x ∈ pt(L) | u ∈ x}, where u ranges over L. For now, we will consider pt(L) as a poset, equipped with the specialization ordering of that topology. It turns out that this specialization ordering is just inclusion: for any two points x and y of L, x is below y in the specialization ordering if and only if for every u ∈ L, x ∈ O_u implies y ∈ O_u, if and only if every u ∈ x is in y, if and only if x ⊆ y.

Proposition B. For every exponentiable frame Ω, there is a string of order-isomorphisms pt(OS^Ω) ≅ [OS^Ω →_frm O1] ≅ [OS →_frm O1 ×_loc Ω] ≅ [OS →_frm Ω] ≅ Ω.

Proof. The first order-isomorphism can be written more generally as pt(L) ≅ [L →_frm O1], for any frame L. Any point x of L determines a frame homomorphism χ_x from L to O1, which maps every u in L to 1 if u is in x, to ∅ otherwise. (χ_x is the characteristic map of x.) That is a frame homomorphism: it preserves finite infima because x is a filter, and it preserves arbitrary suprema because x is completely prime. Conversely, any frame homomorphism φ from L to O1 determines a completely prime filter φ^–1(1): it is a filter because φ preserves finite infima, and it is completely prime because φ preserves arbitrary suprema. It is then easy to see that the operations φ ↦ φ^–1(1) and x ↦ χ_x are inverse of each other, and are monotonic.

The second isomorphism [OS^Ω →_frm O1] ≅ [OS →_frm O1 ×_loc Ω] is an order-isomorphism between the poset of all locale morphisms from O1 to OS^Ω and the poset of all locale morphisms from O1 ×_loc Ω to OS, and it is given by Proposition A.

The third isomorphism comes from the fact that, since O1 is a terminal object in Loc, O1 ×_loc Ω is isomorphic (in Loc) to Ω. Explicity, the isomorphism is second projection from O1 ×_loc Ω to Ω in one direction, and 〈!_Ω, id_Ω〉 in the other direction.

The fourth isomorphism [OS →_frm Ω] ≅ Ω is the following. Given any frame homomorphism φ from OS to Ω, φ({1}) is an element of Ω. Conversely, given any element u of Ω, let φ_u map {1} to u, bottom to bottom and top to top. This is a frame homomorphism, and the only one such that φ_u=φ, if u=φ({1}). Explicitly, the composition of φ ↦ u≝φ({1}) ↦ φ_u is the identity map; conversely, u ↦ φ_u ↦ φ_u({1}) is also the identity map. Also, the map u ↦ φ_u is clearly monotonic, and so is the map φ ↦ u≝φ({1}). ☐

Every exponentiable locale Ω is a continuous dcpo

We can now prove that, if Ω is exponentiable in Loc, or in fact just if OS^Ω exists in Loc, then Ω must be a continuous dcpo. I will follow M. Hyland’s proof [1, Proposition 2, pages 267–280]. The argument matches the proof that every exponential topological space must be core-compact (Proposition 5.3.3 in the book) rather closely, up to some transposition to the case of locales.

We will use the order-isomorphisms given in Proposition B a lot. Since Ω is a frame, hence a dcpo, so is pt(OS^Ω) ≅ [OS^Ω →_frm O1].

We may also check this directly; for now, let us take this as a cross-check. Given any directed family (φ_i)_{i ∈ I} of frame homomorphisms from OS^Ω to O1, its supremum φ is computed pointwise. In order to see this, we let φ be the pointwise supremum of the family, and we check that it is a frame homomorphism. It clearly preserves all suprema, since every φ_i does. The map φ sends top to top because each φ_i does (and I is non-empty). The fact that φ preserves binary infima depends on the fact that we are working in a poset of frame homomorphisms whose codomain is O1. For all u, v in OS^Ω, in order to show that φ(u ⋀ v) = φ(u) ⋀ φ(v), it suffices to show that φ(u) ⋀ φ(v) ≤ φ(u ⋀ v), since the reverse inequality follows from monotonicity; and in order to show that, it suffices to show that if φ(u) ⋀ φ(v)=1, namely if both φ(u) and φ(v) are equal to 1, then φ(u ⋀ v)=1. Since φ(u)=1, φ_i(u)=1 for some i in I (otherwise, φ_i(u) would be equal to the bottom element ∅ for every i, hence so would be the supremum φ(u)). Similarly, φ_i(v)=1 for some i in I, and we can take the same i for both u and v, by directedness. Then φ_i(u ⋀ v) = φ_i(u) ⋀ φ_i(v) = 1, so φ(u) ⋀ φ(v) = 1.

The point of doing this check is the following (the same would hold for [L →_frm O1], for any frame L).

Lemma. Directed suprema in [OS^Ω →_frm O1] are computed pointwise.

Given any element d of OS^Ω, we form the set O_d ≝ {φ ∈ [OS^Ω →_frm O1] | φ(d)=1}. Such sets are exactly the open subsets of pt(OS^Ω), taken in the isomorphic copy [OS^Ω →_frm O1].

The following is the analogue of the fact that, if X is an exponentiable topological space, then the Scott topology in [X → S] (≅ OX) is finer than the exponential topology on [X → S], which is one of the steps in the proof of Proposition 5.3.3 in the book (fourth paragraph, to be precise).

Proposition C. For every exponentiable frame Ω, for every element d of OS^Ω, O_d is a Scott-open subset of [OS^Ω →_frm O1].

Proof. We first check that O_d is upwards closed: if φ≤φ’, and if φ(d)=1 then certainly φ'(d)=1. Next, let us consider a directed family (φ_i)_{i ∈ I} in [OS^Ω →_frm O1], with (pointwise) supremum φ in O_d. That φ is in O_d means that φ(d)=1. Since suprema are computed pointwise, φ(d) = sup_{i ∈ I} φ_i(d), so φ_i(d)=1 for some i in I; and therefore φ_i is in O_d. ☐

In order to go any further, we need to use the isomorphism between [OS^Ω →_frm O1] and Ω. This isomorphism makes use of the App locale morphism, and we will exploit the properties of App to say a few important, new things. This matches the study of App in the case of topological spaces that is part of the final two paragraphs of the proof of Proposition 5.3.3 in the book; there, we used the specific form of App : [X → S] × X → S, or equivalently of the set (∋) of all pairs (U, x) of an open subset U of X and of a point x of X such that x ∈ U, as a union of open rectangles. In our case, we will use the fact that App({1}) (the application of App : OS^Ω ×_loc Ω → OS, namely of the frame homomorphism App from OS to OS^Ω ×_loc Ω, to the element {1} of OS) is a C-ideal.

Let us name the isomorphism between [OS^Ω →_frm O1] and Ω, first. In one direction, it maps every element φ of [OS^Ω →_frm O1] to some element of Ω, which I will write as u_φ. In the other direction, it maps every element u of Ω to some frame homomorphism from OS^Ω to O1, which I will write as φ_u.

We make the map φ ↦ u_φ explicit, looking at the constructions we used in Proposition B. That is formed by looking at the composition App o (φ ×_loc id_Ω) o 〈!_Ω, id_Ω〉 : Ω → OS (in Loc—that is a frame homomorphism the other way around, from OS to Ω), and applying it (as a frame homomorphism) to {1}. We can simplify (φ ×_loc id_Ω) o 〈!_Ω, id_Ω〉 as 〈φ o !_Ω, id_Ω〉, and therefore u_φ = (App o 〈φ o !_Ω, id_Ω〉) ({1}). The application to {1} is ordinary function application, but the composition inside the parenthesis is in Loc, which runs in the other direction. (I am sorry if I am being heavy about this, but I really feel that it would be ever so confusing without those periodic checks!) Hence u_φ is obtained by first computing App({1}), and then applying 〈φ o !_Ω, id_Ω〉 to it. Explicitly, we obtain the following explicit formula.

Fact D. For every φ in [OS^Ω →_frm O1], u_φ = ⋁{v ∈ Ω | ∃d’ ∈ OS^Ω, φ(d’)=1 and d’ ⊗ v ∈ App({1})}.

Indeed, computing the application of 〈φ o !_Ω, id_Ω〉 to App({1}), we obtain ⋁{!_Ω(φ(d’)) ⋀ v | d’ ⊗ v ∈ App({1})}. When φ(d’)=1, !_Ω(φ(d’))=⊤, so !_Ω(φ(d’)) ⋀ v = v, while if φ(d’)=∅, we have !_Ω(φ(d’))=⊥, so !_Ω(φ(d’)) ⋀ v = ⊥, which does not play any rôle in the computation of the supremum.

Now App({1}) is a C-ideal, in OS^Ω ×_loc Ω. For every d ∈ OS^Ω, there is collection Ω_d ≝ {v ∈ Ω | d ⊗ v ∈ App({1})}, and if we call v_d its supremum in Ω, then we see that v_d is in Ω_d: indeed, d ⊗ v_d is the supremum of all the elements of the form d ⊗ v ∈ App({1}) (with d fixed), because d ⊗ _ commutes with arbitrary suprema; since App({1}) is a C-ideal, d ⊗ v_d is also in App({1}), and therefore v_d is in Ω_d, as promised. In other words, v_d is the largest element of Ω_d, or equivalently the largest element v such that d ⊗ v ∈ App({1}). (We are really retrieving the equivalence of C-ideals with Galois connections: the map that sends each d to v_d is one side of the corresponding Galois connection.)

This allows us to rewrite Fact D as the following.

Fact E. For every φ in [OS^Ω →_frm O1], u_φ = ⋁{v_d’ | d’ ∈ OS^Ω such that φ(d’)=1}.

Lemma F. For every d ∈ OS^Ω, the open set O_d is included in the upward closure ↑φ_vd in [OS^Ω →_frm O1].

Proof. Using the fact that φ ↦ u_φ and u ↦ φ_u are mutually inverse order-isomorphisms (Proposition D), it suffices to show that every element φ of O_d is such that u_φ≥v_d. By definition of O_d, the fact that φ is in O_d means that φ(d)=1. But u_φ≥v_d’ for every d’ ∈ OS^Ω such that φ(d’)=1, by Fact E. ☐

Lemma G. For every φ in [OS^Ω →_frm O1], the family of elements v_d’, when d’ ranges over the elements of OS^Ω such that φ(d’)=1, is directed.

Proof. The map d’ ↦ v_d’ is antitonic (just like for any Galois connection!). Hence it suffices to show that the family F ≝ {d’ ∈ OS^Ω | φ(d’)=1} is filtered. It is certainly so, since φ(⊤)=1 (so ⊤ is in F) and given any two elements d’, d” in F, φ(d’ ⋀ d”)=φ(d’) ⋀ φ(d”)=1, since φ is a frame homomorphism. In fact, F=φ^–1({1}), and we even know that this is a completely prime filter. ☐

We can now conclude.

Theorem. Every frame such that OS^Ω exists in Loc is continuous. In particular, every exponentiable frame Ω is a continuous frame.

Proof. By Proposition D, Ω is order-isomorphic to [OS^Ω →_frm O1], so it suffices to show that [OS^Ω →_frm O1] is a continuous dcpo. For every φ in [OS^Ω →_frm O1], u_φ is the supremum of the directed family of elements v_d’, where d’ ranges over the set φ^–1({1}) of elements of OS^Ω such that φ(d’)=1, by Fact E and Lemma G. Using the order-isomorphism φ ↦ u_φ and its inverse, φ is itself the supremum of the directed family of elements φ_vd’, where d’ ranges over φ^–1({1}). For each such d’, O_d’ is included in↑φ_vd’ by Lemma F, and O_d’ is Scott-open by Proposition C. Hence φ_vd is way-below φ. (Explicitly, any directed family D whose supremum is above φ will be such that sup D is in O_d’. Since O_d’ is Scott-open, some element of D will be in O_d’, and therefore in ↑φ_vd’ since O_d’ ⊆ ↑φ_vd’. Namely, that element will be above φ_vd’.) We have obtained that every element φ of [OS^Ω →_frm O1] ≅ Ω is the supremum of a directed family of elements way-below φ, and that is enough for our purpose, by Trick 5.1.20 in the book, for example. ☐

Conclusion

So there we have it: any exponentiable locale must be a continuous frame. We will show the converse next time (or another time, if I have something more interesting to say in the meantime).

Let me notice that this implies that any exponentiable locale is spatial: every continuous distributive complete lattice is a spatial frame (Proposition 8.3.19 in the book, for example). This is the basis of Hofmann-Lawson duality, which says more; in particular, that a continuous distributive lattice Ω must be isomorphic to OX for some locally compact space X (which happens to be ptΩ).

In order to show that every continuous frame is exponentiable (hence, another time), I am tempted to use that and see whether we obtain a construction that would be somehow easier to grasp than Hyland’s construction. His construction is purely localic, but maybe sacrificing purity by making some hidden uses of the Axiom of Choice (… which are behind the spatiality of continuous frames, in the form of Zorn’s Lemma) will result in a more readable object. If I do it this way, I hope that the purists will forgive me. We’ll see!

1. John Martin Elliott Hyland. Function spaces in the category of locales. In B. Banaschewski, R.-E.Hoffmann (eds.), Proceedings of the Conference on Topological and Categorical Aspects of Continuous Lattices (Workshop IV) held at the University of Bremen, Germany, November 9-11, 1979. Springer Verlag Lecture Notes in Mathematics 871, pages 264–281, 1981.
2. Jorge Picado and Aleš Pultr. Frames and locales — topology without points. Birkhäuser, 2010.

— Jean Goubault-Larrecq (May 21st, 2023)