Exponentiable locales II: the exponentiable locales are the continuous frames

In a previous post, we had seen that every exponentiable locale Ω has to be a continuous frame. We will show the converse: every continuous frame Ω is exponentiable in the category Loc of locales, thus entirely characterizing the exponentiable locales. The result is due to Martin Hyland [1]. Since then, there have been several other proofs of it, by Peter T. Johnstone [2,3] and by Christopher F. Townsend [4], at least.

Martin Hyland proves this in a very elementary way. (Warning: I said “elementary”, not “simple”. “Elementary” means with the help of little background knowledge.) Given a continuous frame Ω, he builds a frame out of generators and relations, and then shows that this frame is the desired exponential object in Loc.

One can understand the construction by looking at exponential objects in Top (see Section 5.4 of the book.) This is entirely similar. When X is a core-compact space, namely a space such that OX is a continuous frame, one builds the exponential object YX, for every topological space Y, as the space [X → Y] of all continuous maps from X to Y, with the core-open topology. The core-open topology is generated by subbasic open sets of the form [U ⋐–1 V] (Definition 5.4.1 in the book), where U ranges over the open subsets of X and V ranges over the open subsets of Y; and [U ⋐–1 V] denotes the collection of continuous maps f : X → Y such that U ⋐ f–1(V).

In order to build the exponential locale LΩ, where Ω is substituted for X, and L is now an arbitrary frame, we cannot rely on having a convenient space of functions f, so we declare that LΩ should be generated from generators which I would write as [u ⋐–1 v], where u ranges over Ω and v over L. We cannot define [u ⋐–1 v] as any kind of collection of functions, but we can axiomatize the properties that the sets [U ⋐–1 V] have in the topological case, and quotient the free frame generated by the generators [u ⋐–1 v] by the resulting axioms (or relations, as one usually says).

In this post, I will allow myself a few shortcuts. This has no interest whatsoever, mathematically, especially since those shortcuts will eventually rely on results that require classical logic and the axiom of choice, while M. Hyland’s argument does not: his argument is constructive. (If you object: yes, I have sinned, and I repent.) But I hope that what I will do will be easier to grasp.

The first of these shortcuts is that, if Ω is a continuous frame, then it is spatial. In fact, Ω is isomorphic to OX, for some topological space X (the space pt Ω of points of Ω, as usual with Stone duality), so that I will simply equate Ω with OX. Additionally, X is locally compact sober: this is Hofmann–Lawson duality (Theorem 8.3.21 in the book).

This leads us to the second shortcut. Instead of imitating an axiomatization of the core-open topology, we will imitate an axiomatization of the compact-open topology: when X is locally compact, the compact-open and core-open topologies coincide on [X → Y] for any space Y (Exercise 5.4.8 in the book), so that should be fine. The compact-open topology has subbasic open sets of the form [Q ⊆ V], where Q is compact saturated in X and V is open in Y, where [Q ⊆ V] means the collection of continuous maps f : X → Y such that f[Q] ⊆ V; or equivalently, such that Q ⊆ f–1(V).

Axiomatizing the compact-open topology

Let me list all the axioms we can think of that the subbasic open subsets [Q ⊆ V] defining the compact-open topology on [X → Y] should have, for all spaces X and Y such that X is locally compact and sober.

However, before I do that, let me list a few useful properties that I will need later on. Let us write QX for the set of compact saturated subsets of X; we order it by reverse inclusion ⊇, yielding the (extended) Smyth powerdomain of X, which we have already encountered a few times, and is also mentioned in the book (in Proposition 8.3.25, for example).

Property Wf. (Wf is for `well-filtered’) Every sober space X is well-filtered: given any filtered family (Qi)i ∈ I of compact saturated subsets of X and any open subset U of X, if ∩i ∈ I Qi ⊆ U then Qi ⊆ U for some i in I.

By filtered, I mean directed in QX, namely: the family is non-empty, and for all i and j in I, there is a k in I such that both Qi and Qj contain Qk. Now Property Wf is simply Proposition 8.3.5 in the book.

Property U. (U is for `union’) For every open subset U of a locally compact space X, there is a family (Qi)i ∈ I of compact saturated subsets of X, all included in U, such that U = ∪i ∈ I int(Qi).

Proof. We write U as a union of interiors int(Qx) of compact saturated subsets Qx of U: this is by local compactness, choosing a compact saturated neighborhood Qx of x included in U for each point x of U. The desired family is (Qx)x ∈ U. ☐

Property I. (I is for `interpolation’) Let X be a locally compact space, Q be a compact saturated subset of X, and U1, …, Un be finitely many open subsets of X. If Q ⊆ ∪k=1n Uk then there are compact saturated subsets Q1 ⊆ U1, …, Qn ⊆ Un such that Q ⊆ ∪k=1n int(Qk).

Proof. For each x in Q, let us pick some index kx in {1, …, n} such that x ∈ Ukx. Then by local compactness there is a compact saturated neighborhood Qx of x that is included in Ukx. The open sets int(Qx) cover Q. Since Q is compact, finitely many cover Q already. In other words, there is a finite subset E of Q such that Q ⊆ ∪x ∈ E int(Qx). For each index k ∈ {1, …, n}, we let Qk be the union of those compact sets Qx such that x ∈ E and kx=k. Then ∪x ∈ E, kx=k int(Qx) ⊆ int(Qk), so Q ⊆ ∪k=1n int(Qk). Each Qk is a finite union of compact saturated sets, and is therefore in QX. And finally, each Qk is a union of sets Qx included in Ukx where kx=k, so Qk ⊆ Uk. ☐

We will use Properties Wf and I pretty soon, while we will use Property U only once, and much later on. All right, this being done, let us list the axioms that [Q ⊆ V] should satisfy.

The first axiom is that [Q ⊆ V] is antitonic in Q and monotonic in V: if Q ⊇ Q’ and V ⊆ V’ then [Q ⊆ V] ⊆ [Q’ ⊆ V’]. Indeed, every element f of [Q ⊆ V] is such that f[Q] ⊆ V, so f[Q’] ⊆ f[Q] ⊆ V ⊆ V’. If we order compact saturated subsets by reverse inclusion ⊇ and open subsets by ordinary inclusion ⊆, this axiom says that the map (Q, V) ↦ [Q ⊆ V] is monotonic. I will not include that axiom in my list of axioms, though, as it is a consequence of axioms (Infs,left) and (Infs,right) below; this is because any map that preserves binary infima has to be monotonic already.

The (remaining) axioms are of the following five kinds.

  1. (Infs,left) For all Q1, …, Qn ∈ QX, ∩i=1n [Qi ⊆ V] ⊆ [∪i=1n Qi ⊆ V]. In fact the two sides of the inclusion are equal: it is equivalent for a function f to map every element of each Qi to a point of V, or to map every element of ∪i=1n Qi to a point of V. But the converse inclusion [∪i=1n Qi ⊆ V] ⊆ ∩i=1n [Qi ⊆ V] is an immediate consequence of Axiom 1, so we do not need to write it down.
    One can equivalently state Axiom 2 as two subaxioms, corresponding to the cases n=0 and n=2: X ⊆ [∅ ⋐–1 V], and [Q1 ⊆ V] ∩ [Q2 ⊆ V] ⊆ [Q1 ∪ Q2 ⊆ V].
    Alternatively, this axiom means that the map Q ↦ [Q ⊆ V] (with V fixed) preserves finite infima; note that, since the ordering on QX is reverse inclusion, finite infima in QX are unions.
  2. (Infs,right) For every finite list of open subsets V1, …, Vn of X, ∩i=1n [Q ⊆ Vi] ⊆ [Q ⊆ ∩i=1n Vi]. Similar comments apply. Equivalently, X ⊆ [Q ⊆ Y] and [Q ⊆ V1] ∩ [Q ⊆ V2] ⊆ [Q ⊆ V1 ∩ V2].
    Alternatively, the map V ↦ [Q ⊆ V] (with Q fixed) preserves finite infima.
  3. (Cont.,right) For every directed family (Vi)i ∈ I of open subsets of Y, [Q ⊆ ∪i ∈ I Vi] ⊆ ∪i ∈ I [Q ⊆ Vi]. Again, equality holds. Now this is a statement about the compactness of Q. For every continuous map f from X to Y, if f[Q] ⊆ ∪i ∈ I Vi, then, using the fact that f[Q] is compact, and that the family (Vi)i ∈ I is directed, f[Q] must be included in some Vi; namely, f must be in some [Q ⊆ Vi].
    In other words, the map V ↦ [Q ⊆ V] (with Q fixed) is Scott-continuous.
  4. (Cont.,left) For every filtered family (Qi)i ∈ I of compact saturated subsets of X, [∩i ∈ I Qi ⊆ V] ⊆ ∪i ∈ I [Qi ⊆ V].
    Indeed, for every continuous map f from X to Y, if f[∩i ∈ I Qi] ⊆ V, namely if ∩i ∈ I Qi ⊆ f–1(V), then by Property Wf (well-filteredness), we have Qi ⊆ f–1(V) for some i in I; namely, f is in [Qi ⊆ V] for some i in I.
    As usual, this axiom is really equivalent to the equality [∩i ∈ I Qi ⊆ V] = ∪i ∈ I [Qi ⊆ V], and states that the map Q ↦ [Q ⊆ V] (with V fixed) is Scott-continuous.
  5. (Interpolation) For every finite family of open subsets V1, …, Vn of Y, [Q ⊆ ∪k=1n Vk] ⊆ ∪{∩k=1n [Qk ⊆ Vk] | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}. Indeed, for every f ∈ [Q ⊆ ∪k=1n Vk], by definition, Q is included in f–1(∪k=1n Vk) = ∪k=1n f–1(Vk). By Property I (interpolation), there are compact saturated sets Q1 ⊆ f–1(V1), …, Qn ⊆ f–1(Vn) ∈ QX such that Q ⊆ ∪k=1n int(Qk), and the inclusions Qk ⊆ f–1(Vk) mean that f is in ∩k=1n [Qk ⊆ Vk]. Since f is arbitrary, [Q ⊆ ∪i=1n Vi] ⊆ ∪{∩i=1n [Qi ⊆ Vi] | Q1, …, Qn ∈ QX, Q ⊆ ∪i=1n int(Qi)}, as claimed.
    Let me note that (Interpolation) is equivalent to the equality [Q ⊆ ∪i=1n Vi] = ∪{∩i=1n [Qi ⊆ Vi] | Q1, …, Qn ∈ QX, Q ⊆ ∪i=1n int(Qi)}. In order to prove the right-to-left inclusion, it is enough to note that for all Q1, …, Qn ∈ QX such that Q ⊆ ∪i=1n int(Qi), ∩i=1n [Qi ⊆ Vi] is included in ∩i=1n [Qi ⊆ ∪i=1n Vi] by monotonicity, hence in [∪i=1n Qi ⊆ ∪i=1n Vi] by (Infs,left), hence in [Q ⊆ ∪i=1n Vi] by monotonicity.
    The (Interpolation) property is also equivalent with its subcases n=0, n=1 and n=2.
    • The case n=0 is a bit subtle: there is exactly one list of compact saturated sets Q1, …, Qn in that case, and that is the empty list; that list satisfies Q ⊆ ∪i=1n int(Qi) if and only if Q is empty; so the case n=0 splits into two further subcases:
      • if Q is empty, then exactly one list Q1, …, Qn has to be considered, and then (Interpolation) says that [Q ⊆ ∅] is included in ∩i=1n [Qi ⊆ Vi], which is the empty intersection, namely the whole space; in other words, this subcase tells us nothing;
      • if Q is non-empty, then no list Q1, …, Qn fits our needs, and then (Interpolation) says that [Q ⊆ ∅] is included in the empty union, namely that [Q ⊆ ∅] = ∅.
    • The case n=1 says that [Q ⊆ V] ⊆ ∪{[Q1 ⊆ V] | Q1 ∈ QX, Q ⊆ int(Q1)}, and is a consequence of (Cont.,left) and the fact that every compact saturated subset Q of a locally compact space X is the intersection of its open neighborhoods of the form int(Q1), Q1 ∈ QX. (Exercise! First observe that every open neighborhood U of Q contains such a Q1, by Property I.) Conversely, this n=1 case implies (Cont.,left). (Exercise again; use Property Wf.) Hence (Cont.,left) is redundant.
    • The case n=2 says that [Q ⊆ V1 ∪ V2] ⊆ ∪{[Q1 ⊆ V1] ∩ [Q2 ⊆ V2] | Q1, Q2 ∈ QX, Q ⊆ int(Q1) ∪ int(Q2)}.

A preframe is a dcpo with finite infima, and a preframe morphism is a Scott-continuous map that preserves finite infima. The first four axioms above say that [Q ⊆ V] is a preframe morphism in each of the two variables Q and V. I will call such functions that are preframe morphisms in each argument separately C-preframe morphisms. As usual, the C- prefix is for `componentwise’.

Additionally, we have axiom (Interpolation).

One might as well axiomatize the core-open topology, but that leads to something slightly more complicated. If you are interested, look at the beginning of the proof of Proposition 3 in [1], where Hyland’s notation a ≪ f*(b) stands for our [a ⋐–1 b]; or at the Appendix of this post.

A candidate for the exponential object

We fix a continuous frame Ω. For each frame L, we will define a frame E(L, Ω) that we claim is the desired exponential object LΩ in the category of locales. Let me warn you that I will spend some time building it, but that eventually the only think we will need to know about it is its universal property, which we will see in the next section; in other words, you may as well skip to the next section, and return here if you have any doubts as to the existence of E(L, Ω).

Since Ω is a continuous frame, and as I have already recalled, we may equate Ω with OX, where X ≝ pt Ω is a locally compact sober space. By imitation with the topological case, we will define E(L, Ω) as an imitation of what the compact-open topology would be if L were the lattice of open sets of a topological space Y as in the previous section.

In other words, we will define the frame E(L, Ω) by generators and relations (we have already explained how one can define frames by generators and relations in a previous post, and I will come back to it), and the generators will be pairs 〈Q, v〉, where Q ranges over the compact saturated subsets of X, and v ranges over L.

The idea is that 〈Q, v〉 is meant to be some kind of syntax for the subbasic compact-open subset [Q ⊆ v] of [X → Y], if L happened to be the lattice of open subsets of a topological space Y, and where v were an open subset of Y. As I often do, I will write actual open subsets in capital letters, such as V, and I will use letters such as u, v, …, for elements of frames.

The recipe for forming frames defined by generators and relations given in the previous post mentioned above consists in forming the free frame over the set of generators, and then taking the sublocale defined by the congruence associated with the relations. Let me be more explicit.

Let G be any set, which we wish to see as a set of generators for a frame. In our case, G = QX × L, the set of pairs 〈Q, v〉, where Q ranges over the compact saturated subsets of X, and v ranges over L. We first form the free frame over G, and that happens to be the frame O(P(G)) of Scott-open subsets of the powerset P(G) of G. (The powerset is ordered by inclusion.) Explicitly, P(G) is an algebraic dcpo, whose basis of finite elements is Pfin(G), the set of finite subsets of G. Then a Scott-open subset of P(G) is the same thing as a union ∪i ∈ I ↑Ai of upward closures of finite elements of P(G). Each Ai is a finite set of generators (of elements of G), and ∪i ∈ I ↑Ai is the collection of sets E of generators that contain some Ai.

If we write Ai as the finite set {〈Qi1, vi1〉, …, 〈Qimi, vimi〉}, then ∪i ∈ I ↑Ai is formally similar to the compact-open set ∪i ∈ I ∩j=1mi [Qij ⊆ vij]. In fact, it is useful to understand ∪i ∈ I ↑Ai as some form of syntax for the latter. It is standard in locale theory to think of ∪i ∈ I ↑Ai as an abstract formula obtained as the (possibly infinite) disjunction over i ∈ I of the finite conjunctions, over j=1, …, mi, of the atomic formulae 〈Qij, vij〉. To fix ideas, let us write that as ⊔i ∈ I ⊓j=1mi 〈Qij, vij〉. This formula is subject to conjunctions ⊓ being associative, commutative, and idempotent, and similar for disjunctions ⊔, and also to the frame distributivity law (implicit in the fact that we have normalized our formulae by putting all conjunctions ⊓ below all disjunctions ⊔) but no other law is imposed on such formulae—for now.

In order to impose the other laws, which in our case will be transcriptions of the axioms (Infs,left), (Infs,right), (Cont.,left), (Cont.,right) and (Interpolation) of the compact-open topology, we quotient this free frame O(P(G)) (where G = QX × L, here) by a collection of relations. Formally, these relations are formal equalities up≡vp, where p ranges over some set of indices. (One could also allow for formal inequalities, but we will not need this, and in any case the two approaches are equivalent.)

For example, (Infs,left) will be transcribed into the relations ⊓k=1n 〈Qk, v〉 ≡ 〈∪k=1n Qk, V〉. That relation has to be compatible with the formation of formulae, and really means that in a formula ⊔i ∈ I ⊓j=1mi 〈Qij, vij〉, we can pick some i in I, look at the conjunction ⊓j=1mi 〈Qij, vij〉, and if there are several different values of j such that vij is the same element v, let us say j=1, j=2, and j=5, then we can replace the three terms 〈Qi1, v〉, 〈Qi2, v〉 and 〈Qi5, v〉 by the single term 〈Qi1 ∪ Qi2 ∪ Qi5, v〉; and conversely. The zero-ary case of this is that we can always remove (or insert back) any term of the form 〈∅, v〉 in a conjunction.

Formally, we ought to build the quotient O(P(G))/≡ of O(P(G)) by the smallest frame congruence ≡ defined by the equations up≡vp which we will have decided upon. But I guess the human mind is better made to understand the informal idea of symbolic formulae ⊔i ∈ I ⊓j=1mi 〈Qij, vij〉 (up to frame laws for ⊔ and ⊓), modulo a collection of axioms, rather than the formal view, as O(P(G))/≡, so we will reason with the former. Now, explicitly, here are the axioms we will impose:

  1. (Infs,left) ⊓k=1n 〈Qk, v〉 ≡ 〈∪k=1n Qk, v〉
  2. (Infs,right) ⊓k=1n 〈Q, vk〉 ≡ 〈Q, ⋀k=1n vk〉
  3. (Cont.,right) 〈Q, ⋁i ∈ I vi〉 ≡ ⊔i ∈ I 〈Q, vi〉 if (vi)i ∈ I is directed
  4. (Cont.,left) 〈∩i ∈ I Qi, v〉 ≡ ⊔i ∈ I 〈Qi, v〉 if (Qi)i ∈ I is filtered (i.e., directed in QX under ⊇)
  5. (Interpolation) 〈Q, ⋁k=1n vk〉 ≡ ⊔{⊓k=1n 〈Qk, vk〉 | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}.

As in the case of the compact-open topology, the case n=1 of (Interpolation) is equivalent to (Cont.,left), and therefore (Cont.,left) is redundant, but I am leaving it in for symmetry with (Cont.,right).

We let E(L, Ω) denote the collection of symbolic formulae ⊔i ∈ I ⊓j=1mi 〈Qij, vij〉 (up to frame laws for ⊔ and ⊓), where each Qij is compact saturated in X (remembering that Ω=OX, and that X is locally compact and sober), each vij is an element of L, modulo the five axioms we have just stated.

I will write F, G, … for such symbolic formulas, modulo the axioms, namely for elements of E(L, Ω). I will also confuse the formulae with their equivalence classes modulo ≡, unless otherwise stated. Using the frame axioms, one can define operations ⊓ and ⊔ on formulas, and they satisfy the frame axioms; I will not verify this here. In particular, there is an ordering on E(L, Ω), defined by F≤G if and only if F ⊔ G ≡ G, if and only if F ⊓ G ≡ F, and this ordering turns ⊓ into the corresponding infimum operation, and ⊔ into supremum. In particular, ⊔ and ⊓ are monotonic, and Scott-continuous; also, one should notice that the ordering restricts to generators 〈Q, v〉 ≤ 〈Q’, v’〉 if and only if Q ⊇ Q’ and v≤v’—namely, the componentwise ordering, paying attention to the fact that the ordering on compact saturated subsets is reverse inclusion ⊇ (and where ≤ in v≤v’ refers to the ordering on L).

The universal property of E(L, Ω), and interpolating C-preframe morphisms

There is a notation that locale theorists would use in order to describe E(L, Ω) in a concise way:

E(L, Ω) = Fr ((Q, v) ∈ QX × L | (_, _) qua preframe in each coordinate, (Interpolation))

meaning that E(L, Ω) is the free frame over generators 〈Q, v〉 ∈ QX × L, modulo the equations stating that the two coordinatewise maps Q ↦ 〈Q, v〉 and V ↦ 〈Q, v〉 should be understood as preframe morphisms (namely, should be Scott-continuous and preserve finite infima) and modulo the (Interpolation) law; or, as we have already said, that the map (Q, v) ↦ 〈Q, v〉 should be a C-preframe morphism satisfying (Interpolation).

I find this notation somehow obscure (and I may simply have failed to imitate similar notations, for that matter! If so, that will show how little I understand that kind of notation). But that notation is meant to be indicative of the following universal property. The good news is that this is the only thing we will need to remember about E(L, Ω)!

Let me say that a C-preframe morphism φ : QX × L → L’ is interpolating (or satisfies (Interpolation), by extension) if and only if it satisfies the following analogue of (Interpolation):

φ(Q, ⋁k=1n vk) = ⋁{⋀k=1n φ(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}.

Lemma A. Let X be a locally compact sober space and L and L’ be two frames.

  1. For every interpolating C-preframe morphism φ : QX × L → L’, there is a unique frame homomorphism Φ : E(L, Ω) → L’ that extends φ, in the sense that Φ(〈Q, v〉) = φ(Q, v) for every pair (Q, v) ∈ QX × L.
  2. Every frame homomorphism Φ : E(L, Ω) → L’ restricts to an interpolating C-preframe morphism φ : QX × L → L’, namely φ(Q, v) = Φ(〈Q, v〉) for every pair (Q, v) ∈ QX × L.

Proof. 1. We must define Φ as mapping every formula ⊔i ∈ I ⊓j=1mi 〈Qij, vij〉 to ⋁i ∈ I ⋀j=1mi φ(Qij, vij). This shows uniqueness. In order to show that Φ is well-defined, we need to show that it maps ≡-equivalent formulae to the same element of L’. But that is exactly the statement that φ is an interpolating C-preframe morphism.

2. The map (Q, v) ↦ 〈Q, v〉 is a C-preframe morphism, and φ is obtained by composing Φ with it. Since Φ is a frame homomorphism, it is in particular a C-preframe morphism, and then we observe that C-preframe morphisms compose. It remains to verify that φ is interpolating. We have φ(Q, ⋁i=1n vi) = Φ(〈Q, ⋁i=1n vi〉). By (Interpolation), this is equal to Φ(⊔{⊓i=1n 〈Qi, vi〉 | Q1, …, Qn ∈ QX, Q ⊆ ∪i=1n int(Qi)}. Since Φ is a frame homomorphism, this is equal to ⋁{⋀i=1n Φ〈Qi, vi〉 | Q1, …, Qn ∈ QX, Q ⊆ ∪i=1n int(Qi)}, namely to ⋁{⋀i=1n φ(Qi, vi) | Q1, …, Qn ∈ QX, Q ⊆ ∪i=1n int(Qi)}. ☐

As I said, Lemma A is the only thing we will need to know about E(L, Ω). So you can forget about formulae F, and the axioms modulo which they should be taken. From now now, we will replace all that by the study of certain interpolating C-preframe morphisms.

The Λ operator

In order to show that E(L, Ω) is the exponential LΩ and Ω of L and Ω in the category Loc of locales, we may first attempt to find an application morphism App : E(L, Ω) ×loc Ω → L in Loc, namely a frame homomorphism App from L to E(L, Ω) ×loc Ω. That turns out to be the hard way of doing it. We will have to do it anyway! but let us start with things that are more accessible.

Instead, we will start by defining the currification operator Λ (just like Hyland). Given a morphism of locales g : L’ ×loc Ω → L, Λ(g) should be a morphism of locales from L’ to E(L, Ω). Equivalently, given a frame homomorphism g : L → L’ ×loc Ω, we are looking for a frame homomorphism Λ(g) : E(L, Ω) → L’. We have just seen—in Lemma A—that is was equivalent to look for an interpolating C-preframe morphism φ : QX × L → L’; then Λ(g) will be its uniquely defined extension Φ as a frame homomorphism. As usual, we assume that Ω is a continuous frame, and that Ω=OX, where X is a locally compact sober space.

Let us try to imagine what it can be, by imitation from the case of topological spaces. Instead of g, we consider a continuous map f : Z × X → Y, and we think of g as being the frame homomorphism f–1. L’ corresponds to OZ, and L corresponds to OY, but only for the purposes of the analogy. In Top, Λ(f) : Z → [X → Y] maps every point z of Z to the continuous map f(z, _) : X → Y. The analogue of Λ(g) is the frame homomorphism Λ(f)–1 : O([X → Y]) → OZ, and we need to compute Λ(f)–1 ([Q ⊆ V]), for every subbasic open set [Q ⊆ V] of the compact-open topology on [X → Y]. This is equal to {z ∈ Z | ∀x ∈ Q, f(z,x) ∈ V}.

We wish to write this as a function of the frame homomorphism f–1, and to this end we write it as {z ∈ Z | ∀x ∈ Q, (z,x) ∈ f–1(V)}. Now f–1(V) is open in Z × X, hence is a union of open rectangles W × U in that product. Therefore Λ(f)–1 ([Q ⊆ V]) is the union of all the open subsets W of X such that there is an open subset U of X such that Q ⊆ U and W × U ⊆ f–1(V). Let me show the difficult implication only: if z is such that ∀x ∈ Q, (z,x) ∈ f–1(V), then there is an open rectangle W × U ⊆ f–1(V) such that Q ⊆ U. Indeed, for every x ∈ Q, we can find an open rectangle Wx × Ux ⊆ f–1(V) that contains the pair (z, x). Since Q is compact, and the open sets Ux cover Q, there is a finite subcover (Ux)x ∈ E, namely, we can pick a finite subset E of Q such that Q ⊆ ∪x ∈ E Ux; then we let U be ∪x ∈ E Ux and W be ∩x ∈ E Ux.

This leads us to the following definition in the world of locales. As we did earlier, ×loc denotes product in Loc, and is built as the frame of C-ideals of its two argument frames.

Definition (λ(g)). For every frame homomorphism g : L → L’ ×loc Ω (with Ω=OX), we let λ(g) : QX × L → L’ be defined by:

λ(g)(Q, v) ≝ ⋁{w ∈ L’ | w ⊗ U ∈ g(v) for some open neighborhood U of Q in X}.

Since the ⊗ commutes with C-suprema, and since g(v) is an ideal, the supremum defining λ(g)(Q, v) is attained: λ(g)(Q, v) is the largest element w of L’ such that w ⊗ U ∈ g(v) for some open neighborhood U of Q in X.

Lemma B. If X is well-filtered, then λ(g) is a C-preframe morphism.

(I have stated the assumption on X explicitly, so as to stress the fact that we do not need X to be locally compact here. We will require it in order to show that λ(g) is interpolating, which we will do separately.)

Proof. A word of warning: this is a pretty long verification. We have four axioms to verify, and each will take a bit of time; in fact, I will devote a subsection to each one of them. The most complex of all is the final one, (Cont.,right).

First, λ(g) is monotonic: if you make v grow, then g(v) will grow, hence will contain more rectangles w ⊗ U, and therefore the sup of the corresponding values of w will grow, too; if you make Q grow (in QX, namely if you replace Q by a smaller compact saturated set), then this gives you more open neighborhoods U from which we can choose, hence again a supremum of a larger family.

Verifying (Infs,left).

We consider finitely many compact saturated sets Q1, …, Qn. Since λ(g) is monotonic, it is enough to show that λ(g)(∪k=1n Qk, v) ≥ ⋀k=1n λ(g)(Qk, v); said otherwise, the reverse inequality holds by monotonicity, remembering that ∪ is infimum in QX. Let w1 ≝ λ(g)(Q1, v), …, wn ≝ λ(g)(Qn, v). Since each wk is the largest element such that wk ⊗ Uk ∈ g(v) for some open neighborhood Uk of Qk in X, in particular we can find such open neighborhoods Uk of Qk such that wk ⊗ Uk ∈ g(v). Then U ≝ ∪k=1n Uk is an open neighborhood of ∪k=1n Qk, and I claim that w ⊗ U ∈ g(v), where w ≝ ⋀k=1n wk.

The reason is that, since a C-ideal is downwards-closed, and since wk ⊗ Uk ∈ g(v), we must also have w ⊗ Uk ∈ g(v) (at least if n≠0). Then since a C-ideal is closed under componentwise suprema, and in particular in the second argument, we obtain that w ⊗ U is in g(v)—at least if n≠0. If n=0, then U is empty, and in that case w ⊗ U is the bottom rectangle, which lies in every C-ideal.

We have obtained that w ⊗ U ∈ g(v), where U is an open neighborhood of ∪k=1n Qk. By definition of λ(g), it follows that λ(g)(∪k=1n Qk, v) ≥ w. This completes the proof of this first part, since w ≝ ⋀k=1n wk and wk = λ(g)(Qk, v) for each k.

Verifying (Infs, right).

We consider finitely many elements v1, …, vn of L. As before, by monotonicity we only have to show that λ(g)(Q, ⋀k=1n vk) ≥ ⋀k=1n wk, where wk ≝ λ(g)(Q, vk). If n=0, then the left-hand side is λ(g)(Q, ⊤); g(⊤) is the largest C-ideal, namely the collection of all rectangles w ⊗ U, and therefore the supremum of the corresponding values of w (when U ranges over the open neighborhoods of Q) is ⊤, which is certainly larger than or equal to the right-hand side. Let us therefore assume n≠0.

By definition of wk as λ(g)(Q, vk)., there are open neighborhoods Uk of Q such that wk ⊗ Uk ∈ g(vk). The intersection U of all the open sets Uk (which are only finitely many) is still an open neighborhood of Q, and because C-ideals are downwards-closed, wk ⊗ U is in g(vk) for every k, and then again that (⋀k=1n wk) ⊗ U is in every g(vk). Hence (⋀k=1n wk) ⊗ U is in ∩k=1n g(vk), which is equal to g(⋀k=1n vk), since g, as a frame homomorphism, preserves finite infima (and because finite infima of C-ideals are computed as intersections).

We have obtained that (⋀k=1n wk) ⊗ U is in g(⋀k=1n vk); U is an open neighborhood of Q, therefore, by definition of λ(g), we obtain that λ(g)(Q, ⋀k=1n vk) ≥ ⋀k=1n wk, which is what we wanted to show.

Verifying (Cont.,left).

Let (Qi)i ∈ I be a filtered family of compact saturated subsets of X. We wish to show that λ(g)(∩i ∈ I Qi, v) = ∨i ∈ I λ(g)(Qi, v). By monotonicity, we only need to prove the ≤ direction. Let w ≝ λ(g)(∩i ∈ I Qi, v). By definition, there is an open neighborhood U of ∩i ∈ I Qi such that w ⊗ U is in g(v). Since X is well-filtered, U must in fact contain Qi for some i in I. This shows that w ≤ λ(g)(Qi, v), and we are done.

Verifying (Cont.,right).

Let (vi)i ∈ I be a directed family in L. We wish to show that λ(g)(Q, ∨i ∈ I vi) = ∨i ∈ I λ(g)(Q, vi). By monotonicity, once again, we only need to prove the ≤ direction. This is the hardest property of all. The left-hand side, λ(g)(Q, ∨i ∈ I vi), is the supremum of all values w such that w ⊗ U is in g(∨i ∈ I vi) for some open neighborhood U of Q. Taking the largest possible one will be useless here. Instead, we need to show that all those possible values w are ≤ ∨i ∈ I λ(g)(Q, vi).

We know that g(∨i ∈ I vi) = ∨i ∈ I g(vi), since g is a frame homomorphism, but the supremum ∨i ∈ I g(vi) is a supremum of C-ideals, and suprema of C-ideals are complicated objects: you need to take unions, and then to complete under componentwise suprema, for transfinitely long.

In order to get started, we can at least show that every value w such that w ⊗ U is in the union ∪i ∈ I g(vi) (not the supremum) for some open neighborhood U of Q is ≤ ∨i ∈ I λ(g)(Q, vi) (whatever compact saturated Q we take). Indeed, in that special case, w ⊗ U is in ∪i ∈ I g(vi) for some i in I, and then by definition of λ(g), we have w ≤ λ(g)(Q, vi). In particular, w ≤ ∨i ∈ I λ(g)(Q, vi).

That is a good start. Let us rephrase: for every rectangle w ⊗ U in ∪i ∈ I g(vi), for every compact saturated set Q ⊆ U, we have the inequality w ≤ ∨i ∈ I λ(g)(Q, vi). Hence let C be the collection of rectangles w ⊗ U such that for every compact saturated set Q ⊆ U, w ≤ ∨i ∈ I λ(g)(Q, vi). We have just shown that ∪i ∈ I g(vi) is included in C.

Also, C is a C-ideal; most conditions are trivial, and we concentrate on the preservation of suprema in the second component. In other words, let w be fixed, and let (Uj)j ∈ J be a family (not necessarily directed) of open subsets of X such that, for every j in J, the rectangle w ⊗ Uj is in C; explicitly, for every compact saturated set Q ⊆ Uj, w ≤ ∨i ∈ I λ(g)(Q, vi). We let U ≝ ∪j ∈ J Uj, and we wish to show that the rectangle w ⊗ U is in C. In order to do so, we consider an arbitrary compact saturated set Q ⊆ U, and we wish to show that w ≤ ∨i ∈ I λ(g)(Q, vi).

  • Since Q ⊆ U and Q is compact, there is a finite subfamily K of J such that Q ⊆ ∪k ∈ K Uk. By Property I, there are compact saturated subsets Qk ⊆ Uk, one for each k in K, such that Q ⊆ ∪k=1n int(Qk).
  • Since w ⊗ Uk is in C for every k in K, and since Qk ⊆ Uk, we have w ≤ ∨i ∈ I λ(g)(Qk, vi), by definition of C.
  • Taking the conjunction over the finitely many indices k in K, and since the frame distributivity law implies in particular that ∧ is Scott-continuous, w ≤ ⋀k=1n ∨i ∈ I λ(g)(Qk, vi) = ∨i ∈ I ⋀k=1n λ(g)(Qk, vi).
  • We use the fact that λ(g) preserves finite infima componentwise, and we obtain that w ≤ ∨i ∈ I λ(g)(∪k ∈ K Qk, vi). Since Q ⊆ ∪k=1n int(Qk), in particular Q ⊆ ∪k=1n Qk, so by monotonicity of λ(g) (and remembering that the ordering on QX is reverse inclusion), w ≤ ∨i ∈ I λ(g)(Q, vi), which is what we wanted to prove.

Let us summarize: C is a C-ideal, and it contains ∪i ∈ I g(vi). Hence it contains the smallest C-ideal containing ∪i ∈ I g(vi), which is ∨i ∈ I g(vi). Expanding the definition of C, we obtain that for every rectangle w ⊗ U in ∨i ∈ I g(vi), for every compact saturated set Q ⊆ U, w ≤ ∨i ∈ I λ(g)(Q, vi). Equivalently, and essentially just permuting quantifiers, for every Q ∈ QX, every w such that w ⊗ U is in in ∨i ∈ I g(vi) for some open neighborhood U of Q, w ≤ ∨i ∈ I λ(g)(Q, vi). Fixing Q and taking suprema over w, it follows that λ(g)(Q, ∨i ∈ I vi) ≤ ∨i ∈ I λ(g)(Q, vi), and we are finally done! (End of proof of Lemma B.) ☐

Lemma C. If X is locally compact and sober, then λ(g) is an interpolating C-preframe morphism.

Proof. We only need to show (Interpolation). The hard direction of the proof uses the same trick with suprema of C-ideals as the one we just used in the proof of (Cont.,right). If you think you have understood it, you can skip this proof. Alternately, you may read the following with the aim of understanding the technique.

Let v ≝ ∨k=1n vk. We wish to show that λ(g)(Q, v) = ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}. The ≥ direction is easy: for every list Q1, …, Qn ∈ QX such that Q ⊆ ∪i=1n int(Qi), we have ⋀k=1n λ(g)(Qk, vk) ≤ ⋀k=1n λ(g)(Qk, v) = λ(g)(∪k=1n Qk, v) by monotonicity and (Infs,left), and that is smaller than or equal to λ(g)(Q, v) by monotonicity.

In the ≤ direction, we need to show that for every rectangle w ⊗ U in g(v), where U is an open neighborhood of Q, we have w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}. Since g is a frame homomorphism, g(v) = ∨k=1n g(vk), and the latter is supremum of C-ideals, not a union.

In the ≥ direction, let C be the collection of rectangles w ⊗ U such that for every compact saturated set Q ⊆ U, w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}.

  • We first claim that ∪k=1n g(vk) is included in C. For every rectangle w ⊗ U in ∪k=1n g(vk), w ⊗ U is in some g(vj). By definition of λ(g), w ≤ λ(g)(Q, vj) for every compact saturated set Q ⊆ U. Fixing any such Q, there is a compact saturated set Qj such that Q ⊆ int(Qj) ⊆ Qj ⊆ U. This is the interpolation property of locally compact spaces (Proposition 4.8.14 in the book), or equivalently Property I in the case of just one open set. By definition of λ(g), w ≤ λ(g)(Qj, vj). We choose the other compact saturated sets Q1, …, Qj–1, Qj+1, …, Qn to be empty. Since λ(g)(∅, vj) = ⊤ by (Infs.,left), we easily obtain that w ≤ ⋀k=1n λ(g)(Qj, vj). Also, Q ⊆ ∪k=1n int(Qk). Therefore so w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}.
  • We claim that C is a C-ideal. The only difficult point is to show that it is closed under suprema taken over second coordinates. Let therefore w be fixed, and let (Uj)j ∈ J be a family (not necessarily directed) of open subsets of X such that, for every j in J, the rectangle w ⊗ Uj is in C. We let U ≝ ∪j ∈ J Uj, and we wish to show that the rectangle w ⊗ U is in C. In order to do so, we consider an arbitrary compact saturated set Q ⊆ U, and we wish to show that w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}.
    • Since Q ⊆ U = ∪j ∈ J Uj, there is a finite subfamily J’ of J such that Q ⊆ ∪j ∈ J’ Uj. By Property I, there are compact saturated subsets Q’j ⊆ Uj, one for each j in J’, such that Q ⊆ ∪j ∈ J’ int(Q’j).
    • For each j in J’, w ⊗ Uj is in C. By definition of C, applied to Q’j ⊆ Uj, w ≤ ⋁{⋀k=1n λ(g)(Qjk, vk) | Qj1, …, Qjn ∈ QX, Q’j ⊆ ∪k=1n int(Qjk)}.
    • Taking infima over all j in J’, w ≤ ⋀j ∈ J’ ⋁{⋀k=1n λ(g)(Qjk, vk) | Qj1, …, Qjn ∈ QX, Q’j ⊆ ∪k=1n int(Qjk)}. Distributing ⋁ over ⋀, w is less than or equal to ⋁{⋀j ∈ J’ ⋀k=1n λ(g)(Qjk, vk) | ∀j ∈ J’, Qj1, …, Qjn ∈ QX, Q’j ⊆ ∪k=1n int(Qjk)}, namely to ⋁{⋀k=1n λ(g)(∪j ∈ J’ Qjk, vk) | ∀j ∈ J’, Qj1, …, Qjn ∈ QX, Q’j ⊆ ∪k=1n int(Qjk)}, since λ(g) satisfies (Infs,left).
    • In any situation where the condition ∀j ∈ J’, Q’j ⊆ ∪k=1n int(Qjk) holds, the condition Q ⊆ ∪k=1n int(∪j ∈ J’ Qjk) also holds, because Q ⊆ ∪j ∈ J’ int(Q’j), hence Q ⊆ ∪j ∈ J’ ∪k=1n int(Qjk) = ∪k=1n ∪j ∈ J’ int(Qjk) ⊆ ∪k=1n int(∪j ∈ J’ Qjk). It follows that the supremum ⋁{⋀k=1n λ(g)(∪j ∈ J’ Qjk, vk) | ∀j ∈ J’, Qj1, …, Qjn ∈ QX, Q’j ⊆ ∪k=1n int(Qjk)} is less than or equal to the supremum ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}, which is a supremum of the same quantities taken over a larger indexing set.
    • Therefore w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}, completing the proof.
  • Summing up, C is a C-ideal that contains ∪k=1n g(vk), hence it contains ∨k=1n g(vk). Expanding the definition of C, for every rectangle w ⊗ U in ∨k=1n g(vk), for every compact saturated set Q ⊆ U, w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}. Equivalently, for every Q ∈ QX, if w ⊗ U in ∨k=1n g(vk) for some open neighborhood U of Q, then w ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}. By taking suprema over w, λ(g)(Q, v) ≤ ⋁{⋀k=1n λ(g)(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}, as desired. ☐

Let us summarize what we have obtained. Given any frame homomorphism g : L → L’ ×loc Ω, we have built an interpolating C-preframe morphism φ=λ(g) : QX × L → L’ (Lemmata B and C), which extends to a unique frame homomorphism Φ : E(L, Ω) → L’ by Lemma A. We will write that Φ as Λ(g): this will be define the currification operator Λ we need on Loc!

The inverse of Λ

If Ω is exponentiable, and if E(L, Ω) is really the exponential object LΩ, then the function Λ, which maps every morphism of locales g : L’ ×loc Ω → L to a morphism of locales Λ(g) : L’ → E(L, Ω), should have an inverse. Indeed, there should be an application morphism App : E(L, Ω) ×loc Ω → L in Loc, and the inverse should map any morphism of locales h : L’ → E(L, Ω) to App o (h × idΩ) : L’ ×loc Ω → L. One can check this from the equations (β) App o (Λ(g) × idΩ) = g in one direction; and, in the other direction, by using the equations (η) Λ(App) = idE(L, Ω) and (σ) Λ(f) o h = Λ(f o (h × idΩ)) to infer Λ(App o (h × idΩ)) = h. Or one may remember that an equivalent definition of exponential objects is that _ ×loc Ω should be left adjoint to E(_, Ω), so that there should be a (natural) bijection between the set of morphisms from L’ ×loc Ω to L in Loc and the set of morphisms from L’ to E(L, Ω) in Loc.

Hence, let us take any frame homomorphism Φ : E(L, Ω) → L’. By Lemma A, it restricts to a C-preframe morphism φ : QX × L → L’. We wish to show that there is a unique frame homomorphism g : L → L’ ×loc Ω such that φ=λ(g). It will follow that g is the unique frame homomorphism such that Φ=Λ(g).

Once again, let us try to find that inverse by analogy with the case of topological spaces. In that case, (and assuming X locally compact and sober, as usual), App : [X → Y] × X → Y maps (f, x) to f(x), and given any continuous map h : Z → [X → Y], h is equal to Λ(f) for some unique continuous map f : Z × X → Y, which we obtain as App o (h × idX). The corresponding frame homomorphism (App o (h × idX))–1 maps every open subset V of Y to (App o (h × idX))–1(V) = {(z, x) ∈ Z × X | h(z)(x) ∈ V}. I claim that this is equal to

(App o (h × idX))–1(V) = ∪{W × U | ∀Q ⊆ U, W ⊆ h–1([Q ⊆ V])},

where W ranges over the open subsets of Z, U over those of X, and Q over QX. Here is how we prove the equality:

  • For every pair (z, x) in (App o (h × idX))–1(V), by definition h(z)(x) is in V, so x is in the open set h(z)–1(V). Since X is locally compact, there is a compact saturated subset Q0 of X such that x ∈ int(Q0) ⊆ Q0 ⊆ h(z)–1(V). Let U ≝ int(Q0) and W ≝ h–1([Q0 ⊆ V]). It remains to show that for every compact saturated set Q ⊆ U, W ⊆ h–1([Q ⊆ V]). And indeed, if Q ⊆ U then Q ⊆ Q0, so [Q0 ⊆ V] is included in [Q ⊆ V], from which it follows that W = h–1([Q0 ⊆ V]) ⊆ h–1([Q ⊆ V]).
  • Conversely, if (z, x) is in an open rectangle W × U such that for every compact saturated set Q ⊆ U, W ⊆ h–1([Q ⊆ V]), then we can apply this to Q ≝ ↑x. Then z is in W, hence in h–1([Q ⊆ V]); so h(z) maps every element of Q, in particular x, to V.

The formula we just gave for (App o (h × idX))–1(V) is not the only one. For example, it is also equal to ∪Q ∈ QX (h–1([Q ⊆ V]) × int(Q)). However, the formula ∪{W × U | ∀Q ⊆ U, W ⊆ h–1([Q ⊆ V])} is easier to imitate in Loc. We will make the link with ∪Q ∈ QX (h–1([Q ⊆ V]) × int(Q)) in Lemma Alt below.

Let us imitate that in Loc. We consider an arbitrary interpolating C-preframe morphism φ : QX × L → L’, obtained as the restriction of a frame homomorphism Φ : E(L, Ω) → L’ (a morphism from L’ to E(L, Ω) in Loc); φ plays the rôle of h–1. We then define a map g : L → L’ ×loc Ω (or rather, gφ, in order to show the dependency on φ) by letting:

gφ(v) ≝ {w ⊗ U | ∀Q ⊆ U, w≤φ(Q,v)},

where w ranges over L’, U over Ω=OX, and Q over QX; and, as usual, X is locally compact and sober.

Lemma. gφ(v) is a C-ideal for every v in L.

Proof. It is clear that gφ(v) is downwards-closed, and closed under suprema on the first components, namely on w. Let us show that it is closed under suprema on the second components. Let (Ui)i ∈ I be any directed family of open subsets of X such that each rectangle w ⊗ Ui is in gφ(v), let U ≝ ∪i ∈ I Ui, and let us show that w ⊗ U is in gφ(v). For every compact saturated set Q ⊆ U, Q is included in some Ui (by compactness), and since w ⊗ Ui is in gφ(v), w≤φ(Q,v), by definition of gφ(v). Hence w ⊗ U is in g(v). ☐

Lemma. The map gφ preserves finite infima.

Proof. Let v1, …, vn be finitely many elements in L, and v ≝ ⋀k=1n vk. Intersections of C-ideals are C-ideals, so ⋀k=1n gφ(vk) = ∩k=1n gφ(vk). The latter is equal to ∩k=1n {w ⊗ U | ∀Q ⊆ U, w≤φ(Q,vk)} = {w ⊗ U | ∀k ∈ {1, …, n}, ∀Q ⊆ U, w≤φ(Q,vk)} = {w ⊗ U | ∀Q ⊆ U, w≤⋀k=1n φ(Q,vk)}. Since φ preserves finite infima in its second argument, the latter is equal to {w ⊗ U | ∀Q ⊆ U, w≤φ(Q,v)}, namely to gφ(v). ☐

I had promised that the formula ∪Q ∈ QX (h–1([Q ⊆ V]) × int(Q)) would have a localic equivalent, and here it is. We will need it to complete the previous lemma and prove that g is a frame homomorphism.

Lemma Alt. For every v in L, gφ(v) is the supremum in L’ ×loc Ω of the C-ideals ↓(φ(Q,v) ⊗ int(Q)), where Q ranges over QX.

Proof. First, we claim that it is an upper bound, namely that for every Q ∈ QX, φ(Q,v) ⊗ int(Q) is a rectangle w ⊗ U such that for every compact saturated set Q’ ⊆ U, w≤φ(Q’,v). And indeed, letting w ≝ φ(Q,v) and U ≝ int(Q), if Q’ ⊆ U then Q’ ⊆ Q, so w = φ(Q,v) ≤ φ(Q’,v), by monotonicity of φ.

Second, we claim that it is the least upper bound. Let C be another upper bound, namely any C-ideal that contains all the open rectangles φ(Q,v) ⊗ int(Q), Q ∈ QX. For every rectangle w ⊗ U in g(v), we wish to show that w ⊗ U lies in C. To this end, we use Property U (see the beginning of this post): there is a family (Qi)i ∈ I of compact saturated subsets of X, all included in U, such that U = ∪i ∈ I int(Qi). Then φ(Qi,v) ⊗ int(Qi) is in C for every x in U, by assumption. Since w ⊗ U is in g(v), and since Qi ⊆ U, we have w ≤ φ(Qi,v), by definition of g(v). Now C, being a C-ideal, is downwards-closed, so w ⊗ int(Qi) is in C. We take the suprema of the latter over all x in U; this is a C-supremum since w is fixed. Since C is a C-ideal, we obtain that w ⊗ U is in C, which is what we wanted to prove. ☐

We use this to show that gφ is a frame homomorphism.

Lemma. The map gφ preserves finite suprema: for all v1, …, vn in L, gφ(⋁k=1n vk) = ⋁k=1n gφ(vk).

Proof. Since gφ preserves finite infima, it is monotonic, so we only have to verify that gφ(⋁k=1n vk) ≤ ⋁k=1n gφ(vk). By Lemma Alt, it is enough to show that for every Q ∈ QX, φ(Q, ⋁k=1n vk) ⊗ int(Q) is in ⋁k=1n gφ(vk). Since φ is interpolating, φ(Q, ⋁k=1n vk) = ⋁{⋀k=1n φ(Qk, vk) | Q1, …, Qn ∈ QX, Q ⊆ ∪k=1n int(Qk)}. (Oh yes, you knew that we would have to use this property at some point, right?)

The ⊗ operator commutes with C-suprema, so φ(Q, ⋁k=1n vk) ⊗ int(Q) is the supremum of ⋀k=1n φ(Qk, vk) ⊗ int(Q) over all lists Q1, …, Qn ∈ QX such that Q ⊆ ∪k=1n int(Qk). Since ⋁k=1n gφ(vk) is a C-ideal, and is therefore closed under suprema taken on first coordinates, it suffices to show that (⋀k=1n φ(Qk, vk)) ⊗ int(Q) is in ⋁k=1n gφ(vk) for all Q1, …, Qn ∈ QX such that Q ⊆ ∪k=1n int(Qk).

Now Q ⊆ ∪k=1n int(Qk) implies that (⋀k=1n φ(Qk, vk)) ⊗ int(Q) ≤ (⋀k=1n φ(Qk, vk)) ⊗ (∪k=1n int(Qk)), so it suffices to show that (⋀k=1n φ(Qk, vk)) ⊗ (∪k=1n int(Qk)) is in ⋁k=1n gφ(vk). Since ⋁k=1n gφ(vk) is a C-ideal, and is therefore closed under suprema take on second coordinates, it suffices to show that (⋀k=1n φ(Qk, vk)) ⊗ int(Qk) is in ⋁k=1n gφ(vk) for each k in {1, …, n}. But this is easy: for each k, (⋀k=1n φ(Qk, vk)) ⊗ int(Qk) ≤ φ(Qk, vk) ⊗ int(Qk), which is in gφ(vk) by definition of gφ. ☐

Lemma. The map gφ is Scott-continuous, and is therefore a frame homomorphism.

Proof. One can always write any supremum as a directed supremum of finite suprema. Hence, together with the previous lemma, Scott-continuity is enough to show the preservation of all suprema. Together with the fact that g preserves finite infima, which we had proved earlier on, this will show that gφ is a frame homomorphism.

Let (vi)i ∈ I be a directed family of elements of L, let v be its supremum. We need to show that gφ(v) ≤ ⋁i ∈ I gφ(vi); the reverse inequality follows automatically from monotonicity.

Using Lemma Alt, this means showing that for every Q ∈ QX, φ(Q, v) ⊗ int(Q) is in ⋁i ∈ I gφ(vi). Since φ is Scott-continuous in its second argument, and since ⊗ commutes with C-suprema, this reduces to showing that ⋁i ∈ I φ(Q, vi) ⊗ int(Q) is in ⋁i ∈ I gφ(vi). Now, since ⋁i ∈ I gφ(vi) is a C-ideal, it is enough to show that, for every i in I, φ(Q, vi) ⊗ int(Q) is in ⋁i ∈ I g(vi). And this is clear, since φ(Q, vi) ⊗ int(Q) is in g(vi), by definition of g. ☐

Finally, we show what we had been after all this time.

Lemma D. φ=λ(gφ).

Proof. We remember that λ(gφ)(Q, v) is defined as ⋁{w ∈ L’ | w ⊗ U ∈ gφ(v) for some open neighborhood U of Q in X}, for every Q ∈ QX and for every v ∈ L. (That was defined way back in this post!). For every rectangle w ⊗ U ∈ gφ(v) where U is an open neighborhood of Q, we have w ≤ φ(Q, v) by definition of gφ(v). Taking suprema, we obtain λ(gφ)(Q, v) ≤ φ(Q, v).

Conversely, by Lemma Alt, gφ(v) = ⋁Q ∈ QX ↓(φ(Q,v) ⊗ int(Q)). In particular, φ(Q,v) ⊗ int(Q) is in gφ(v). By taking w ≝ φ(Q,v) and U ≝ int(Q), we see from the definition of λ(gφ)(Q, v) that w ≤ λ(gφ)(Q, v). In other words, φ(Q, v) ≤ λ(gφ)(Q, v). ☐

Lemma E. gλ(g) = g.

Proof. By definition, gλ(g)(v) = {w ⊗ U | ∀Q ⊆ U, w≤λ(g)(Q,v)}, and λ(g)(Q,v) = ⋁{w ∈ L’ | w ⊗ U’ ∈ g(v) for some open neighborhood U’ of Q in X}. (I have renamed the U used in the definition of λ(g)(Q,v) into U’, so as not to confuse it with the U in the definition of gλ(g)(v).)

Right after the definition of λ(g), we had remarked that the supremum ⋁{w ∈ L’ | w ⊗ U’ ∈ g(v) for some open neighborhood U’ of Q in X}. This means that the condition w≤λ(g)(Q,v) in the definition of gλ(g)(v) is equivalent to “w ⊗ U ∈ g(v) for some open neighborhood U of Q in X“. Hence gλ(g)(v) = {w ⊗ U | ∀Q ⊆ U, ∃U’ ⊇ Q, w ⊗ U’ ∈ g(v)}. This makes it clear that g(v) is included in gλ(g)(v).

Conversely, by Lemma Alt, gλ(g)(v) is also equal to ⋁Q ∈ QX ↓(λ(g)(Q,v) ⊗ int(Q)). Since, for each Q ∈ QX, λ(g)(Q,v) is the largest w such that w ⊗ U’ ∈ g(v) for some open neighborhood U’ of Q in X, in particular λ(g)(Q,v) ⊗ U’ ∈ g(v) for some open neighborhood U’ of Q in X. Since g(v), as a C-ideal, is downwards-closed, and since int(Q) ⊆ U’, it follows that λ(g)(Q,v) ⊗ int(Q) is in g(v), and therefore that ↓(λ(g)(Q,v) ⊗ int(Q)) ⊆ g(v), for every Q ∈ QX. Taking suprema over Q ∈ QX then yields the inclusion gλ(g)(v) ⊆ g(v) we were looking for. ☐

Summing up, we obtain the following.

Proposition F. If Ω=QX where X is locally compact and sober, then the map λ : HomLoc(L’ ×loc Ω, L) → {interpolating C-preframe morphisms : QX × L → L’} is inverse to the map φ ↦ gφ.

Since interpolating C-preframe morphisms from QX × L to L’ are in one-to-one-correspondence with frame homomorphisms from E(L, Ω) to L’ by Lemma A, or equivalently to locale morphisms from L’ to E(L, Ω), we obtain:

Corollary G. If Ω is a continuous frame, then the map Λ : HomLoc(L’ ×loc Ω, L) → HomLoc(L’, E(L, Ω)) is one-to-one.

That almost concludes the proof that E(L, Ω) is the desired exponential object ΩL, hence that every continuous frame Ω is exponentiable. What I have in mind here is that an equivalent definition of exponential objects is that _ ×loc Ω should be left adjoint to E(_, Ω), and that means that we are looking for a natural bijection between HomLoc(L’ ×loc Ω, L) → HomLoc(L’, E(L, Ω)).

Hence… we still have to prove naturality. Seasoned category theorists almost never prove naturality, probably because it is usually felt to be “obvious”; in my experience, “obvious” often turns out to mean “boring and tedious” if you take the courage of proving it, but certainly not “easy to see”. One should be warned that there are famous cases of constructions that look “natural” (in an intuitive sense) but that is not natural (in the categorical sense), and expert category theorists know about this; read Section 6 in the nCatLab page on unnatural isomorphisms, for example.

Additionally, for naturality to make sense, we should first show that E(_, Ω) is a functor, which we haven’t done.

Wrapping up the argument

Instead, I will simply define App and show that the three laws I gave in a previous post to define exponential objects are satisfied. They are:

  • (β) App o (Λ(g) ×loc idΩ) = g for every locale morphism g : L’ ×loc Ω → L,
  • (η) Λ(App) = idE(L, Ω)
  • (σ) Λ(g) o h = Λ(g o (h ×loc idΩ)) for all locale morphisms g : L’ ×loc Ω → L and h : L” → L’.

As usual, Ω=QX where X is locally compact and sober; also, composition o is taken in Loc (not Frm, where it would have to be reversed!)

There is an identity frame homomorphism idE(L, Ω) from E(L, Ω) to E(L, Ω), which restricts to an interpolating C-preframe homomorphism φ0 : QX × L → E(L, Ω). (In other words, the unique frame homomorphism Φ0 that extends φ0 is idE(L, Ω).)

We define App as gφ0. This automatically satisfies (η): we have λ(gφ0)=φ0 by Lemma D; in other words, λ(App)=φ0; by the unique extension result guaranteed by Lemma A, Λ(App) is the unique extension Φ0=idE(L, Ω).

What we need to prove (σ) is the following lemma.

Lemma. For all frame homomorphisms g : L → L’ ×loc Ω and h : L’ → L”, λ((h ×loc idΩ) o g) = h o λ(g) (where compositions are compositions in Frm, not in Loc).

Proof. We recall that λ(g) maps every pair (Q, v) to ⋁{w ∈ L’ | w ⊗ U ∈ g(v) for some open neighborhood U of Q in X}, so h o λ(g) maps (Q, v) to ⋁{h(w) | w ⊗ U ∈ g(v) for some open neighborhood U of Q in X}.

We compare this to λ((h ×loc idΩ) o g)(Q, v) = ⋁{w’ ∈ L” | w’ ⊗ U ∈ (h ×loc idΩ)(g(v)) for some open neighborhood U of Q in nX}. From our previous post on exponentiable locales (look at the definition of products in Loc), (h ×loc idΩ) maps any C-ideal C to ↓{h(w) ⊗ U | w ⊗ U ∈ C}. Therefore λ((h ×loc idΩ) o g)(Q, v) is equal to the supremum of the family of all w’ ≤ h(w) such that w ⊗ U ∈ g(v) for some open neighborhood U of Q in X. This is clearly equal to the formula we have obtained for (h o λ(g))(Q, v) in the previous paragraph. ☐

We use this lemma to prove (σ) as follows. Viewed as a frame homomorphism, the left-hand side Λ(g) o h (where composition is in Loc, not Frm, beware) goes from E(L, Ω) to L”, and is uniquely determined by its values on QX × L, in the sense of Lemma A. In order to reason in Frm, we need to interpret composition the other way around, hence the left-hand side, once restricted to QX × L, is h o λ(g). (Sorry if I repeat myself, but this is important: now o is composition in Frm.) Similarly, the right-hand side restricts to λ(g o (h ×loc idΩ)) (assuming o is composition in Loc), namely to λ((h ×loc idΩ) o g) (where o is now composition in Frm). But we have just seen that λ((h ×loc idΩ) o g) = h o λ(g), and (σ) then follows by the uniqueness of extensions to frame homomorphisms given in Lemma A.

Finally, we obtain (β) as follows. By Corollary G, Λ is one-to-one, so it is enough to check that Λ applied to both sides of (β) gives the same result. (To be clear: now we reason in Loc, with compositions in Loc.) On the left, we have that Λ(App o (Λ(g) ×loc idΩ)) = Λ(App) o Λ(g) = Λ(g), using (σ) then (η)… and we are done.

We can now conclude that, given that Ω is a continuous frame, E(L, Ω) is the desired exponential object ΩL. Together with the converse implication we had obtained in our previous post, we finally obtain M. Hyland’s result:

Theorem [1]. The exponentiable locales are the continuous frames.

Oh, a few final words:

  • What is App, explicitly? We have built App as gφ0, where φ0 is the restriction of idE(L, Ω) as given in Lemma A. Hence, as a frame homomorphism from L to E(L, Ω) ×loc Ω, App maps every v in L to gφ0(v) = {w ⊗ U | ∀Q ⊆ U, w≤φ0(Q,v)} = {w ⊗ U | ∀Q ⊆ U, w≤〈Q, v〉}; or, using Lemma Alt, App(v) = ⋁Q ∈ QX ↓(〈Q, v〉 ⊗ int(Q)). I am not sure we learn something from this, but at least we have explicitly formulae.
    Let me also remind you of the (more or less) explicit formula for abstraction: for every frame homomorphism g : L → L’ ×loc Ω, Λ(g) : E(L, Ω) → L’ is the frame homomorphism uniquely defined by Λ(g)(〈Q, v〉) ≝ λ(g)(Q, v) ≝ ⋁{w ∈ L’ | w ⊗ U ∈ g(v) for some open neighborhood U of Q in X}; and that supremum is attained.
  • At the very beginning of this post, I have said that, since Ω is a continuous frame, Ω is isomorphic to OX, for some locally compact sober space X, and I have used this throughout. I have also said that doing so makes us rely on classical logic and the axiom of choice, through uses of the Hofmann-Lawson theorem. One can dispense with the latter as follows: redo everything that we have done here, replacing open subsets U of X by elements u of Ω, compact saturated subsets Q of X by Scott-open filters F in Ω (i.e., Scott-open subsets of Ω that are closed under finite infima), QX by the frame FΩ of Scott-open filters of Ω. Each time I have used expressions such as “Q ⊆ U“, replace them by “u ∈ F“. If I have done it correctly, the only properties I have used of compact saturated sets are Properties Wf, U, and I that were stated near the beginning of this post; I will let you rephrase them in the new context of filters. You should realize that the only difficulty is to prove the analogue of Property U, and that involves finding certain Scott-open filters; you can do this using Proposition 5.1.19 in the book, but its proof relies on a weak form of the axiom of choice called the axiom of dependent choices. Hence working with filters instead of compact saturated sets won’t buy you much… except making the argument less readable. Hyland instead reasons directly on elements way-below u, instead of Scott-open filters, and this way obtains a constructive proof, and which does not use the axiom of choice either, as far as I can 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. Peter T. Johnstone.  Stone Spaces. Cambridge Studies in Advanced Mathematics 3. Cambridge University Press, 1982.
  3. Peter T. Johnstone.  Sketches of an elephant: A topos theory compendium. Vols 1, 2, Oxford Logic Guides 43, 44, Oxford Science Publications, 2002.
  4. Christopher F. Townsend. A categorical proof of the equivalence of local compactness and exponentiability in locale theory. Cahiers de topologie et géométrie différentielle catégoriques, tome 47, no 3 (2006), pages 233–239.
jgl-2011

— Jean Goubault-Larrecq (July 20th, 2023)

Appendix: Hyland’s axioms

I said that Hyland’s axioms encode properties of the core-open topology instead of the compact-open topology. We consider a continuous frame Ω, an arbitrary frame L, and generators [u ⋐–1 v] where u ∈ Ω and v ∈ L; those are written as a ≪ f*(b) by Hyland. Here are the axioms (a.k.a. the relations):

  1. ⊓k=1n [uk ⋐–1 v] ≡ [⋁k=1n uk ⋐–1 v]
  2. ⊓k=1n [u ⋐–1 vk] ≡ [u ⋐–1 ⋀k=1n vk]
  3. [u ⋐–1 ⋁i ∈ I vi] ≡ ⊔i ∈ I [u ⋐–1 vi] if (vi)i ∈ I is directed
  4. [u ⋐–1 v] ≡ ⊔u’ ∈ Ω, u ≪ u’ [u’ ⋐–1 v]
  5. [u ⋐–1 ⋁i ∈ I vi] ≡ ⊔{⊓j ∈ J [uj ⋐–1 vj] | J finite ⊆ I, (uj)j ∈ J such that u=⋁j ∈ J uj}.

The first two are very close cousins of (Infs,left) and (Infs,right). The third out is adapted from (Cont.,right). The fourth one parallels (Cont.,left), with some rewriting. The fifth one is similar to (Interpolation). Then E(L, Ω) would be defined as the free frame defined by those generators and relations. The analogue of Lemma A would then say that the frame homomorphisms from E(L, Ω) to another frame L’ are in one-to-one correspondence with the maps φ : Ω × L → L’ such that (all variable names below are implicitly universally quantified):

  1. φ maps finite suprema in the first argument to infima: φ(⋁k=1n uk, v) = ⋀k=1n φ(uk, v);
  2. φ preserves finite infima in the second argument: φ(u, ⋀k=1n vk) = ⋀k=1n φ(u, vk);
  3. φ is Scott-continuous in its second argument: φ(u, ⋁i ∈ I vi) = ⋁i ∈ I φ(u, vi) if (vi)i ∈ I is directed;
  4. φ(u, v) = ⋁u’ ∈ Ω, u ≪ u’ φ(u’, v);
  5. φ(u, ⋁i ∈ I vi) = ⋁{⋀j ∈ J φ(uj, vj) | J finite ⊆ I, (uj)j ∈ J such that u=⋁j ∈ J uj}.