{"id":6714,"date":"2023-05-21T16:47:57","date_gmt":"2023-05-21T14:47:57","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=6714"},"modified":"2023-05-21T16:47:57","modified_gmt":"2023-05-21T14:47:57","slug":"exponentiable-locales-i-every-exponentiable-locale-is-continuous","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=6714","title":{"rendered":"Exponentiable locales I: every exponentiable locale is continuous"},"content":{"rendered":"\n<p class=\"wp-block-paragraph\">It seems like I have an obsession about Cartesian-closed categories and exponentiable objects these days, if you consider that my <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=6613\" data-type=\"page\" data-id=\"6613\">latest post<\/a> was on that very topic as well.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The exponentiable objects of <strong>Top<\/strong> are exactly the core-compact spaces.  If <em>X<\/em> is exponentiable, then the exponential <em>Y<sup>X<\/sup><\/em> is the space of all continuous maps from <em>X<\/em> to <em>Y<\/em> for a unique topology, which I call the core-open topology, and also coincides with the so-called Isbell topology (when <em>X<\/em> is core-compact).  This is all explained in Section 5.4 of the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Considering that the category <strong>Loc<\/strong> of locales is related to <strong>Top<\/strong> 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.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Exponentiable objects, and exponentials<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">Let me explain what exponentiable objects and exponentials are in a category <strong>C<\/strong>.  I have already done that, but I hate to refer to other pages.  Instead, let me unashamedly copy what I wrote <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=6613\" data-type=\"page\" data-id=\"6613\">last month<\/a> on the subject.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Given any two objects <em>X<\/em> and <em>Y<\/em> in a category with finite products, the <em>exponential<\/em> <em>Y<sup>X<\/sup><\/em>, if it exists, is an object, together with:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>a morphism App : <em>Y<sup>X<\/sup><\/em> \u00d7 <em>X<\/em> \u2192 <em>Y<\/em> (<em>application<\/em>, sometimes called evaluation);<\/li>\n\n\n\n<li>an operation \u039b (<em>currification<\/em>, sometimes called abstraction), such that \u039b(<em>h<\/em>) is a morphism from <em>Z<\/em> to <em>Y<sup>X<\/sup><\/em> for every morphism <em>h<\/em> : <em>Z<\/em> \u00d7 <em>X<\/em> \u2192 <em>Y<\/em>;<\/li>\n\n\n\n<li>satisfying the equations:\n<ul class=\"wp-block-list\">\n<li>(\u03b2) App o (\u039b(<em>f<\/em>) \u00d7 id<em><sub>X<\/sub><\/em>) =&nbsp;<em>f<\/em>&nbsp;for every morphism <em>f<\/em> : <em>Z<\/em> \u00d7 <em>X<\/em> \u2192 <em>Y<\/em>,<\/li>\n\n\n\n<li>(\u03b7) \u039b(App) = id<sub><em>Y<sup>X<\/sup><\/em><\/sub><\/li>\n\n\n\n<li>(\u03c3) \u039b(<em>f<\/em>) o <em>g<\/em>&nbsp;= \u039b(<em>f<\/em> o (<em>g<\/em> \u00d7 id<em><sub>X<\/sub><\/em>))&nbsp;for all morphisms <em>f<\/em> : <em>Z<\/em> \u00d7 <em>X<\/em> \u2192 <em>Y<\/em> and <em>g<\/em> : <em>Z\u2032<\/em>&nbsp;\u2192 <em>Z<\/em>.<\/li>\n<\/ul>\n<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\">This is discussed in Section 5.5.3 of the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>.  In <strong>Set<\/strong>, every object is exponentiable, <em>Y<sup>X<\/sup><\/em> is the set of all functions from <em>X<\/em> to <em>Y<\/em>, App is the application map (<em>f<\/em>, <em>x<\/em>) \u21a6 <em>f<\/em>(<em>x<\/em>), and \u039b(<em>f<\/em>) maps every point <em>z<\/em> in <em>Z<\/em> to the function <em>x<\/em> \u21a6 <em>f<\/em>(<em>z<\/em>, <em>x<\/em>).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">An object <em>X<\/em> is exponentiable if and only if the exponential <em>Y<sup>X<\/sup><\/em> exists for every object <em>Y<\/em>. Equivalently, <em>X<\/em> is exponentiable if and only if the functor _ \u00d7 <em>X<\/em> has a right adjoint (and that right adjoint is the functor _<em><sup>X<\/sup><\/em>).<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Frames and locales<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">I have already produced a few posts on <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=984\" data-type=\"page\" data-id=\"984\">frames and locales<\/a>.  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 <strong>Frm<\/strong>.  It is customary to call <strong>Loc<\/strong> the dual category <strong>Frm<\/strong><sup>op<\/sup>, and to call its objects (which are just frames\u2014but the morphism are reversed!) <em>locales<\/em>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The point (if I may say so) is that <strong>Top<\/strong> and <strong>Loc<\/strong> are related by Stone duality: an adjunction <strong>O<\/strong> \u22a3 <strong>pt<\/strong> between topological spaces and locales, which restricts to an equivalence of categories between sober spaces and spatial locales; a locale is <em>spatial<\/em> if and only if it is of the form <strong>O<\/strong><em>X<\/em> for some space <em>X<\/em> (up to frame isomorphism).  See Section 8.1 of the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>, for example, or the book by Jorge Picado and Ale\u0161 Pultr [2] for more information on locales.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">As Picado and Pultr do, I prefer to reason with frames, but exponentials in <strong>Loc<\/strong> 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.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Products in locales are a bit complicated.  In the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>, I use the frame of Galois connections Gal(<em>L<\/em>, <em>L&#8217;<\/em>) between two frames <em>L<\/em> and <em>L&#8217;<\/em>, and that serves as the locale product <em>L<\/em> \u00d7<sub>loc<\/sub> <em>L&#8217;<\/em> of <em>L<\/em> and <em>L&#8217;<\/em>.  In this post, I will rather use <em>C-ideals<\/em>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">A <em>C-ideal<\/em> on a pair of frames <em>L<\/em>, <em>L&#8217;<\/em> is a downwards closed set <em>D<\/em> of rectangles <em>u<\/em> \u2297 <em>v<\/em> (I will defined what they are below) that is <em>closed under C-suprema<\/em> (for &#8220;suprema taken <strong>c<\/strong>omponentwise&#8221;), namely such that:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>for every <em>u<\/em> \u2208 <em>L<\/em>, for every family of elements (<em>v<sub>i<\/sub><\/em>)<sub><em>i<\/em> \u2208 <em>I<\/em><\/sub> with some supremum <em>v<\/em> in <em>L&#8217;<\/em>, such that each rectangle <em>u<\/em> \u2297 <em>v<sub>i<\/sub><\/em> is in <em>D<\/em>, then <em>u<\/em> \u2297 <em>v<\/em> is also in <em>D<\/em>, and<\/li>\n\n\n\n<li>for every <em>v<\/em> \u2208 <em>L&#8217;<\/em>, for every family of elements (<em>u<sub>i<\/sub><\/em>)<sub><em>i<\/em> \u2208 <em>I<\/em><\/sub> with some supremum <em>u<\/em> in <em>L<\/em>, such that each rectangle <em>u<sub>i<\/sub><\/em> \u2297 <em>v<\/em> is in <em>D<\/em>, then <em>u<\/em> \u2297 <em>v<\/em> is also in <em>D<\/em>.<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\">A rectangle <em>u<\/em> \u2297 <em>v<\/em> is really a Galois connection (see <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=6400\">this post<\/a>, for example; the definition of C-ideal was taken from there), but we do not need to know that.  It turns out that \u22a5 \u2297 <em>v<\/em> = <em>u<\/em> \u2297 \u22a5 is the least rectangle (much like the open rectangles \u2205 \u00d7 <em>V<\/em> and <em>U<\/em> \u00d7 \u2205 are both empty), but apart from that, <em>u<\/em> \u2297 <em>v<\/em> really behaves just like a pair of elements <em>u<\/em> in <em>L<\/em> (other than its bottom element \u22a5) and <em>v<\/em> in <em>L&#8217;<\/em> (other than its own bottom element, still written \u22a5).  In particular, when <em>u<\/em>, <em>u&#8217;<\/em>\u2260\u22a5 and <em>v<\/em>, <em>v&#8217;<\/em>\u2260\u22a5, we have <em>u<\/em> \u2297 <em>v<\/em> \u2264 <em>u&#8217;<\/em> \u2297 <em>v&#8217;<\/em> if and only if <em>u<\/em>\u2264<em>u&#8217;<\/em> and <em>v<\/em>\u2264<em>v&#8217;<\/em>.  Hence we really should read <em>u<\/em> \u2297 <em>v<\/em> as the pair of the two elements <em>u<\/em> and <em>v<\/em> if they are both different from \u22a5, and as being equal to \u22a5 otherwise (where I continue to use \u22a5 as a notation for the bottom element, this time in the collection of rectangles).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Let us notice that, for every <em>u<\/em>, <em>u<\/em> \u2297 _ preserves all suprema and finite infima.  We will use that observation later.  This is proved by looking at the case <em>u<\/em>=\u22a5, which is trivial since then <em>u<\/em> \u2297 _ is a constant function, and by looking at the case <em>u<\/em>\u2260\u22a5, where this follows from the fact that <em>u<\/em> \u2297 <em>v<\/em> \u2264 <em>u&#8217;<\/em> \u2297 <em>v&#8217;<\/em> if and only if <em>u<\/em>\u2264<em>u&#8217;<\/em> and <em>v<\/em>\u2264<em>v&#8217;<\/em>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">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 \u22a5 is in every C-ideal.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">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 <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>: 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.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">I will write <em>L<\/em> \u00d7<sub>loc<\/sub> <em>L&#8217;<\/em> for the collection of C-ideals on <em>L<\/em> and <em>L&#8217;<\/em>, ordered by inclusion.  This is (an isomorphic copy) of their product in <strong>Loc<\/strong>.  We have:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>first projection \u03c0<sub>1<\/sub> : <em>L<\/em> \u00d7<sub>loc<\/sub> <em>L&#8217;<\/em> \u2192 <em>L<\/em> (in <strong>Loc<\/strong>, so \u03c0<sub>1<\/sub> is a frame homomorphism from <em>L<\/em> to <em>L<\/em> \u00d7<sub>loc<\/sub> <em>L&#8217;<\/em>) maps every <em>u<\/em> in <em>L<\/em> to \u2193(<em>u<\/em> \u2297 \u22a4);<\/li>\n\n\n\n<li>similarly, second projection \u03c0<sub>2<\/sub> maps every <em>v<\/em> in <em>L&#8217;<\/em> to \u2193(\u22a4 \u2297 <em>v<\/em>);<\/li>\n\n\n\n<li>the pairing \u3008<em>f<\/em>, <em>g<\/em>\u3009 : <em>L&#8221;<\/em> \u2192 <em>L<\/em> \u00d7 <em>L&#8217;<\/em> of two locale morphisms <em>f<\/em> : <em>L&#8221;<\/em> \u2192 <em>L<\/em> and <em>g<\/em>: <em>L&#8221;<\/em> \u2192 <em>L&#8217;<\/em> in <strong>Loc<\/strong> (namely, of two frame homomorphisms <em>f<\/em> : <em>L<\/em> \u2192 <em>L&#8221;<\/em> and <em>g<\/em>: <em>L&#8217;<\/em> \u2192 <em>L&#8221;<\/em>) is the frame homomorphism from <em>L<\/em> \u00d7<sub>loc<\/sub> <em>L&#8217;<\/em> to <em>L&#8221;<\/em> that sends every C-ideal <em>D<\/em> to \u22c1 {<em>f<\/em>(<em>u<\/em>) \u22c0 <em>g<\/em>(<em>v<\/em>) | <em>u<\/em> \u2297 <em>v<\/em> \u2208 <em>D<\/em>};<\/li>\n\n\n\n<li>as a consequence, given any two locale morphisms <em>f<\/em> : <em>M<\/em> \u2192 <em>L<\/em> and <em>g<\/em> : <em>M&#8217;<\/em> \u2192 <em>L&#8217;<\/em>, their product <em>f<\/em> \u00d7<sub>loc<\/sub> <em>g<\/em>, namely \u3008<em>f<\/em> o \u03c0<sub>1<\/sub>, <em>g<\/em> o \u03c0<sub>2<\/sub>\u3009 : <em>M<\/em> \u00d7<sub>loc<\/sub> <em>M&#8217;<\/em> \u2192 <em>N<\/em> \u00d7<sub>loc<\/sub> <em>N&#8217;<\/em> (where composition is taken in <strong>Loc<\/strong>, hence works the other way around as in <strong>Frm<\/strong>) maps every C-ideal <em>D<\/em> on <em>N<\/em> and <em>N&#8217;<\/em> to the supremum of the C-ideals \u2193(<em>f<\/em>(<em>u<\/em>) \u2297 \u22a4) \u2229 \u2193(\u22a4 \u2297 <em>g<\/em>(<em>v<\/em>)) = \u2193(<em>f<\/em>(<em>u<\/em>) \u2297 <em>g<\/em>(<em>v<\/em>)), where <em>u<\/em> \u2297 <em>v<\/em> ranges over <em>D<\/em>.  This is just the union of those C-ideals, since that union is already closed under C-suprema; in other words, <em>f<\/em> \u00d7<sub>loc<\/sub> <em>g<\/em> maps <em>D<\/em> to \u2193{<em>f<\/em>(<em>u<\/em>) \u2297 <em>g<\/em>(<em>v<\/em>) | <em>u<\/em> \u2297 <em>v<\/em> \u2208 <em>D<\/em>}.<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\">For completeness, let me make explicit the terminal object in <strong>Loc<\/strong>:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>the terminal object in <strong>Loc<\/strong> is <strong>O1<\/strong>, where <strong>1<\/strong> is the terminal object in <strong>Top<\/strong>; namely, <strong>1<\/strong>\u225d{*}, with only two open subsets, \u2205 and <strong>1<\/strong>;<\/li>\n\n\n\n<li>the unique locale morphism !<em><sub>L<\/sub><\/em> : <em>L<\/em> \u2192 <strong>O1<\/strong> in <strong>Loc<\/strong> (namely, the unique frame homomorphism from <strong>O1<\/strong> to the frame <em>L<\/em>) maps the bottom element \u2205 of <strong>O1<\/strong> to the bottom element \u22a5 of <em>L<\/em> and the top element <strong>1<\/strong> of <strong>O1<\/strong> to the top element \u22a4 of <em>L<\/em>.<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\">Finally, let me transpose the notion of exponentials here.  Given three frames <em>L<\/em>, <em>L&#8217;<\/em> and \u03a9, if the exponential object <em>L<\/em><sup>\u03a9<\/sup> exists in <strong>Loc<\/strong>, then the locale morphisms from <em>L&#8217;<\/em> to <em>L<\/em><sup>\u03a9<\/sup> are in one-to-one-correspondence with those from <em>L&#8217;<\/em> \u00d7<sub>loc<\/sub> \u03a9 to <em>L<\/em>; in one direction, \u039b sends every locale morphism from <em>L&#8217;<\/em> \u00d7<sub>loc<\/sub> \u03a9 to <em>L<\/em> to one from <em>L&#8217;<\/em> to <em>L<\/em><sup>\u03a9<\/sup>, and its inverse sends any locale morphism <em>h<\/em> : <em>L&#8217;<\/em> \u2192 <em>L<\/em><sup>\u03a9<\/sup> to App o (<em>h<\/em> \u00d7<sub>loc<\/sub> id<sub>\u03a9<\/sub>) : <em>L&#8217;<\/em> \u00d7<sub>loc<\/sub> \u03a9 \u2192 <em>L<\/em>.  This is with any exponentiable object in any category with finite products, and can be checked by using the equations (\u03b2), (\u03b7) and (\u03c3).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">In other words, and writing [\u03a9<sub>1<\/sub> \u2192<sub>frm<\/sub> \u03a9<sub>2<\/sub>] for the poset of all frame homomorphisms from a frame \u03a9<sub>1<\/sub> to a frame \u03a9<sub>2<\/sub>, ordered by the pointwise ordering, \u039b is a bijection from [<em>L<\/em> \u2192<sub>frm<\/sub> <em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9] onto [<em>L<\/em><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <em>L&#8217;<\/em>].  We have more: \u039b 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 <em>L<\/em>=<strong>OS<\/strong> and <em>L&#8217;<\/em>=<strong>O1<\/strong>.  (I will introduce <strong>OS<\/strong> not too far away below.)<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Proposition A.<\/strong>  If the exponential object <em>L<\/em><sup>\u03a9<\/sup> exists in <strong>Loc<\/strong>, then for every frame <em>L&#8217;<\/em>, \u039b is an order-isomorphism from [<em>L<\/em> \u2192<sub>frm<\/sub> <em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9] onto [<em>L<\/em><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <em>L&#8217;<\/em>].<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Proof.<\/em>  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 (_ \u00d7<sub>loc<\/sub> id<sub>\u03a9<\/sub>) of \u039b is monotonic, and is pretty immediate.  The remaining five steps will be devoted to showing that \u039b itself is monotonic.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Step 1: the inverse of \u039b is monotonic.<\/em> <strong>Frm<\/strong> is enriched over the category <strong>Pos<\/strong> of posets and monotonic maps.  In other words, every hom-set [\u03a9<sub>1<\/sub> \u2192<sub>frm<\/sub> \u03a9<sub>2<\/sub>] is ordered, and composition is monotonic in both morphisms being composed.  Looking at the explicit description of products <em>f<\/em> \u00d7<sub>loc<\/sub> <em>g<\/em> in <strong>Loc<\/strong> given above, we see that the product operation \u00d7<sub>loc<\/sub> on morphisms is also monotonic.  Hence the inverse of \u039b, which maps <em>h<\/em> to App o (<em>h<\/em> \u00d7<sub>loc<\/sub> id<sub>\u03a9<\/sub>) (with composition taken in <strong>Loc<\/strong>), is monotonic.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Step 2: \u039b is monotonic, basic ideas.<\/em>  In order to show that \u039b is monotonic, we will need to use Sierpi\u0144ski space <strong>S<\/strong>.  The space <strong>S<\/strong> is the two-element space {0, 1}, ordered by 0&lt;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 <strong>Top<\/strong>.  Imagine we have two continuous maps <em>f<\/em> and <em>g<\/em> from a space <em>X<\/em> \u00d7 <em>Y<\/em> to a space <em>Z<\/em>, with <em>f<\/em>\u2264<em>g<\/em>.  In order to show that \u039b(<em><em>f<\/em><\/em>) \u2264 \u039b(<em>g<\/em>) without knowing how \u039b operates, we would define a continuous map <em>h<\/em> : <strong>S<\/strong> \u00d7 (<em>X<\/em> \u00d7 <em>Y<\/em>) \u2192 <em>Z<\/em> by <em>h<\/em>(0,<em>c<\/em>)\u225d<em>f<\/em>(<em>c<\/em>) and <em>h<\/em>(1,<em>c<\/em>)\u225d<em>g<\/em>(<em>c<\/em>) for every <em>c<\/em> in <em>X<\/em> \u00d7 <em>Y<\/em>; in this way, <em>h<\/em> o \u3008false o !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>, id<sub><em>X<\/em><\/sub> <sub>\u00d7 <em>Y<\/em><\/sub>\u3009 = <em>f<\/em> and <em>h<\/em> o \u3008true o !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>, id<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>\u3009 = <em>g<\/em>, where true : <strong>1<\/strong> \u2192 <strong>S<\/strong> is the constant map with value 1, false : <strong>1<\/strong> \u2192 <strong>S<\/strong> is the constant map with value  0, and !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub> is the unique map from <em><em>X <\/em>\u00d7 <em>Y<\/em><\/em> to <strong>1<\/strong>.  Then, using Equation (\u03c3), we realize that \u039b(<em><em>f<\/em><\/em>) = \u039b(<em>h<\/em> o \u3008false o !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>, id<sub><em>X<\/em><\/sub> <sub>\u00d7 <em>Y<\/em><\/sub>\u3009) must be equal to \u039b(<em>h<\/em>) o false o !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>, and similarly that \u039b(<em><em>g<\/em><\/em>) = \u039b(<em>h<\/em>) o true o !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>.  Since false\u2264true and composition is monotonic, this entails the desired inequality \u039b(<em><em>f<\/em><\/em>) \u2264 \u039b(<em>g<\/em>).  We adapt this argument to the case of locales right away.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Step 3: true, false, and the analogue of h.<\/em>  The role of the two maps true and false will be played by their localic analogues True\u225d<strong>O<\/strong>(true) and False\u225d<strong>O<\/strong>(false).  As morphisms in <strong>Loc<\/strong>, they go from <strong>O1<\/strong> to <strong>OS<\/strong>, hence they are frame homomorphisms from <strong>OS<\/strong> to <strong>O1<\/strong>.  There are three elements in <strong>OS<\/strong>, which are \u2205, {1}, and <strong>S<\/strong>.  Any frame homomorphism from <strong>OS<\/strong> to <strong>O1<\/strong> must map \u2205 to \u2205 and <strong>S<\/strong> to <strong>1<\/strong>.  Additionally, True maps {1} to <strong>1<\/strong>, and False maps {1} to \u2205.  Let us notice that, similarly to the fact that false\u2264true, we have False\u2264True.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Defining the analogue of <em>h<\/em> is slightly trickier.  Let us look back at how we defined <em>h<\/em> above.   For every open subset <em>V<\/em> of <em>Y<\/em>, <em>h<\/em><sup>\u20131<\/sup>(<em>V<\/em>) is equal to (<strong>S<\/strong> \u00d7 <em>f<\/em><sup>\u20131<\/sup>(<em>V<\/em>)) \u222a ({1} \u00d7 <em>g<\/em><sup>\u20131<\/sup>(<em>V<\/em>)), using the fact that <em>f<\/em>\u2264<em>g<\/em>.  Analogously, we assume two locale morphisms <em>F<\/em>, <em>G<\/em> : <em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9 \u2192 <em>L<\/em> with <em>F<\/em>\u2264<em>G<\/em> (as elements of [<em>L<\/em> \u2192<sub>frm<\/sub> <em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9]), and we define <em>H<\/em> : <strong>OS<\/strong> \u00d7<sub>loc<\/sub> (<em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9) \u2192 <em>L<\/em>, namely as a frame homomorphism from <em>L<\/em> to <strong>OS<\/strong> \u00d7<sub>loc<\/sub> (<em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9) by:<\/p>\n\n\n\n<p class=\"has-text-align-center wp-block-paragraph\">For every <em>v<\/em> in <em>L<\/em>, <em>H<\/em>(<em>v<\/em>) \u225d \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), {1} \u2297 <em>G<\/em>(<em>v<\/em>)}.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Step 4: H(v) is well-defined for every v.<\/em>   We check that \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), {1} \u2297 <em>G<\/em>(<em>v<\/em>)} is a C-ideal.  Crucially, this requires <em>F<\/em>(<em>v<\/em>)\u2264<em>G<\/em>(<em>v<\/em>), a fact that we will use near the end of the argument.<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>Let us assume a family of open rectangles <em>a<sub>i<\/sub><\/em> \u2297 <em>b<\/em>, where some of them are below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>) (say, those such that <em>i<\/em> ranges over a subset <em>I<\/em> of the indices), and the others (say, where <em>i<\/em> ranges over the complement <em>J<\/em> of <em>I<\/em>) are below {1} \u2297 <em>G<\/em>(<em>v<\/em>).  For the purposes of taking suprema, the open rectangles equal to \u22a5 play no role, so we may as well assume that <em>a<sub>i<\/sub><\/em>\u2260\u22a5 for every index <em>i<\/em>, and that <em>b<\/em>\u2260\u22a5.<br>If <em>I<\/em> is empty, then sup<em><sub>i<\/sub><\/em> (<em>a<sub>i<\/sub><\/em> \u2297 <em>b<\/em>), where <em>i<\/em> ranges over all indices, is a supremum of rectangles all below {1} \u2297 <em>G<\/em>(<em>v<\/em>), hence is below {1} \u2297 <em>G<\/em>(<em>v<\/em>) as well.  If <em>I<\/em> is non-empty, then we pick some <em>i<\/em> in <em>I<\/em>, and from <em>a<sub>i<\/sub><\/em> \u2297 <em>b<\/em> \u2264 <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>) (and the fact that <em>a<sub>i<\/sub><\/em>\u2260\u22a5), we deduce that <em>b<\/em> \u2264 <em>F<\/em>(<em>v<\/em>).  Hence we are taking a supremum of rectangles that are all below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), whether <em>i<\/em> is in <em>I<\/em> or in <em>J<\/em> \u2014 the point is that the rectangles <em>a<sub>i<\/sub><\/em> \u2297 <em>b<\/em> with <em>i<\/em> in <em>J<\/em> still have the same second component <em>b<\/em>, and <em>b<\/em> \u2264 <em>F<\/em>(<em>v<\/em>).<\/li>\n\n\n\n<li>Let us assume a family of open rectangles <em>a<\/em> \u2297 <em>b<sub>i<\/sub><\/em>, some below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>) (as before, when <em>i<\/em> is in some set <em>I<\/em> of indices), some below {1} \u2297 <em>G<\/em>(<em>v<\/em>) (where <em>i<\/em> ranges over a disjoint set <em>J<\/em>).  As above, we assume that neither <em>a<\/em> nor any <em>b<sub>i<\/sub><\/em> is equal to \u22a5.  If <em>J<\/em> is empty, then sup<em><sub>i<\/sub><\/em> (<em>a<sub>i<\/sub><\/em> \u2297 <em>b<\/em>) is a supremum of elements all below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), hence is itself below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>).  Otherwise, we pick a <em>j<\/em> in <em>J<\/em>, and from <em>a<\/em> \u2297 <em>b<sub>j<\/sub><\/em> \u2264 {1} \u2297 <em>G<\/em>(<em>v<\/em>) we obtain that <em>a<\/em> \u2264 {1}.  It follows that for every <em>i<\/em> in <em>I<\/em>, <em>a<\/em> \u2297 <em>b<sub>i<\/sub><\/em> is not only below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), but even below {1} \u2297 <em>F<\/em>(<em>v<\/em>).  Since <em>F<\/em>(<em>v<\/em>) \u2264 <em>G<\/em>(<em>v<\/em>), it is below {1} \u2297 <em>G<\/em>(<em>v<\/em>).  The rectangles <em>a<\/em> \u2297 <em>b<sub>i<\/sub><\/em> with <em>i<\/em> in <em>J<\/em> are also below {1} \u2297 <em>G<\/em>(<em>v<\/em>), by assumption, so sup<em><sub>i<\/sub><\/em> (<em>a<sub>i<\/sub><\/em> \u2297 <em>b<\/em>) \u2264 {1} \u2297 <em>G<\/em>(<em>v<\/em>).<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Step 5: H is a frame homomorphism.<\/em>  <em>H<\/em>(<em>v<\/em>) is simply the supremum of \u2193(<strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>)) and of \u2193({1} \u2297 <em>G<\/em>(<em>v<\/em>)); since <em>F<\/em> and <em>G<\/em> preserve all suprema, and since <strong>S<\/strong> \u2297 _ and {1} \u2297 _ do, too, <em>H<\/em> preserves all suprema.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>H<\/em> maps \u22a4 to \u2193{<strong>S<\/strong> \u2297 \u22a4, {1} \u2297 \u22a4} = \u2193(<strong>S<\/strong> \u2297 \u22a4), which is the top element of <strong>OS<\/strong> \u00d7<sub>loc<\/sub> (<em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">In order to show that <em>H<\/em> is a frame homomorphism, it remains to show that <em>H<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>) = <em>H<\/em>(<em>v<\/em>) \u22c0 <em>H<\/em>(<em>w<\/em>), for all <em>v<\/em>, <em>w<\/em> in <em><em>L&#8217;<\/em><\/em> \u00d7<sub>loc<\/sub> \u03a9.  Since <em>H<\/em> preserves suprema, it is monotonic, so <em>H<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>) \u2264 <em>H<\/em>(<em>v<\/em>) \u22c0 <em>H<\/em>(<em>w<\/em>).  We therefore concentrate on the reverse inequality.  <em>H<\/em>(<em>v<\/em>) \u22c0 <em>H<\/em>(<em>w<\/em>) is the intersection of \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), {1} \u2297 <em>G<\/em>(<em>v<\/em>)} and of \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em>w<\/em>), {1} \u2297 <em>G<\/em>(<em>w<\/em>)}.  We consider any rectangle in that intersection, and we need to show that it is in <em>H<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>) = \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em><em>v<\/em><\/em> \u22c0 <em><em>w<\/em><\/em>), {1} \u2297 <em>G<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>)}:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>any rectangle below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>) and <strong>S<\/strong> \u2297 <em>F<\/em>(<em>w<\/em>) is below their infimum, which is <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>), since <em>F<\/em> and <strong>S<\/strong> \u2297 _ both preserve binary infima;<\/li>\n\n\n\n<li>any rectangle below {1} \u2297 <em>G<\/em>(<em>v<\/em>) and below {1} \u2297 <em>G<\/em>(<em>w<\/em>) will similarly be below {1} \u2297 <em>G<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>);<\/li>\n\n\n\n<li>any rectangle <em>a<\/em> \u2297 <em>b<\/em> below <strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>) and {1} \u2297 <em>G<\/em>(<em>w<\/em>) must be such that <em>a<\/em>\u2264{1} and <em>b<\/em>\u2264<em>F<\/em>(<em>v<\/em>); then <em>b<\/em>\u2264<em>G<\/em>(<em>v<\/em>) since <em>F<\/em>\u2264<em>G<\/em>, so <em>a<\/em> \u2297 <em>b<\/em> is below {1} \u2297 <em>G<\/em>(<em>v<\/em>); since it is below {1} \u2297 <em>G<\/em>(<em>w<\/em>) by assumption, it is also below their infimum, which is {1} \u2297 <em>G<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>);<\/li>\n\n\n\n<li>any rectangle <em>a<\/em> \u2297 <em>b<\/em> below {1} \u2297 <em>G<\/em>(<em>v<\/em>) and <strong>S<\/strong> \u2297 <em>F<\/em>(<em>w<\/em>) must be below {1} \u2297 <em>G<\/em>(<em>v<\/em> \u22c0 <em>w<\/em>), by the same argument.<\/li>\n<\/ul>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Step 6: replaying the topological argument in <strong>Loc<\/strong>.<\/em>  In step 2, I had argued that <em>h<\/em> o \u3008false o !<sub><em><sub><em>X <\/em>\u00d7 <em>Y<\/em><\/sub><\/em><\/sub>, id<sub><em>X<\/em><\/sub> <sub>\u00d7 <em>Y<\/em><\/sub>\u3009 = <em>f<\/em>.  Similarly, let us show that <em>H<\/em> o \u3008False o !<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub>, id<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub>\u3009 = <em>F<\/em>, where composition is in <strong>Loc<\/strong> (hence works the other way around as in <strong>Frm<\/strong>, as usual).  We compute the image of an arbitrary element <em>v<\/em> of <em>L<\/em> under the map on the left hand side.  We first apply <em>H<\/em> (composition is the other way around in <strong>Frm<\/strong>!), and we obtain \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), {1} \u2297 <em>G<\/em>(<em>v<\/em>)}.  Next, we apply a pairing \u3008<em>A<\/em>, <em>B<\/em>\u3009 of two frame homomorphisms <em>A<\/em> \u225d False o !<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub> and <em>B<\/em> \u225d id<sub><em><sub><em>L&#8217;<\/em><\/sub><\/em><sub> \u00d7loc \u03a9<\/sub><\/sub>, and this gives us (<em>A<\/em>(<strong>S<\/strong>) \u22c0 <em>B<\/em>(<em>F<\/em>(<em>v<\/em>))) \u22c1 (<em>A<\/em>({1}) \u22c0 <em>B<\/em>(<em>G<\/em>(<em>v<\/em>))).  Since <em>B<\/em> is the identity map, this simplifies to (<em>A<\/em>(<strong>S<\/strong>) \u22c0 <em>F<\/em>(<em>v<\/em>)) \u22c1 (<em>A<\/em>({1}) \u22c0 <em>G<\/em>(<em>v<\/em>)).  Since <em>A<\/em> is a frame homorphism, <em>A<\/em>(<strong>S<\/strong>) = \u22a4.  Since False ({1}) = \u2205, and !<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub> is a frame homomorphism, <em>A<\/em>({1}) = \u22a5.  Therefore (<em>A<\/em>(<strong>S<\/strong>) \u22c0 <em>F<\/em>(<em>v<\/em>)) \u22c1 (<em>A<\/em>({1}) \u22c0 <em>G<\/em>(<em>v<\/em>)) = (\u22a4 \u22c0 <em>F<\/em>(<em>v<\/em>)) \u22c1 \u22a5 = <em>F<\/em>(<em>v<\/em>).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">We show that <em>H<\/em> o \u3008True o !<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub>, id<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub>\u3009 = <em>G<\/em> in a similar way.  Explicitly (but in brief!), <em>v<\/em> is now first mapped by <em>H<\/em> to \u2193{<strong>S<\/strong> \u2297 <em>F<\/em>(<em>v<\/em>), {1} \u2297 <em>G<\/em>(<em>v<\/em>)}, as above, and we apply a pairing \u3008<em>A<\/em>, <em>B<\/em>\u3009 to that where now <em>A<\/em> \u225d True o !<sub><em><sub><em><em><em>L&#8217;<\/em><\/em><\/em><\/sub><\/em><sub> \u00d7<sub>loc<\/sub> \u03a9<\/sub><\/sub> (and <em>B<\/em> is id<sub><em><sub><em>L&#8217;<\/em><\/sub><\/em><sub> \u00d7loc \u03a9<\/sub><\/sub>, unchanged from above).  This produces (<em>A<\/em>(<strong>S<\/strong>) \u22c0 <em>F<\/em>(<em>v<\/em>)) \u22c1 (<em>A<\/em>({1}) \u22c0 <em>G<\/em>(<em>v<\/em>)), and <em>A<\/em>(<strong>S<\/strong>) = \u22a4, as above, but now <em>A<\/em>({1}) = \u22a4; so (<em>A<\/em>(<strong>S<\/strong>) \u22c0 <em>F<\/em>(<em>v<\/em>)) \u22c1 (<em>A<\/em>({1}) \u22c0 <em>G<\/em>(<em>v<\/em>)) = <em>F<\/em>(<em>v<\/em>)) \u22c1 <em>G<\/em>(<em>v<\/em>), which is equal to <em>G<\/em>(<em>v<\/em>), since <em>F<\/em>\u2264<em>G<\/em>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">We are almost finished.  Using Equation (\u03c3), \u039b(<em>F<\/em>) = \u039b(<em>H<\/em> o \u3008False o !<sub><em><sub><em>L&#8217;<\/em><\/sub><\/em><sub> \u00d7loc \u03a9<\/sub><\/sub>, id<sub><em><sub><em>L&#8217;<\/em><\/sub><\/em><sub> \u00d7loc \u03a9<\/sub><\/sub>\u3009) is equal to \u039b(<em>H<\/em>) o False o !<sub><em><sub><em>L&#8217;<\/em><\/sub><\/em><sub> \u00d7loc \u03a9<\/sub><\/sub>, and similarly \u039b(<em><em>G<\/em><\/em>) = \u039b(<em>H<\/em>) o True o !<sub><em><sub><em>L&#8217;<\/em><\/sub><\/em><sub> \u00d7loc \u03a9<\/sub><\/sub>. Since False\u2264True and composition is monotonic, it follows that \u039b(<em><em>F<\/em><\/em>) \u2264 \u039b(<em>G<\/em>).  \u2610<\/p>\n\n\n\n<h2 class=\"wp-block-heading\"><strong>pt<\/strong>(<strong>OS<\/strong><sup>\u03a9<\/sup>) \u2245 \u03a9<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">In order to show that the exponentiable topological spaces are the core-compact spaces, the usual proof of the exponential \u21d2 core-compact direction consists in observing that if <em>X<\/em> is an exponentiable topological space, then <em>Y<sup>X<\/sup><\/em> exists for every space <em>Y<\/em>, and in particular for Sierpi\u0144ski space <strong>S<\/strong>.  Next, <strong>S<\/strong><em><sup>X<\/sup><\/em> must be the space of all continuous maps from <em>X<\/em> to <strong>S<\/strong>, with some topology, and that is exactly the set of characteristic functions of open subsets of <em>X<\/em>.  This is exactly the observation that Hyland makes in the localic context: the role of <strong>S<\/strong> is played by its associated locale <strong>OS<\/strong> (of open subsets of <strong>S<\/strong>, namely \u2205, {1}, and {0,1}), and then, for every exponentiable frame \u03a9, the points of <strong><strong>OS<\/strong><\/strong><sup>\u03a9<\/sup> are in one-to-one correspondence with the elements of \u03a9.  This is even an order-isomorphism; we will show this below, as a consequence of Proposition A.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">For any frame <em>L<\/em>, a <em>point<\/em> of <em>L<\/em> is a completely prime filter of <em>L<\/em>, and <strong>pt<\/strong>(<em>L<\/em>) denotes the set of all points of <em>L<\/em>.  It is customary to equip <strong>pt<\/strong>(<em>L<\/em>) with the topology whose open sets are <em>O<sub>u<\/sub><\/em> \u225d {<em>x<\/em> \u2208 <strong>pt<\/strong>(<em>L<\/em>) | <em>u<\/em> \u2208 <em>x<\/em>}, where <em>u<\/em> ranges over <em>L<\/em>.  For now, we will consider <strong>pt<\/strong>(<em>L<\/em>) 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 <em>x<\/em> and <em>y<\/em> of <em>L<\/em>, <em>x<\/em> is below <em>y<\/em> in the specialization ordering if and only if for every <em>u<\/em> \u2208 <em>L<\/em>, <em>x<\/em> \u2208 <em>O<sub>u<\/sub><\/em> implies <em>y<\/em> \u2208 <em>O<sub>u<\/sub><\/em>, if and only if every <em>u<\/em> \u2208 <em>x<\/em> is in <em>y<\/em>, if and only if <em>x<\/em> \u2286 <em>y<\/em>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Proposition B.<\/strong>  For every exponentiable frame \u03a9, there is a string of order-isomorphisms <strong>pt<\/strong>(<strong>OS<\/strong><sup>\u03a9<\/sup>) \u2245 [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] \u2245 [<strong>OS<\/strong> \u2192<sub>frm<\/sub> <strong>O1<\/strong> \u00d7<sub>loc<\/sub> \u03a9] \u2245 [<strong>OS<\/strong> \u2192<sub>frm<\/sub> \u03a9] \u2245 \u03a9.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Proof.<\/em>  The first order-isomorphism can be written more generally as <strong>pt<\/strong>(<em>L<\/em>) \u2245 [<em>L<\/em> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], for any frame <em>L<\/em>.  Any point <em>x<\/em> of <em>L<\/em> determines a frame homomorphism \u03c7<em><sub>x<\/sub><\/em> from <em>L<\/em> to <strong>O1<\/strong>, which maps every <em>u<\/em> in <em>L<\/em> to <strong>1<\/strong> if <em>u<\/em> is in <em>x<\/em>, to \u2205 otherwise.  (\u03c7<em><sub>x<\/sub><\/em> is the characteristic map of <em>x<\/em>.)  That is a frame homomorphism: it preserves finite infima because <em>x<\/em> is a filter, and it preserves arbitrary suprema because <em>x<\/em> is completely prime.  Conversely, any frame homomorphism \u03c6 from <em>L<\/em> to <strong>O1<\/strong> determines a completely prime filter \u03c6<sup>\u20131<\/sup>(<strong>1<\/strong>): it is a filter because \u03c6 preserves finite infima, and it is completely prime because \u03c6 preserves arbitrary suprema.  It is then easy to see that the operations \u03c6 \u21a6 \u03c6<sup>\u20131<\/sup>(<strong>1<\/strong>) and <em>x<\/em> \u21a6 \u03c7<em><sub>x<\/sub><\/em> are inverse of each other, and are monotonic.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The second isomorphism [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] \u2245 [<strong>OS<\/strong> \u2192<sub>frm<\/sub> <strong>O1<\/strong> \u00d7<sub>loc<\/sub> \u03a9] is an order-isomorphism between the poset of all locale morphisms from <strong>O1<\/strong> to <strong>OS<\/strong><sup>\u03a9<\/sup> and the poset of all locale morphisms from <strong>O1<\/strong> \u00d7<sub>loc<\/sub> \u03a9 to <strong>OS<\/strong>, and it is given by Proposition A.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The third isomorphism comes from the fact that, since <strong>O1<\/strong> is a terminal object in <strong>Loc<\/strong>, <strong>O1<\/strong> \u00d7<sub>loc<\/sub> \u03a9 is isomorphic (in <strong>Loc<\/strong>) to \u03a9.  Explicity, the isomorphism is second projection from <strong>O1<\/strong> \u00d7<sub>loc<\/sub> \u03a9 to \u03a9 in one direction, and \u3008!<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009 in the other direction.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The fourth isomorphism [<strong>OS<\/strong> \u2192<sub>frm<\/sub> \u03a9] \u2245 \u03a9 is the following.  Given any frame homomorphism \u03c6 from <strong>OS<\/strong> to \u03a9, \u03c6({1}) is an element of \u03a9.  Conversely, given any element <em>u<\/em> of \u03a9, let \u03c6<em><sub>u<\/sub><\/em> map {1} to <em>u<\/em>, bottom to bottom and top to top.  This is a frame homomorphism, and the only one such that \u03c6<em><sub>u<\/sub><\/em>=\u03c6, if <em>u<\/em>=\u03c6({1}).  Explicitly, the composition of \u03c6 \u21a6 <em>u<\/em>\u225d\u03c6({1}) \u21a6 \u03c6<em><sub>u<\/sub><\/em> is the identity map; conversely, <em>u<\/em> \u21a6 \u03c6<em><sub>u<\/sub><\/em> \u21a6 \u03c6<em><sub>u<\/sub><\/em>({1}) is also the identity map.  Also, the map <em>u<\/em> \u21a6 \u03c6<em><sub>u<\/sub><\/em> is clearly monotonic, and so is the map \u03c6 \u21a6 <em>u<\/em>\u225d\u03c6({1}).  \u2610<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Every exponentiable locale \u03a9 is a continuous dcpo<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">We can now prove that, if \u03a9 is exponentiable in <strong>Loc<\/strong>, or in fact just if <strong>OS<\/strong><sup>\u03a9<\/sup> exists in <strong>Loc<\/strong>, then \u03a9 must be a continuous dcpo.  I will follow M. Hyland&#8217;s proof [1, Proposition 2, pages 267\u2013280].  The argument matches the proof that every exponential topological space must be core-compact (Proposition 5.3.3 in the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>) rather closely, up to some transposition to the case of locales.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">We will use the order-isomorphisms given in Proposition B a lot.  Since \u03a9 is a frame, hence a dcpo, so is <strong>pt<\/strong>(<strong>OS<\/strong><sup>\u03a9<\/sup>) \u2245 [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>].<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">We may also check this directly; for now, let us take this as a cross-check.  Given any directed family (\u03c6<em><sub>i<\/sub><\/em>)<sub><em>i<\/em> \u2208 <em>I<\/em><\/sub> of frame homomorphisms from <strong>OS<\/strong><sup>\u03a9<\/sup> to <strong>O1<\/strong>, its supremum \u03c6 is computed pointwise.  In order to see this, we let \u03c6 be the pointwise supremum of the family, and we check that it is a frame homomorphism.  It clearly preserves all suprema, since every \u03c6<em><sub>i<\/sub><\/em> does.  The map \u03c6 sends top to top because each \u03c6<em><sub>i<\/sub><\/em> does (and <em>I<\/em> is non-empty).  The fact that \u03c6 preserves binary infima depends on the fact that we are working in a poset of frame homomorphisms whose codomain is <strong>O1<\/strong>. For all <em>u<\/em>, <em>v<\/em> in <strong>OS<\/strong><sup>\u03a9<\/sup>, in order to show that \u03c6(<em>u<\/em> \u22c0 <em>v<\/em>) = \u03c6(<em>u<\/em>) \u22c0 \u03c6(<em>v<\/em>), it suffices to show that \u03c6(<em>u<\/em>) \u22c0 \u03c6(<em>v<\/em>) \u2264 \u03c6(<em>u<\/em> \u22c0 <em>v<\/em>), since the reverse inequality follows from monotonicity; and in order to show that, it suffices to show that if \u03c6(<em>u<\/em>) \u22c0 \u03c6(<em>v<\/em>)=<strong>1<\/strong>, namely if both \u03c6(<em>u<\/em>) and \u03c6(<em>v<\/em>) are equal to <strong>1<\/strong>, then \u03c6(<em>u<\/em> \u22c0 <em>v<\/em>)=<strong>1<\/strong>.  Since \u03c6(<em>u<\/em>)=<strong>1<\/strong>, \u03c6<em><sub>i<\/sub><\/em>(<em>u<\/em>)=<strong>1<\/strong> for some <em>i<\/em> in <em>I<\/em> (otherwise, \u03c6<em><sub>i<\/sub><\/em>(<em>u<\/em>) would be equal to the bottom element \u2205 for every <em>i<\/em>, hence so would be the supremum \u03c6(<em>u<\/em>)).  Similarly, \u03c6<em><sub>i<\/sub><\/em>(<em>v<\/em>)=<strong>1<\/strong> for some <em>i<\/em> in <em>I<\/em>, and we can take the same <em>i<\/em> for both <em>u<\/em> and <em>v<\/em>, by directedness.  Then \u03c6<em><sub>i<\/sub><\/em>(<em>u<\/em> \u22c0 <em>v<\/em>) = \u03c6<em><sub>i<\/sub><\/em>(<em>u<\/em>) \u22c0 \u03c6<em><sub>i<\/sub><\/em>(<em>v<\/em>) = <strong>1<\/strong>, so \u03c6(<em>u<\/em>) \u22c0 \u03c6(<em>v<\/em>) = <strong>1<\/strong>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The point of doing this check is the following (the same would hold for [<em>L<\/em> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], for any frame <em>L<\/em>).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Lemma.<\/strong>  Directed suprema in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] are computed pointwise.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Given any element <em>d<\/em> of <strong>OS<\/strong><sup>\u03a9<\/sup>, we form the set <em>O<sub>d<\/sub><\/em> \u225d {\u03c6 \u2208 [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] | \u03c6(<em>d<\/em>)=<strong>1<\/strong>}.  Such sets are exactly the open subsets of <strong>pt<\/strong>(<strong>OS<\/strong><sup>\u03a9<\/sup>), taken in the isomorphic copy [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>].<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">The following is the analogue of the fact that, if <em>X<\/em> is an exponentiable topological space, then the Scott topology in [<em>X<\/em> \u2192 <strong>S<\/strong>] (\u2245 <strong>O<\/strong><em>X<\/em>) is finer than the exponential topology on [<em>X<\/em> \u2192 <strong>S<\/strong>], which is one of the steps in the proof of Proposition 5.3.3 in the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a> (fourth paragraph, to be precise).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Proposition C.<\/strong>  For every exponentiable frame \u03a9, for every element <em>d<\/em> of <strong>OS<\/strong><sup>\u03a9<\/sup>, <em>O<sub>d<\/sub><\/em> is a Scott-open subset of [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>].<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Proof.<\/em>  We first check that <em>O<sub>d<\/sub><\/em> is upwards closed: if \u03c6\u2264\u03c6&#8217;, and if \u03c6(<em>d<\/em>)=<strong>1<\/strong> then certainly \u03c6'(<em>d<\/em>)=<strong>1<\/strong>.  Next, let us consider a directed family (\u03c6<em><sub>i<\/sub><\/em>)<sub><em>i<\/em> \u2208 <em>I<\/em><\/sub> in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], with (pointwise) supremum \u03c6 in <em>O<sub>d<\/sub><\/em>.  That \u03c6 is in <em>O<sub>d<\/sub><\/em> means that \u03c6(<em>d<\/em>)=<strong>1<\/strong>.  Since suprema are computed pointwise, \u03c6(<em>d<\/em>) = sup<sub><em>i<\/em> \u2208 <em>I<\/em><\/sub> \u03c6<em><sub>i<\/sub><\/em>(<em>d<\/em>), so \u03c6<em><sub>i<\/sub><\/em>(<em>d<\/em>)=<strong>1<\/strong> for some <em>i<\/em> in <em>I<\/em>; and therefore \u03c6<em><sub>i<\/sub><\/em> is in <em>O<sub>d<\/sub><\/em>.  \u2610<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">In order to go any further, we need to use the isomorphism between [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] and \u03a9.  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 <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>; there, we used the specific form of App : [<em>X<\/em> \u2192 <strong>S<\/strong>] \u00d7 <em>X<\/em> \u2192 <strong>S<\/strong>, or equivalently of the set (\u220b) of all pairs (<em>U<\/em>, <em>x<\/em>) of an open subset <em>U<\/em> of <em>X<\/em> and of a point <em>x<\/em> of <em>X<\/em> such that <em>x<\/em> \u2208 <em>U<\/em>, as a union of open rectangles.  In our case, we will use the fact that App({1}) (the application of App : <strong>OS<\/strong><sup>\u03a9<\/sup> \u00d7<sub>loc<\/sub> \u03a9 \u2192 <strong>OS<\/strong>, namely of the frame homomorphism App from <strong>OS<\/strong> to <strong>OS<\/strong><sup>\u03a9<\/sup> \u00d7<sub>loc<\/sub> \u03a9, to the element {1} of <strong>OS<\/strong>) is a C-ideal.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Let us name the isomorphism between [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] and \u03a9, first.  In one direction, it maps every element \u03c6 of [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] to some element of \u03a9, which I will write as <em>u<\/em><sub>\u03c6<\/sub>.  In the other direction, it maps every element <em>u<\/em> of \u03a9 to some frame homomorphism from <strong>OS<\/strong><sup>\u03a9<\/sup> to <strong>O1<\/strong>, which I will write as   \u03c6<em><sub>u<\/sub><\/em>.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">We make the map \u03c6 \u21a6 <em>u<\/em><sub>\u03c6<\/sub> explicit, looking at the constructions we used in Proposition B.  That is formed by looking at the composition App o (\u03c6 \u00d7<sub>loc<\/sub> id<sub>\u03a9<\/sub>) o \u3008!<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009 : \u03a9 \u2192 <strong>OS<\/strong> (in <strong>Loc<\/strong>\u2014that is a frame homomorphism the other way around, from <strong>OS<\/strong> to \u03a9), and applying it (as a frame homomorphism) to {1}.  We can simplify (\u03c6 \u00d7<sub>loc<\/sub> id<sub>\u03a9<\/sub>) o \u3008!<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009 as \u3008\u03c6 o !<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009, and therefore <em>u<\/em><sub>\u03c6<\/sub> = (App o \u3008\u03c6 o !<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009) ({1}).  The application to {1} is ordinary function application, but the composition inside the parenthesis is in <strong>Loc<\/strong>, 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 <em>u<\/em><sub>\u03c6<\/sub> is obtained by first computing App({1}), and then applying \u3008\u03c6 o !<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009 to it.  Explicitly, we obtain the following explicit formula.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Fact D.<\/strong>  For every \u03c6 in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], <em>u<\/em><sub>\u03c6<\/sub> = \u22c1{<em>v<\/em> \u2208 \u03a9 | \u2203<em>d&#8217;<\/em> \u2208 <strong>OS<\/strong><sup>\u03a9<\/sup>, \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong> and <em>d&#8217;<\/em> \u2297 <em>v<\/em> \u2208 App({1})}.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Indeed, computing the application of \u3008\u03c6 o !<sub>\u03a9<\/sub>, id<sub>\u03a9<\/sub>\u3009 to App({1}), we obtain \u22c1{!<sub>\u03a9<\/sub>(\u03c6(<em>d&#8217;<\/em>)) \u22c0 <em>v<\/em> | <em>d&#8217;<\/em> \u2297 <em>v<\/em> \u2208 App({1})}.  When \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong>, !<sub>\u03a9<\/sub>(\u03c6(<em>d&#8217;<\/em>))=\u22a4, so !<sub>\u03a9<\/sub>(\u03c6(<em>d&#8217;<\/em>)) \u22c0 <em>v<\/em> = <em>v<\/em>, while if \u03c6(<em>d&#8217;<\/em>)=\u2205, we have !<sub>\u03a9<\/sub>(\u03c6(<em>d&#8217;<\/em>))=\u22a5, so !<sub>\u03a9<\/sub>(\u03c6(<em>d&#8217;<\/em>)) \u22c0 <em>v<\/em> = \u22a5, which does not play any r\u00f4le in the computation of the supremum.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Now App({1}) is a C-ideal, in <strong>OS<\/strong><sup>\u03a9<\/sup> \u00d7<sub>loc<\/sub> \u03a9.  For every <em>d<\/em> \u2208 <strong>OS<\/strong><sup>\u03a9<\/sup>, there is collection \u03a9<em><sub>d<\/sub><\/em> \u225d {<em>v<\/em> \u2208 \u03a9 | <em>d<\/em> \u2297 <em>v<\/em> \u2208 App({1})}, and if we call <em>v<sub>d<\/sub><\/em> its supremum in \u03a9, then we see that <em>v<sub>d<\/sub><\/em> is in \u03a9<em><sub>d<\/sub><\/em>: indeed, <em>d<\/em> \u2297 <em>v<sub>d<\/sub><\/em> is the supremum of all the elements of the form <em>d<\/em> \u2297 <em>v<\/em> \u2208 App({1}) (with <em>d<\/em> fixed), because <em>d<\/em> \u2297 _ commutes with arbitrary suprema; since App({1}) is a C-ideal, <em>d<\/em> \u2297 <em>v<sub>d<\/sub><\/em> is also in App({1}), and therefore <em>v<sub>d<\/sub><\/em> is in \u03a9<em><sub>d<\/sub><\/em>, as promised.  In other words, <em>v<sub>d<\/sub><\/em> is the largest element of \u03a9<em><sub>d<\/sub><\/em>, or equivalently the largest element <em>v<\/em> such that <em>d<\/em> \u2297 <em>v<\/em> \u2208 App({1}).  (We are really retrieving the equivalence of C-ideals with Galois connections: the map that sends each <em>d<\/em> to <em>v<sub>d<\/sub><\/em> is one side of the corresponding Galois connection.)<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">This allows us to rewrite Fact D as the following.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Fact E.<\/strong>  For every \u03c6 in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], <em>u<\/em><sub>\u03c6<\/sub> = \u22c1{<em>v<sub>d&#8217;<\/sub><\/em> | <em>d&#8217;<\/em> \u2208 <strong>OS<\/strong><sup>\u03a9<\/sup> such that \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong>}.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Lemma F.<\/strong>  For every <em>d<\/em> \u2208 <strong>OS<\/strong><sup>\u03a9<\/sup>, the open set <em>O<sub>d<\/sub><\/em> is included in the upward closure \u2191\u03c6<em><sub><em>v<sub>d<\/sub><\/em><\/sub><\/em> in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>].<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Proof.<\/em>  Using the fact that \u03c6 \u21a6 <em>u<\/em><sub>\u03c6<\/sub> and <em>u<\/em> \u21a6 \u03c6<em><sub>u<\/sub><\/em> are mutually inverse <em>order<\/em>-isomorphisms (Proposition D), it suffices to show that every element \u03c6 of <em>O<sub>d<\/sub><\/em> is such that <em>u<\/em><sub>\u03c6<\/sub>\u2265<em>v<sub>d<\/sub><\/em>.  By definition of <em>O<sub>d<\/sub><\/em>, the fact that \u03c6 is in <em>O<sub>d<\/sub><\/em> means that \u03c6(<em>d<\/em>)=<strong>1<\/strong>.  But <em>u<\/em><sub>\u03c6<\/sub>\u2265<em>v<sub>d&#8217;<\/sub><\/em> for every <em>d&#8217;<\/em> \u2208 <strong>OS<\/strong><sup>\u03a9<\/sup> such that \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong>, by Fact E.  \u2610<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Lemma G.<\/strong>  For every \u03c6 in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], the family of elements <em>v<sub>d&#8217;<\/sub><\/em>, when <em>d&#8217;<\/em> ranges over the elements of <strong>OS<\/strong><sup>\u03a9<\/sup> such that \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong>, is directed.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Proof.<\/em>  The map <em>d&#8217;<\/em> \u21a6 <em>v<sub>d&#8217;<\/sub><\/em> is antitonic (just like for any Galois connection!).  Hence it suffices to show that the family <em>F<\/em> \u225d {<em>d&#8217;<\/em> \u2208 <strong>OS<\/strong><sup>\u03a9<\/sup> | \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong>} is filtered.  It is certainly so, since  \u03c6(\u22a4)=<strong>1<\/strong> (so \u22a4 is in <em>F<\/em>) and given any two elements <em>d&#8217;<\/em>, <em>d&#8221;<\/em> in <em>F<\/em>, \u03c6(<em>d&#8217;<\/em> \u22c0 <em>d&#8221;<\/em>)=\u03c6(<em>d&#8217;<\/em>) \u22c0 \u03c6(<em>d&#8221;<\/em>)=<strong>1<\/strong>, since \u03c6 is a frame homomorphism.  In fact, <em>F<\/em>=\u03c6<sup>\u20131<\/sup>({<strong>1<\/strong>}), and we even know that this is a completely prime filter.   \u2610<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">We can now conclude.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><strong>Theorem.<\/strong>  Every frame such that <strong>OS<\/strong><sup>\u03a9<\/sup> exists in <strong>Loc<\/strong> is continuous.  In particular, every exponentiable frame \u03a9 is a continuous frame.<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><em>Proof.<\/em>  By Proposition D, \u03a9 is order-isomorphic to [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], so it suffices to show that [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] is a continuous dcpo.  For every \u03c6 in [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>], <em>u<\/em><sub>\u03c6<\/sub> is the supremum of the directed family of elements <em>v<sub>d&#8217;<\/sub><\/em>, where <em>d&#8217;<\/em> ranges over the set \u03c6<sup>\u20131<\/sup>({<strong>1<\/strong>}) of elements of <strong>OS<\/strong><sup>\u03a9<\/sup> such that \u03c6(<em>d&#8217;<\/em>)=<strong>1<\/strong>, by Fact E and Lemma G.  Using the order-isomorphism \u03c6 \u21a6 <em>u<\/em><sub>\u03c6<\/sub> and its inverse, \u03c6 is itself the supremum of the directed family of elements <em>\u03c6<em><sub><em>v<sub>d&#8217;<\/sub><\/em><\/sub><\/em><\/em>, where <em>d&#8217;<\/em> ranges over \u03c6<sup>\u20131<\/sup>({<strong>1<\/strong>}).  For each such <em>d&#8217;<\/em>, <em>O<sub>d&#8217;<\/sub><\/em> is included in\u2191\u03c6<em><sub><em>v<sub>d&#8217;<\/sub><\/em><\/sub><\/em> by Lemma F, and <em>O<sub>d&#8217;<\/sub><\/em> is Scott-open by Proposition C.  Hence \u03c6<em><sub><em>v<sub>d<\/sub><\/em><\/sub><\/em> is way-below \u03c6.  (Explicitly, any directed family <em>D<\/em> whose supremum is above \u03c6 will be such that sup D is in <em>O<sub>d&#8217;<\/sub><\/em>.  Since <em>O<sub>d&#8217;<\/sub><\/em> is Scott-open, some element of <em>D<\/em> will be in <em>O<sub>d&#8217;<\/sub><\/em>, and therefore in \u2191\u03c6<em><sub><em>v<sub>d&#8217;<\/sub><\/em><\/sub><\/em> since <em>O<sub>d&#8217;<\/sub><\/em> \u2286 \u2191\u03c6<em><sub><em>v<sub>d&#8217;<\/sub><\/em><\/sub><\/em>.  Namely, that element will be above \u03c6<em><sub><em>v<sub>d&#8217;<\/sub><\/em><\/sub><\/em>.)   We have obtained that every element \u03c6 of [<strong>OS<\/strong><sup>\u03a9<\/sup> \u2192<sub>frm<\/sub> <strong>O1<\/strong>] \u2245 \u03a9 is the supremum of a directed family of elements way-below \u03c6, and that is enough for our purpose, by Trick 5.1.20 in the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>, for example.  \u2610<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Conclusion<\/h2>\n\n\n\n<p class=\"wp-block-paragraph\">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).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">Let me notice that this implies that any exponentiable locale is <em>spatial<\/em>: every continuous distributive complete lattice is a spatial frame (Proposition 8.3.19 in the <a href=\"https:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item7069109\/Non-Hausdorff%20Topology%20and%20Domain%20Theory\/?site_locale=en_GB\">book<\/a>, for example).  This is the basis of Hofmann-Lawson duality, which says more; in particular, that a continuous distributive lattice \u03a9 must be isomorphic to <strong>O<\/strong><em>X<\/em> for some locally compact space <em>X<\/em> (which happens to be <strong>pt<\/strong>\u03a9).<\/p>\n\n\n\n<p class=\"wp-block-paragraph\">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&#8217;s construction.  His construction is purely localic, but maybe sacrificing purity by making some hidden uses of the Axiom of Choice (&#8230; which are behind the spatiality of continuous frames, in the form of Zorn&#8217;s Lemma) will result in a more readable object.  If I do it this way, I hope that the purists will forgive me.  We&#8217;ll see!<\/p>\n\n\n\n<ol class=\"wp-block-list\">\n<li>John Martin Elliott Hyland.  <a href=\"https:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0089910.pdf\">Function spaces in the category of&nbsp;locales<\/a>.  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 <a href=\"https:\/\/link.springer.com\/book\/10.1007\/BFb0089899\">Lecture Notes in Mathematics 871<\/a>, pages 264\u2013281, 1981.<\/li>\n\n\n\n<li>Jorge Picado and Ale\u0161 Pultr. Frames and locales \u2014 topology without points. Birkh\u00e4user, 2010.<\/li>\n<\/ol>\n\n\n<div class=\"wp-block-image\">\n<figure class=\"alignright is-resized\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/wp-content\/uploads\/2016\/08\/jgl-2011.png\" alt=\"jgl-2011\" class=\"wp-image-993\" width=\"60\" height=\"83\"\/><\/figure>\n<\/div>\n\n\n<p class=\"wp-block-paragraph\">\u2014 <a href=\"https:\/\/www.lsv.ens-paris-saclay.fr\/~goubault\/?l=en\">Jean Goubault-Larrecq<\/a> (May 21st, 2023)<\/p>\n\n\n\n<p class=\"wp-block-paragraph\"><\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 &hellip; <a href=\"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/?page_id=6714\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"_crdt_document":"","footnotes":""},"class_list":["post-6714","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/6714","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=6714"}],"version-history":[{"count":94,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/6714\/revisions"}],"predecessor-version":[{"id":6817,"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=\/wp\/v2\/pages\/6714\/revisions\/6817"}],"wp:attachment":[{"href":"https:\/\/projects.lsv.ens-paris-saclay.fr\/topology\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=6714"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}