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*for every morphism^{X}*h*:*Z*×*X*→*Y*; - satisfying the equations:
- (β) App o (Λ(
*f*) × id) =_{X}*f*for every morphism*f*:*Z*×*X*→*Y*, - (η) Λ(App) = id
_{YX} - (σ) Λ(
*f*) o*g*= Λ(*f*o (*g*× id)) for all morphisms_{X}*f*:*Z*×*X*→*Y*and*g*:*Z′*→*Z*.

- (β) App o (Λ(

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 **O***X* 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 **c**omponentwise”), 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*is in_{i}*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 π
_{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*:*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 π_{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*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 [Ω_{1} →_{frm} Ω_{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 [*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 [Ω_{1} →_{frm} Ω_{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 *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

*to*

*X*×*Y***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*≠⊥ for every index_{i}*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*≠⊥), we deduce that_{i}*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*, some below_{i}**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*is equal to ⊥. If_{i}*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*≤ {1} ⊗_{j}*G*(*v*) we obtain that*a*≤ {1}. It follows that for every*i*in*I*,*a*⊗*b*is not only below_{i}**S**⊗*F*(*v*), but even below {1} ⊗*F*(*v*). Since*F*(*v*) ≤*G*(*v*), it is below {1} ⊗*G*(*v*). The rectangles*a*⊗*b*with_{i}*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**), {1} ⊗*

*w**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**

*must be the space of all continuous maps from*

^{X}*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*implies

_{u}*y*∈

*O*, if and only if every

_{u}*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. (χ

*is the characteristic map of*

_{x}*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*↦ χ

*are inverse of each other, and are monotonic.*

_{x}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 φ

*=φ, if*

_{u}*u*=φ({1}). Explicitly, the composition of φ ↦

*u*≝φ({1}) ↦ φ

*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}*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 φ

*does. The map φ sends top to top because each φ*

_{i}*does (and*

_{i}*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**] (≅ **O***X*) 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*. That φ is in

_{d}*O*means that φ(

_{d}*d*)=

**1**. Since suprema are computed pointwise, φ(

*d*) = sup

_{i ∈ I}φ

*(*

_{i}*d*), so φ

*(*

_{i}*d*)=

**1**for some

*i*in

*I*; and therefore φ

*is in*

_{i}*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*its supremum in Ω, then we see that

_{d}*v*is in Ω

_{d}*: indeed,*

_{d}*d*⊗

*v*is the supremum of all the elements of the form

_{d}*d*⊗

*v*∈ App({1}) (with

*d*fixed), because

*d*⊗ _ commutes with arbitrary suprema; since App({1}) is a C-ideal,

*d*⊗

*v*is also in App({1}), and therefore

_{d}*v*is in Ω

_{d}*, as promised. In other words,*

_{d}*v*is the largest element of Ω

_{d}*, or equivalently the largest element*

_{d}*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*is one side of the corresponding Galois connection.)

_{d}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 ↑φ

*in [*

_{vd}**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*is such that

_{d}*u*

_{φ}≥

*v*. By definition of

_{d}*O*, the fact that φ is in

_{d}*O*means that φ(

_{d}*d*)=

**1**. But

*u*

_{φ}≥

*v*for every

_{d’}*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

*φ*, where

_{vd’}*d’*ranges over φ

^{–1}({

**1**}). For each such

*d’*,

*O*is included in↑φ

_{d’}*by Lemma F, and*

_{vd’}*O*is Scott-open by Proposition C. Hence φ

_{d’}*is way-below φ. (Explicitly, any directed family*

_{vd}*D*whose supremum is above φ will be such that sup D is in

*O*. Since

_{d’}*O*is Scott-open, some element of

_{d’}*D*will be in

*O*, and therefore in ↑φ

_{d’}*since*

_{vd’}*O*⊆ ↑φ

_{d’}*. Namely, that element will be above φ*

_{vd’}*.) We have obtained that every element φ of [*

_{vd’}**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 **O***X* 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!

- 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.
- Jorge Picado and Aleš Pultr. Frames and locales — topology without points. Birkhäuser, 2010.

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