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 YX 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 YX, if it exists, is an object, together with:

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

This is discussed in Section 5.5.3 of the book. In Set, every object is exponentiable, YX 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 xf(z, x).

An object X is exponentiable if and only if the exponential YX 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 Frmop, 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 Opt 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 uv (I will defined what they are below) that is closed under C-suprema (for “suprema taken componentwise”), namely such that:

  • for every uL, for every family of elements (vi)iI with some supremum v in L’, such that each rectangle uvi is in D, then uv is also in D, and
  • for every vL’, for every family of elements (ui)iI with some supremum u in L, such that each rectangle uiv is in D, then uv is also in D.

A rectangle uv 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, uv 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 uvu’v’ if and only if uu’ and vv’. Hence we really should read uv 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 uvu’v’ if and only if uu’ and vv’.

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 π1 : L ×loc L’L (in Loc, so π1 is a frame homomorphism from L to L ×loc L’) maps every u in L to ↓(u ⊗ ⊤);
  • similarly, second projection π2 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 : LL” 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) | uvD};
  • as a consequence, given any two locale morphisms f : ML and g : M’L’, their product f ×loc g, namely 〈f o π1, g o π2〉 : 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 uv 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) | uvD}.

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 : LO1 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 [Ω1frm Ω2] for the poset of all frame homomorphisms from a frame Ω1 to a frame Ω2, ordered by the pointwise ordering, Λ is a bijection from [Lfrm 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 [Lfrm 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 [Ω1frm Ω2] 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 fg. 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, idX × Y〉 = f and h o 〈true o !X × Y, idX × Y〉 = g, where true : 1S is the constant map with value 1, false : 1S 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, idX × 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 fg. Analogously, we assume two locale morphisms F, G : L’ ×loc Ω → L with FG (as elements of [Lfrm 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) ≝ ↓{SF(v), {1} ⊗ G(v)}.

Step 4: H(v) is well-defined for every v. We check that ↓{SF(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 aib, where some of them are below SF(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 ai≠⊥ for every index i, and that b≠⊥.
    If I is empty, then supi (aib), 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 aibSF(v) (and the fact that ai≠⊥), we deduce that bF(v). Hence we are taking a supremum of rectangles that are all below SF(v), whether i is in I or in J — the point is that the rectangles aib with i in J still have the same second component b, and bF(v).
  • Let us assume a family of open rectangles abi, some below SF(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 bi is equal to ⊥. If J is empty, then supi (aib) is a supremum of elements all below SF(v), hence is itself below SF(v). Otherwise, we pick a j in J, and from abj ≤ {1} ⊗ G(v) we obtain that a ≤ {1}. It follows that for every i in I, abi is not only below SF(v), but even below {1} ⊗ F(v). Since F(v) ≤ G(v), it is below {1} ⊗ G(v). The rectangles abi with i in J are also below {1} ⊗ G(v), by assumption, so supi (aib) ≤ {1} ⊗ G(v).

Step 5: H is a frame homomorphism. H(v) is simply the supremum of ↓(SF(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(vw) = H(v) ⋀ H(w), for all v, w in L’ ×loc Ω. Since H preserves suprema, it is monotonic, so H(vw) ≤ H(v) ⋀ H(w). We therefore concentrate on the reverse inequality. H(v) ⋀ H(w) is the intersection of ↓{SF(v), {1} ⊗ G(v)} and of ↓{SF(w), {1} ⊗ G(w)}. We consider any rectangle in that intersection, and we need to show that it is in H(vw) = ↓{SF(vw), {1} ⊗ G(vw)}:

  • any rectangle below SF(v) and SF(w) is below their infimum, which is SF(vw), 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(vw);
  • any rectangle ab below SF(v) and {1} ⊗ G(w) must be such that a≤{1} and bF(v); then bG(v) since FG, so ab is below {1} ⊗ G(v); since it is below {1} ⊗ G(w) by assumption, it is also below their infimum, which is {1} ⊗ G(vw);
  • any rectangle ab below {1} ⊗ G(v) and SF(w) must be below {1} ⊗ G(vw), 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, idX × Y〉 = f. Similarly, let us show that H o 〈False o !L’ ×loc Ω, idL’ ×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 ↓{SF(v), {1} ⊗ G(v)}. Next, we apply a pairing 〈A, B〉 of two frame homomorphisms A ≝ False o !L’ ×loc Ω and B ≝ idL’ ×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 Ω, idL’ ×loc Ω〉 = G in a similar way. Explicitly (but in brief!), v is now first mapped by H to ↓{SF(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 idL’ ×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 FG.

We are almost finished. Using Equation (σ), Λ(F) = Λ(H o 〈False o !L’ ×loc Ω, idL’ ×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 YX exists for every space Y, and in particular for Sierpiński space S. Next, SX 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 Ou ≝ {xpt(L) | ux}, 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 uL, xOu implies yOu, if and only if every ux is in y, if and only if xy.

Proposition B. For every exponentiable frame Ω, there is a string of order-isomorphisms pt(OSΩ) ≅ [OSΩfrm O1] ≅ [OSfrm O1 ×loc Ω] ≅ [OSfrm Ω] ≅ Ω.

Proof. The first order-isomorphism can be written more generally as pt(L) ≅ [Lfrm 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] ≅ [OSfrm 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 [OSfrm Ω] ≅ Ω 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)iI 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 φ(uv) = φ(u) ⋀ φ(v), it suffices to show that φ(u) ⋀ φ(v) ≤ φ(uv), 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 φ(uv)=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(uv) = φi(u) ⋀ φi(v) = 1, so φ(u) ⋀ φ(v) = 1.

The point of doing this check is the following (the same would hold for [Lfrm 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 Od ≝ {φ ∈ [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 [XS] (≅ OX) is finer than the exponential topology on [XS], 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Ω, Od is a Scott-open subset of [OSΩfrm O1].

Proof. We first check that Od is upwards closed: if φ≤φ’, and if φ(d)=1 then certainly φ'(d)=1. Next, let us consider a directed family (φi)iI in [OSΩfrm O1], with (pointwise) supremum φ in Od. That φ is in Od means that φ(d)=1. Since suprema are computed pointwise, φ(d) = supiI φi(d), so φi(d)=1 for some i in I; and therefore φi is in Od. ☐

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 : [XS] × XS, 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 xU, 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 dOSΩ, there is collection Ωd ≝ {v ∈ Ω | dv ∈ App({1})}, and if we call vd its supremum in Ω, then we see that vd is in Ωd: indeed, dvd is the supremum of all the elements of the form dv ∈ App({1}) (with d fixed), because d ⊗ _ commutes with arbitrary suprema; since App({1}) is a C-ideal, dvd is also in App({1}), and therefore vd is in Ωd, as promised. In other words, vd is the largest element of Ωd, or equivalently the largest element v such that dv ∈ App({1}). (We are really retrieving the equivalence of C-ideals with Galois connections: the map that sends each d to vd 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φ = ⋁{vd’ | d’OSΩ such that φ(d’)=1}.

Lemma F. For every dOSΩ, the open set Od 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 Od is such that uφvd. By definition of Od, the fact that φ is in Od means that φ(d)=1. But uφvd’ for every d’OSΩ such that φ(d’)=1, by Fact E. ☐

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

Proof. The map d’vd’ 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 vd’, 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’, Od’ is included in↑φvd’ by Lemma F, and Od’ 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 Od’. Since Od’ is Scott-open, some element of D will be in Od’, and therefore in ↑φvd’ since Od’ ⊆ ↑φ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. ☐


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)