Compactly generated Hausdorff locales

Martín Escardó

Version of 17th March 2005

Abstract

We say that a Hausdorff locale is compactly generated if it is the colimit of the diagram of its compact sublocales connected by inclusions. We show that this is the case if and only if the natural map of its frame of opens into the second Lawson dual is an isomorphism. More generally, for any Hausdorff locale, the second dual of the frame of opens gives the frame of opens of the colimit. In order to arrive at this conclusion, we generalize the Hofmann–Mislove–Johnstone theorem and some results regarding the patch construction for stably locally compact locales.

Key words. Compactly generated Hausdorff locale, k-space, Lawson duality, Hofmann–Mislove–Johnstone theorem, patch construction.

MSC. 06D22, 54D50.

1 Introduction

In his work on function spaces of locales [11], Johnstone left the development of a theory of compactly generated locales open, emphasizing the advantages of considering locales over arbitrary toposes in such a development. We perform first steps in this direction, restricting our attention to the Hausdorff case. Here locales and continuous maps are the objects and morphisms of the opposite of the category of homomorphisms of frames, and the Hausdorff property of a locale X is taken to mean that the diagonal map X → X × X is a closed sublocale inclusion.

Compactly generated Hausdorff locales. For a Hausdorff locale X, we define

KX = colimit of the compact sublocales of X connected by inclusions.

Considering the cocone of inclusions of compact sublocales of X into X, the universal property of colimit gives a canonical map

ε_{X}: KX → X.

We say that X is compactly generated if this is a homeomorphism. In this paper we analyse this notion in terms of Lawson duality. In order to discuss this, we first introduce and recall notation, terminology and facts.

The topology of a locale. Our main references to locales are Johnstone’s books [10] and [13]. Recall that a sublocale is defined to be a regular monomorphism. For a locale X, we define

O X = topology of X = frame of open sublocales of X.

Isbell’s terminology is paratopology [9]. Open sublocales are ranged over by U, V, W. The smallest (open) sublocale of X is denoted by 0 and the largest by X or 1.

Lawson duality and the Hofmann–Mislove–Johnstone theorem. A preframe (or meetcontinuous semilattice) is a poset with finite meets and directed joins such that the former distribute over the latter. For a preframe L, one has a preframe

L^{∧} = Lawson dual of L = Scott open filters of L.

For any preframe homomorphism h: L → M, one has a preframe homomorphism h^{∧}: M^{∧} → L^{∧} defined by

h^{∧}(γ) = {u ∈ L | h(u) ∈ γ}.

This makes Lawson dualization into a contravariant endofunctor, which in turn makes the preframe homomorphism

e_{L}: L → L^{∧∧}
u ↦ {ϕ ∈ L^{∧} | u ∈ ϕ}

into a natural transformation.

For any locale X, let

Q X = compact fitted sublocales under reverse sublocale inclusion,

where a sublocale is called fitted if it is the meet of its neighbourhoods. The Hofmann– Mislove–Johnstone (HMJ) theorem [8, 12] says that the assignment

Q ↦ {U ∈ O X | Q ≤ U}

is an order (and hence preframe) isomorphism

Q X ≅ (O X)^{∧}.

Main theorem. We show that if X is Hausdorff then all compact sublocales are fitted and

O KX ≅ (Q X)^{∧}.

It follows that X is compactly generated if and only if the opens are determined by the compacts via Lawson dualization:

X is compactly generated ⟺ O X ≅ (Q X)^{∧}.

By the HMJ theorem, it follows that

O KX ≅ (O X)^{∧∧}.

From this and additional information we conclude that

X is compactly generated ⟺ O X ≅ (O X)^{∧∧} naturally.

For Hausdorff topological spaces, Hofmann and Lawson [7] had previously established the direction (⇒) of this conclusion. They achieved this by showing that, under suitable assumptions, the direct limit of preframes that are naturally isomorphic to their second duals is itself naturally isomorphic to its second dual. Their proof invokes the axiom of choice in a way that we haven’t been able to avoid. In any case, we observe that this doesn’t establish the implication (⇐) or that O KX ≅ (O X)^{∧∧}.

It follows from the description of KX via Lawson duality that KX has enough compacts for any Hausdorff locale X, in the sense that U ≤ V holds in O KX if and only if Q ≤ U implies Q ≤ V for all Q ∈ Q KX. Hence, in toposes satisfying the axiom of choice, compactly generated Hausdorff locales have enough points, because in such a topos every non-null compact locale has at least one point [10].

The patch construction. A striking connection with the patch construction [3] arises in our journey to the isomorphism O KX ≅ (Q X)^{∧}. This construction coreflectively transforms a stably locally compact locale X into a locally compact Hausdorff locale, denoted by Patch X and given by

O Patch X = frame of Scott continuous nuclei on O X.

For example, for a continuous poset that is stably locally compact in its Scott topology, the patch construction transforms the Scott topology into the Lawson topology. In the original formulation, regularity is used instead of the Hausdorff separation axiom, but the work of Vermeulen [15] shows that both notions coincide in the presence of compactness or local compactness.

If X is additionally compact, the preframe Q X is a frame. Moreover, this is the topology of another compact, stably locally compact locale [6, 10], here denoted by X^{op}:

O X^{op} = Q X.

Then X ≅ X^{op op}, which shows that Q X^{op} ≅ O X,

Patch X^{op} ≅ Patch X,

the locale X is Hausdorff if and only if X ≅ X^{op}, if and only if X ≅ Patch X. Constructive proofs of these classically known facts are given in [2].

Now, for any Hausdorff locale X, the preframe Q X is a frame if and only if X is compact. Hence if the locale X^{op} exists then it is homeomorphic to X and both are compact Hausdorff. However, for any preframe, the Scott continuous nuclei form a frame [1]. As a first step towards the main theorem, we show that, for X Hausdorff,

O KX ≅ frame of Scott continuous nuclei on Q X.

Thus, we can imagine KX as the patch of the non-existent locale X^{op}. Moreover, we show that, again for X a Hausdorff locale, a nucleus j on Q X is Scott continuous if and only if the filter j^{−1}(1) is Scott open, and that such nuclei are fitted. We record the immediate consequence:

O KX ≅ frame of fitted nuclei j on Q X with j^{−1}(1) Scott open.

This brings us back to the HMJ theorem.

A generalized HMJ theorem. In terms of frames and nuclei, the HMJ theorem says that, for any frame L, the assignment j ↦ j^{−1}(1) is an order isomorphism from compact fitted nuclei on L to the preframe L^{∧}. Moreover, a nucleus j is compact if and only if the filter j^{−1}(1) is Scott open. This holds, more generally, if L is a Heyting preframe, with literally the same proof of the HMJ theorem given in [5]:

1.1 Theorem For any Heyting preframe L, every ϕ ∈ L^{∧} is of the form j^{−1}(1) for a unique compact fitted nucleus j on L, given by j = ⋁{u^{∘} | u ∈ ϕ}.

Here a u^{∘} is the “open” nucleus

u^{∘}(v) = (u ⇒ v),

and a nucleus is said to be fitted if it is a join of open nuclei. In other words, the theorem says that there is an isomorphism

L^{∧} ≅ preframe of fitted nuclei j on L with j^{−1}(1) Scott open

given by

Δ(ϕ) = ⋁{u^{∘} | u ∈ ϕ}, ∇(j) = j^{−1}(1).

Now, a sufficient condition for Q X being a Heyting preframe is that the meet of any two compact fitted sublocales, calculated in the lattice of sublocales, be compact, because then Q X has all non-empty joins, which are enough to construct Heyting implication. Because this condition holds if the locale X is Hausdorff, the main result O KX ≅ (Q X)^{∧} is obtained by considering L = Q X in the above theorem.

What makes the above theorem difficult is that, in general, such joins are not computed pointwise. For L = O X with X a stably locally compact locale, there is a more economical proof of the HMJ theorem, which first establishes that the join is computed pointwise in this particular situation [3]. It turns out that this method can also be used to establish the above theorem for L = Q X with X Hausdorff, and we present such a proof of the theorem for this special case.

Partial results and open questions. It is well known that the category of compactly generated Hausdorff topological spaces is a coreflective subcategory of that of Hausdorff spaces [14]. Also, the canonical map ε: KX → X is a monomorphism in the category of spaces, because the space KX has the same points as X and a finer topology, and the canonical map is the identity on points.

We show that if the canonical map is a monomorphism for Hausdorff locales, then compactly generated Hausdorff locales form a coreflective subcategory of that of Hausdorff locales. Hence we are led to ask:

1.2 Question Is ε_{X} a monomorphism for every Hausdorff locale X?

It is plausible that KX is Hausdorff even if ε_{X} fails to be a monomorphism. Generalizing the above, we show, with a more laborious argument, that if KX is Hausdorff for every Hausdorff locale X, then the coreflection holds. Hence, if the answer to the previous question is negative, or the question resists to be answered, we are led to ask, more modestly:

1.3 Question Does K preserve the Hausdorff property?

In the course of this investigation, we have obtained a number of additional partial results in various directions, in particular regarding cartesian closedness, which are recorded in the unpublished paper [4].

Generality of the results. Our results hold for locales over any topos. In practice, as usual, this is achieved by working informally within set theory, but without invoking the principle of excluded-middle, the axiom of choice, or any principles that are not valid in the internal language of arbitrary toposes. (Whenever we say that a set is non-empty we mean the positive statement that it is inhabited.)

Acknowledgements. Reinhold Heckmann is gratefully acknowledged for a careful reading of a preliminary draft version and Achim Jung for many discussions. This work was partially developed during a visit to the École Normale Supérieure of Paris in June 2001. Thanks to Giuseppe Longo for the invitation and to Frédéric De Jaeger for discussions on the subject. A preliminary version of this work, which at that time was restricted to regular locales, was presented at the Venice Second Workshop on Formal Topology in April 2002. I am grateful to Per Martin-Löf and Giovanni Sambin for the invitation to take part of that enjoyable and productive meeting with people from various (topo)logical communities and to deliver a lecture.

2 The first Lawson dual of a Hausdorff locale

In this section we analyse the preframe Q X and the notion of Hausdorff separation for a locale X.

2.1 The preframe of compact closed sublocales

Our proofs of the results discussed in the introduction rely on representing the preframe Q X as a subpreframe of the frame O X, where X is a Hausdorff locale. Because the compact sublocales of a Hausdorff locale are closed, we can represent them by their open complements. In particular, because complementation reverses order, the order reversal that arises in the construction of Q X is cancelled out. More generally, the compact closed sublocales of any locale are in order-reversing bijection with a subpreframe of the topology of the locale.

2.1 Definition We say that an open sublocale C of a locale X is cocompact if its boolean complement X \ C in the lattice of sublocales of X is compact. The poset of cocompact opens of X is denoted by C X and cocompact opens are ranged over by the letters C, D, E.

Because the topology of the closed sublocale whose complement is the open U is the frame ↑ U = {V ∈ O X | U ≤ V }, the first and second assertions of the following lemma are equivalent. Since a sublocale X_{j} of a locale X induced by a nucleus j is compact if and only if its open-neighbourhood filter j^{−1}(1) is Scott open and since the boolean complement of an open sublocale U is the sublocale induced by the closed nucleus

U^{□}(V) = U ∨ V,

the equivalence of the first and the third follow.

2.2 Lemma The following are equivalent for any open sublocale C of a locale X.

1. C is cocompact.

2. The top open 1 is compact in the frame ↑ C = {U ∈ O X | C ≤ U}.

3. The filter {U ∈ O X | C ∨ U = X} is Scott open.

2.3 Lemma The following hold for any locale.

1. If C is a cocompact open and U ≥ C is open, then U is cocompact.

2. The cocompact opens are closed under the formation of non-empty joins and Heyting implication in the topology.

3. The cocompact opens are closed under the formation of finite meets.

4. The cocompact opens form a sub Heyting preframe of the topology.

5. The top open 1 is compact in the preframe of cocompact opens. Proof (1): A closed sublocale of a compact sublocale is compact.

(2): Heyting implication is inflationary in its second argument.

(3): Compact sublocales are closed under finite joins.

(4): Immediate.

(5): Let D be a directed set of cocompact opens with ⋁ D = 1 and choose any C ∈ D. Because C is cocompact, 1 is compact in the frame ↑ C and hence 1 ∈ D∩↑ C because this set has the same join as D by directedness. □

Notice that 2.3(5) amounts to the fact that if a filtered collection of compact closed sublocales has meet 0, then some member of the collection is already 0. Notice also that cocompact opens are closed under the formation of the empty join 0 if and only if the locale is compact. By 2.3(1), this is equivalent to saying that all opens are cocompact.

2.2 Hausdorff locales

Hausdorff locales are closed under the formation of sublocales, and compact sublocales of Hausdorff locales are closed [15]. Hence every compact sublocale of a Hausdorff locale is closed and Hausdorff. Most of the results formulated for Hausdorff locales in the introduction hold for locales satisfying this conclusion.

2.4 Definition We say that a locale is proto-Hausdorff if every compact sublocale is closed and Hausdorff.

Our reason for considering the generalization is that it distills the properties of Hausdorff locales that we exploit in our technical development, and the chosen terminology reflects the fact that we don’t attach importance to it.

2.5 Remark All the results formulated for Hausdorff locales in Sections 3–5, with the sole exception of 5.7, hold for proto-Hausdorff locales with the same proofs.

We exploit the fact that, in the presence of compactness, the Hausdorff and regularity separation axioms coincide [15]. Recall that a locale is called regular if every open V is a join of opens U ⪕ V. Here U ⪕ V is defined to mean that U^{−} ≤ V, where U^{−} is the closure of U in X, which is equivalent to V ∨ ¬U = X, where ¬U is the Heyting complement of U in O X. In this case one says that U is well inside V.

2.6 Definition For C ∈ C X and D, E ∈ ↑ C, we write E ⪕_{C} D to denote the well-inside relation of the frame ↑ C.

Because (E ⇒ C) calculated in O X or C X is the Heyting complement of E in ↑ C,

E ⪕_{C} D ⟺ D ∨ (E ⇒ C) = 1.

The following easy observation is our main method of proof for various facts concerning (proto-)Hausdorff locales.

2.7 Lemma The following are equivalent for any proto-Hausdorff locale X and all C ∈ C X and D, D′ ∈ ↑ C.

1. D ≤ D′,

2. D ∨ E = 1 implies D′ ∨ E = 1 for every E ∈ ↑ C.

3. E ⪕_{C} D implies E ≤ D′ for every E ∈ ↑ C, Proof (1) ⇒ (2): Immediate. (2) ⇒ (3): If E ⪕_{C} D then D ∨ (E ⇒ C) = 1 and hence the assumption (2) shows that D′ ∨ (E ⇒ C) = 1, that is, E ⪕_{C} D′, which in turn gives E ≤ D′. (3) ⇒ (1): This amounts to regularity of the compact sublocale X \ C, because its topology is ↑ C. □

The following is easily verified.

2.8 Lemma For any locale X, the map α_{X}: C X → (O X)^{∧} defined by

α(C) = {U ∈ O X | C ∨ U = 1}

is a preframe homomorphism.

2.9 Lemma For any proto-Hausdorff locale X,

1. α_{X}: C X → (O X)^{∧} is an isomorphism, and

2. all compact sublocales of X are fitted. Proof (1): By the HMJ theorem and the proto-Hausdorff property, if ϕ ∈ (O X)^{∧} then there is C ∈ C X with ϕ = ∇C^{□} = α(C). Hence α is a surjection. To show that it is an injection, assume that α(C) = α(D), that is, C ∨ U = 1 ⟺ D ∨ U = 1 for every U ∈ O X. Because C ∧ D ∈ C X and C, D ∈ ↑(C ∧ D), it follows from 2.7(2) that C = D, as required.

(2): By the proto-Hausdorff property, it is enough to show that C^{□} is fitted for every C ∈ C X. By the HMJ theorem and the proto-Hausdorff property, there is D ∈ C X with D^{□} fitted and α(C) = ∇D^{□} = α(D). But then D = C by (1) and hence C^{□} is fitted, as required. □

3 The colimit construction

In the introduction we constructed a locale KX for every Hausdorff locale X. Generalizing this, for an arbitrary locale X, we define KX to be the colimit of the compact closed sublocales of X. For each C ∈ C X,

O (X \ C) = ↑ C,

and if D ≥ C then we have a sublocale embedding i_{DC}: X \ D → X \ C given by

i_{DC}^{∗}(U) = D ∨ U.

It is clear that if E ≥ D ≥ C then

X \ E \overline{i_{ED}} X \ D
[figure: i_{EC}; i_{DC}]
X \ C,

and that i_{CC}: X \ C → X \ C is the identity. In other words, this construction produces a functor F : (C X)^{op} → Loc, given by F (C) = X \ C on objects and by F (D ≥ C) = (X \ D ⟶^{i_{DC}} X \ C) on arrows. We denote the legs of the colimiting cocone by

i_{C}: X \ C → KX.

Because colimits in Loc are limits in Frm, which can be calculated as in the category of sets, with pointwise joins and finite meets,

O KX = {j ∈ ∏_{C∈C X} ↑ C | ∀D ≥ C, j(D) = i_{DC}^{∗}(j(C))}
= {j: C X → C X | ∀D ≥ C, j(D) = D ∨ j(C)}.

The second equations holds because

j ∈ ∏_{C∈C X} ↑ C ⟺ C ≤ j(C) for all C ∈ C X,

and because this is entailed by the condition that j(D) = D ∨ j(C) for all D ≥ C as the choice C = D shows. The legs i_{C}: X \ C → KX of the colimiting cocone are then given by

i_{C}^{∗}(j) = j(C),

as these are the projections in the category of sets. If the maps f_{C}: X \ C → Y are the legs of another cocone, that is, for D ≥ C,

X \ D \overline{i_{DC}} X \ C
[figure: f_{D}; f_{C}]
Y,

then the unique continuous map f: KX → Y such that

X \ C  \overline{i_{C}} KX
[figure: f_{C}; f]
Y

for every C ∈ C X is given by

f^{∗}(V) = (C ↦ f_{C}^{∗}(V)),

again by the nature of limits in the category of sets.

Now considering Y = X and f_{C} = ε_{C} in the above construction, where the continuous map ε_{C}: X \ C → X is the closed inclusion

ε_{C}^{∗}(U) = C ∨ U,

we obtain a cocone and hence a unique map ε_{X}: KX → X with

X \ C  \overline{i_{C}} KX
[figure: ε_{C}; ε]
X

for every C ∈ C X, given by

ε^{∗}(U) = (C ↦ C ∨ U).

We now have a closer look at the topology of KX.

3.1 Lemma For any locale X and every function j: C X → C X, the following are equivalent.

1. j ∈ O KX.

2. j(D) = j(C) ∨ D for all D ≥ C in C X.

3. j(C ∨ U) = j(C) ∨ U for all C ∈ C X and U ∈ O X.

4. j(C ∨ E) = j(C) ∨ E for all C, E ∈ C X. Proof (1 ⇔ 2): This has already been established. (2 ⇒ 3): Choosing D = C ∨ U, as we may because C X is an upper set, we have C ≤ D and hence (2) gives j(C ∨ U) = j(C) ∨ C ∨ U = j(C) ∨ U because C ≤ j(C), as we have already seen. (3 ⇒ 4): Immediate. (4 ⇒ 2): For D ≥ C we have that C ∨ D = D, and hence using (4) with E = D, we get j(D) = j(C) ∨ D, as required. □

3.2 Lemma For any locale X, every j ∈ O KX is a nucleus on C X. Proof We have already seen that C ≤ j(C). By 3.1(2) with the choice D = j(C) we conclude that j(j(C)) = j(C) ∨ j(C) = j(C) and hence that j is idempotent. For given D and D′, the choice C = D ∧ D′, which implies D ≥ C and D′ ≥ C, gives j(D) = j(D ∧ D′) ∨ D and j(D′) = j(D ∧ D′) ∨ D′. It follows that j(D) ∧ j(D′) = (j(D ∧ D′) ∨ D) ∧ (j(D ∧ D′) ∨ D′) = j(D ∧ D′) ∨ (D ∧ D′) = j(D ∧ D′) using distributivity and again the fact that j is inflationary, which shows that j preserves finite meets. □

For any nucleus j on a meet-semilattice, there is a filter ∇j = j^{−1}(1).

3.3 Lemma For any nucleus j on a Heyting semilattice L and any u ∈ L, the inequality u^{∘} ≤ j holds if and only if j(u) = 1, where u^{∘}(v) = (u ⇒ v).

The standard proof for frames works without any modification. In particular, we have that ⋁{u^{∘} | j(u) = 1} ≤ j, and the nucleus j is called fitted if equality holds.

3.4 Theorem The following are equivalent for any Hausdorff locale X and every nucleus j: C X → C X.

1. j ∈ O KX.

2. j preserves non-empty joins.

3. j is Scott continuous.

4. ∇j ∈ (C X)^{∧}. Proof (1) ⇒ (2): Binary joins: j(C ∨ D) = j(C) ∨ D ≤ j(C) ∨ j(D) by 3.1(4), and the other inequality holds by monotonicity of j. Directed joins: Let D ⊆ C X be a directed set and choose any C ∈ D. Then, using 3.1(4) twice and the fact that the binary-join operation preserves directed joins in any of its arguments, j(⋁ D) = j(C ∨ ⋁ D) = j(C) ∨ ⋁ D = ⋁_{D∈D} j(C) ∨ D = ⋁_{D∈D} j(C ∨ D) = ⋁_{E∈D} j(E).

The last equation holds by directedness of D, because if D ∈ D then there is some E ∈ D above D and C and hence above C ∨ D.

(2) ⇒ (3): Immediate.

(3) ⇒ (4): The set {1} is Scott open in C X by 2.3(5).

(4) ⇒ (1): By 3.1(2), it suffices to show that j(D) ≤ D∨j(C) for D ≥ C because the other inequality holds as j is inflationary and monotone. We apply 2.7(2) using the fact that j(D) and D ∨ j(C) belong to ↑ C. For E ∈ ↑ C with 1 = E ∨ j(D), we need to conclude that 1 = E ∨ D ∨ j(C). Since 1 = E ∨ j(D) ≤ j(E ∨ D), Scott openness of ∇j and regularity of ↑ C show that there is some B ⪕_{C} E ∨ D such that already 1 = j(B). By 3.3, the second condition gives (B ⇒ C) ≤ j(C), and hence the first condition gives 1 = E ∨ D ∨ (B ⇒ C) ≤ E ∨ D ∨ j(C), as required. □

3.5 Corollary If X is Hausdorff then the topology of KX consists of the nuclei j on C X with ∇j ∈ (C X)^{∧}.

4 The second Lawson dual of a Hausdorff locale

Our next goal is to show that KX ≅ (C X)^{∧} if X is Hausdorff. If we show that every nucleus j ∈ O KX is fitted, the result then follows directly from 3.5 and 1.1. However, as discussed in the introduction, there is a more direct proof of the special case of 1.1 invoked here, which we now develop. Half of this argument has the fittedness condition as an immediate consequence.

For a filter ϕ ⊆ C X, let

Δϕ = ⋁{D^{∘} | D ∈ ϕ},

where the join is calculated in the frame of nuclei on the preframe C X. In order to show that this join can be computed pointwise for X Hausdorff and ϕ ∈ (C X)^{∧}, we develop a variation of an argument previously applied to prove [3, Lemma 5.1]. Let κ_{ϕ} denote the pointwise join:

κ_{ϕ}(C) = ⋁{D ⇒ C | D ∈ ϕ}.

4.1 Lemma Let X be a Hausdorff locale, ϕ ∈ (C X)^{∧}, and κ = κ_{ϕ}.

1. If D ∈ ϕ and E ∧ D ≤ C then E ≤ κ(C).

2. If C ≤ C′ and E ⪕_{C} κ(C′) then E ∧ D ⪕_{C} C′ for some D ∈ ϕ. Proof (1): By definition of Heyting implication.

(2): By the assumption, 1 = κ(C′) ∨ (E ⇒ C). Hence, by directedness of the defining join of κ(C′) and cocompactness of (E ⇒ C), there is some D′ ∈ ϕ with 1 = (D′ ⇒ C′) ∨ (E ⇒ C). It follows that E ⪕_{C} (D′ ⇒ C′). Because (D′ ∨ C′ ⇒ C′) = (D′ ⇒ C′) and because ϕ, being a filter, is upper closed, we may assume that D′ ≥ C′ and hence that D′ ∈ ↑ C. Then, because ϕ is Scott open and ↑ C is a regular frame, there is some D ⪕_{C} D′ in ϕ. Finally, because the well-inside relation is multiplicative [10], we conclude that E ∧ D ⪕_{C} (D′ ⇒ C′) ∧ D′ ≤ C′, as required. □

4.2 Lemma If X is Hausdorff and ϕ ∈ (C X)^{∧} then Δϕ = κ_{ϕ}. Proof It is enough to show that κ = κ_{ϕ} is a nucleus. Because κ is a pointwise directed join of nuclei, it is inflationary and, by the preframe distributive law, it preserves finite meets. To show that κ is idempotent, let E ⪕_{C} κ(κ(C)). By two successive applications of 4.1(2), we first conclude that E ∧ D ⪕_{C} κ(C) for some D ∈ ϕ and then that E ∧ D ∧ D′ ≤ C for some D′ ∈ ϕ. Since D ∧ D′ ∈ ϕ as ϕ is a filter, we conclude by 4.1(1) that E ≤ κ(C). By 2.7(3), it follows that κ(κ(C)) ≤ κ(C), as required. □

4.3 Lemma If X is Hausdorff and j ∈ O KX then Δ∇j = j and hence j is fitted. Proof Δ∇j(C) = ⋁{D ⇒ C | j(D) = 1} ≤ j(C) by 4.2 and 3.3. In order to prove the opposite inequality, let E ⪕_{C} j(C). Then 1 = j(C) ∨ (E ⇒ C) ≤ j(C) ∨ j(E ⇒ C) ≤ j(C ∨ (E ⇒ C)) = j(E ⇒ C). Taking D = (E ⇒ C), it follows that E ≤ ((E ⇒ C) ⇒ C) = (D ⇒ C) ≤ Δ∇j(C). The result then follows by 2.7(3). □

The following is a simplification of the argument applied by Johnstone to prove [12, Lemma 2.4], exploiting the fact that Δϕ is calculated pointwise in our situation:

4.4 Lemma If X is Hausdorff and ϕ ∈ (C X)^{∧} then ∇Δϕ = ϕ. Proof Let C ∈ ∇Δϕ, that is, Δϕ(C) = 1. Because 1 ∈ ϕ and ϕ is Scott open, we conclude by directedness of the defining join of Δϕ that (D ⇒ C) ∈ ϕ for some D ∈ ϕ. Hence C ≥ (D ⇒ C) ∧ D is in ϕ too because ϕ is a filter, which shows that ∇Δϕ ⊆ ϕ. Conversely, let C ∈ ϕ. Then (C ⇒ C) = 1 ∈ ϕ and hence Δϕ(C) = 1, that is, C ∈ ∇Δϕ, which shows that ϕ ⊆ ∇Δϕ. □

There is no reason why the nucleus C^{∘} should belong to O KX if C ∈ ϕ, but it is a corollary of the above development that the join of such nuclei does:

4.5 Lemma If X is Hausdorff and ϕ ∈ (C X)^{∧} then Δϕ ∈ O KX. Proof If j = Δϕ then j is a nucleus with ∇j = ∇Δϕ = ϕ ∈ (C X)^{∧}, and hence the desired conclusion follows from 3.4. □

Hence:

4.6 Theorem If X is a Hausdorff locale then the assignment j ↦ ∇j is an isomorphism O KX → (C X)^{∧} with inverse ϕ ↦ Δϕ.

We have seen in 2.9 that the map α: C X → (O X)^{∧} defined by

α(C) = {U ∈ O X | C ∨ U = 1}

is an isomorphism for any Hausdorff locale X. Dualizing this, we get an isomorphism α^{∧}: (O X)^{∧∧} → (C X)^{∧}.

4.7 Corollary The map Δ ∘ α^{∧}: (O X)^{∧∧} → O KX is an isomorphism for any Hausdorff locale X.

Recall that the natural map e: O X → (O X)^{∧∧} is defined by

e(U) = {ϕ ∈ (O X)^{∧} | U ∈ ϕ}.

4.8 Corollary If X is Hausdorff, then e: O X → (O X)^{∧∧} is an isomorphism if and only if β: O X → (C X)^{∧} defined by

β(U) = α^{∧} ∘ e(U) = {C ∈ C X | C ∨ U = 1}

is an isomorphism.

4.9 Lemma For any locale X,

[figure: O X; ε^{∗}; O KX; (O X)^{∧∧}; e; α^{∧}; (C X)^{∧}.; ∇]

Proof For any U ∈ O X and any C ∈ C X we have that C ∈ ∇ε^{∗}(U) if and only if ε^{∗}(U)(C) = 1 if and only if U ∨ C = 1 if and only if U ∈ α(C) if and only if α(C) ∈ e(U) if and only if C ∈ α^{∧}(e(U)). □

It follows that if X is Hausdorff then e: O X → (O X)^{∧∧} is a frame homomorphism, because ε^{∗} is a frame homomorphism and α^{∧} and ∇ are isomorphisms.

4.10 Corollary If X is a Hausdorff locale, then ε_{X}: KX → X is a homeomorphism if and only if e: O X → (O X)^{∧∧} is an isomorphism. Proof Again because α^{∧} and ∇ are isomorphisms. □

We now develop functoriality of K and naturality of ε. For a continuous map f: X → Y of Hausdorff locales, consider the diagram

[figure: O X; e_{O X}; (O X)^{∧∧}; α_{X}^{∧}; (C X)^{∧}; Δ_{X}; O KX; O Y; f^{∗}; e_{O Y}; (O Y)^{∧∧}; (f^{∗})^{∧∧}; α_{Y}^{∧}; (C Y)^{∧}; Δ_{Y}; O KY.; (Kf)^{∗}]

The left square commutes by naturality of e. Because the action of Lawson dualization on morphisms is given by inverse images and because the preframe (O X)^{∧∧}, being isomorphic to the frame O KX, is in fact a frame, we conclude that the preframe homomorphism (f^{∗})^{∧∧} is actually a frame homomorphism. Hence the right rectangle defines a frame homomorphism (Kf)^{∗}: O KY → O KX, because its horizontal arrows are isomorphisms, and hence a continuous map Kf: KX → KY. This construction is clearly functorial. By 4.9 and the fact that ∇ is an isomorphism with inverse Δ, the horizontal arrows of the outer rectangle compose to give

[figure: O X; ε_{X}^{∗}; O KX; O Y; f^{∗}; ε_{Y}^{∗}; O KY,; (Kf)^{∗}; X; ε_{X}; KX; Y; f; ε_{Y}; KY.; Kf]

This proves:

4.11 Theorem K is functorial on Hausdorff locales, making the canonical map ε into a natural transformation.

5 Coreflection

We begin by showing that if X is Hausdorff, then X and KX have the same compact closed sublocales.

5.1 Lemma Let X be any locale.

1. For any j ∈ O KX and all D, E ∈ C X, we have that j(D) ∨ E = D ∨ j(E).

2. If C ∈ C X and j ∈ O KX then ε_{X}^{∗}(C) ∨ j = ε_{X}^{∗}(j(C)).

3. If D ∈ C X and ε_{X}^{∗}(D) = 1 then D = 1. Proof (1): This follows from two applications of 3.1(4). (2): For any D ∈ C X, we have that (ε_{X}^{∗}(C)∨j)(D) = C ∨D∨j(D) = C ∨j(D) = j(C)∨D = ε_{X}^{∗}(j(C))(D). (3): If 1 = ε_{X}^{∗}(D) then 1 = 1(D) = ε_{X}^{∗}(D)(D) = D ∨ D = D. □

5.2 Lemma For any locale X, if C ∈ C X then ε_{X}^{∗}(C) ∈ C KX. Proof We use 5.1 and 2.2. Assume that ε_{X}^{∗}(C)∨⋁ J = 1 for J ⊆ O KX directed. Then ε_{X}^{∗}(⋁ J(C)) = 1 and hence ⋁ J(C) = 1. Because joins in O KX are calculated pointwise and the set {j(C) | j ∈ J} is directed, 2.3(5) gives j ∈ J with j(C) = 1. But then ε_{X}^{∗}(C) ∨ j = ε_{X}^{∗}(j(C)) = ε_{X}^{∗}(1) = 1, as required. □

Hence the frame homomorphism ε_{X}^{∗} (co)restricts to a preframe homomorphism h as in the left square, where i_{X} and i_{KX} are the preframe inclusions:

[figure: O X; i_{X} _{⊃}; C X; O KX; ε_{X}^{∗}; _{i_{KX}_{⊃}}; C KX,; h; . . . . . . . . .; C X; α_{X}; (O X)^{∧}; C KX; h^{−1}; .; .; .; .; .; .; .; .; .; α_{KX}; (O KX)^{∧}.; (ε_{X}^{∗})^{∧}]

By 2.9, the map α_{X}: C X → (O X)^{∧} is an isomorphism if X is Hausdorff, and hence in this case there is a preframe homomorphism h^{−1} defined by commutativity of the right square. The following is immediate:

5.3 Lemma For any locale X,

[figure: (O X)^{∧}; α_{X}; C X; (C X)^{∧}; (i_{X})^{∧}; β_{X}; O X.; i_{X}; ∩]

Here β_{X} = (α_{X})^{∧} ∘ e_{O X} is the preframe homomorphism considered in Corollary 4.8, and notice that (i_{X})^{∧} maps a filter ϕ ∈ (O X)^{∧} to its restriction (ϕ ∩ C X) ∈ (C X)^{∧}.

5.4 Lemma If X is Hausdorff then h: C X → C KX is an isomorphism with inverse h^{−1} : C KX → C X as defined above. Proof Because the maps α_{X}: C X → (O X)^{∧} and ∇: O KX → (C X)^{∧} are isomorphisms and i_{KX}: C KX → O KX is a monomorphism, it is enough to show that α_{X} ∘ h^{−1} ∘ h = α_{X} and ∇ ∘ i_{KX} ∘ h ∘ h^{−1} = ∇ ∘ i_{KX}.

For the first equation, we use 5.1 to calculate, where we have omitted the inclusions i_{X} and i_{KX}:

α_{X} ∘ h^{−1} ∘ h(C) = α_{X} ∘ α_{X}^{−1} ∘ (ε_{X}^{∗})^{∧} ∘ α_{KX} ∘ ε_{X}^{∗}(C)
= (ε_{X}^{∗})^{∧} ∘ α_{KX}(ε_{X}^{∗}(C))
= (ε_{X}^{∗})^{∧}({j ∈ C X | j ∨ ε_{X}^{∗}(C) = 1})
= (ε_{X}^{∗})^{∧}({j ∈ C X | ε_{X}^{∗}(j(C)) = 1})
= (ε_{X}^{∗})^{∧}({j ∈ C X | j(C) = 1})
= {U ∈ O X | ε_{X}^{∗}(U)(C) = 1}
= {U ∈ O X | C ∨ U = 1}
= α_{X}(C).

For the second equation, we use the diagrams of 4.9 and 5.3 and rules of 5.1:

∇ ∘ i_{KX} ∘ h ∘ h^{−1}(j) = ∇ ∘ ε_{X}^{∗} ∘ i_{X} ∘ α_{X}^{−1} ∘ (ε_{X}^{∗})^{∧} ∘ α_{KX}(j)
= α_{X}^{∧} ∘ e ∘ i_{X} ∘ α_{X}^{−1} ∘ (ε_{X}^{∗})^{∧} ∘ α_{KX}(j)
= β ∘ i_{X} ∘ α_{X}^{−1} ∘ (ε_{X}^{∗})^{∧} ∘ α_{KX}(j)
= (i_{X})^{∧} ∘ (ε_{X}^{∗})^{∧} ∘ α_{KX}(j)
= (i_{X})^{∧} ∘ (ε_{X}^{∗})^{∧}({k ∈ O KX | j ∨ k = 1})
= (i_{X})^{∧}({U ∈ O X | j ∨ ε_{X}^{∗}(U) = 1})
= {C ∈ C X | j ∨ ε_{X}^{∗}(C) = 1}
= {C ∈ C X | j(C) = 1}
= ∇ ∘ i_{KX}(j),

as required. □

5.5 Corollary If X is Hausdorff, then ε_{KX}: KKX → KX is a homeomorphism.

5.6 Remark As discussed in 2.5, all the results formulated for Hausdorff locales hold for proto-Hausdorff locales with the exception of Proposition 5.7 below.

5.7 Proposition If ε: KA → A is a monomorphism for every Hausdorff locale A, then compactly generated Hausdorff locales form a coreflective subcategory of that of Hausdorff locales. Proof If A is Hausdorff and KA → A is a monomorphism, then KA is Hausdorff, for the monomorphism property is equivalent to saying that the diagram

[figure: KA; Δ; KA × KA; A; ε; Δ; A × A; ε × ε]

is a pullback, and pullbacks of closed sublocales are closed. Because K is functorial on Hausdorff locales and the canonical map ε is natural, any continuous map f: X → A from a compactly generated Hausdorff locale to a Hausdorff locale factors through ε_{A} as Kf ∘ ε_{X}^{−1} : X → KA, and such a factorization is unique because ε: KA → A is a monomorphism. □

If we don’t assume that the canonical map is a monomorphism but we more modestly assume that K preserves the Hausdorff property, we reach the same conclusion with a more laborious argument, which we now develop. (Regarding locales satisfying the proto-Hausdorff property, notice that for K to preserve this it is enough that every compact sublocale of KA be closed for A proto-Hausdorff, but we don’t know whether this is the case.)

5.8 Proposition If K preserves the Hausdorff property, then compactly generated Hausdorff locales form a coreflective subcategory of that of Hausdorff locales. Proof By [14, Theorem IV-1.2(v)], it suffices to show that Kε_{A} ∘ ε_{KA}^{−1} = id_{KKA} for every Hausdorff locale A. Specializing the definition of Kf to f = ε_{A} and recalling the definition of h^{−1} given above, we get

[figure: O KA; e_{O KA}; (O KA)^{∧∧}; α_{KA}^{∧}; (C KA)^{∧}; Δ_{KA}; O KKA; O A; ε_{A}^{∗}; e_{O A}; (O A)^{∧∧}; (ε_{A}^{∗})^{∧∧}; α_{A}^{∧}; (C A)^{∧}; (h^{−1})^{∧}; Δ_{A}; O KA.; (Kε_{A})^{∗}]

Recalling that the horizontal arrows compose to ε_{KA}^{∗} and ε_{A}^{∗}, we calculate

(Kε_{A} ∘ ε_{KA}^{−1})^{∗}

= (ε_{KA}^{−1})^{∗} ∘ (Kε_{A})^{∗}
= (ε_{KA}^{−1})^{∗} ∘ (Kε_{A})^{∗} ∘ Δ_{A} ∘ Δ_{A}^{−1}
= (ε_{KA}^{−1})^{∗} ∘ Δ_{KA} ∘ (h^{−1})^{∧} ∘ Δ_{A}^{−1} (reworking (Kε_{A})^{∗} ∘ Δ_{A})
= e_{O KA}^{−1} ∘ (α_{KA}^{∧})^{−1} ∘ Δ_{KA}^{−1} ∘ Δ_{KA} ∘ (h^{−1})^{∧} ∘ Δ_{A}^{−1} (applying 4.9 to (ε_{KA}^{−1})^{∗})
= e_{O KA}^{−1} ∘ (α_{KA}^{∧})^{−1} ∘ (h^{−1})^{∧} ∘ Δ_{A}^{−1}  (cancelling Δ_{KA}^{−1} ∘ Δ_{KA})
= e_{O KA}^{−1} ∘ (α_{KA}^{∧})^{−1} ∘ (h^{∧})^{−1} ∘ Δ_{A}^{−1}  (reworking (h^{−1})^{∧})
= (Δ_{A} ∘ h^{∧} ∘ α_{KA}^{∧} ∘ e_{O KA})^{−1}  (by contravariance of (−)^{−1}).

Hence it suffices to show that h^{∧} ∘ α_{KA}^{∧} ∘ e_{O KA} = ∇_{A}. We calculate using 5.1:

C ∈ h^{∧} ∘ α_{KA}^{∧} ∘ e_{O KA}(j) ⟺ h(C) = ε_{A}^{∗}(C) ∈ α_{KA}^{∧} ∘ e_{O KA}(j)
⟺ α_{KA}(ε_{A}^{∗}(C)) ∈ e_{O KA}(j)
⟺ j ∈ α_{KA}(ε_{A}^{∗}(C)))
⟺ ε_{A}^{∗}(C) ∨ j = 1 ⟺ ε_{A}^{∗}(j(C)) = 1
⟺ j(C) = 1 ⟺ C ∈ ∇_{A}(j),

as required. □

References

[1] M.H. Escardó. Properly injective spaces and function spaces. Topology Appl., 89(1–2):75–120, 1998.

[2] M.H. Escardó. The patch frame of the Lawson dual of a stably continuous frame. Unpublished research note, School of Computer Science, St Andrews University, available at the author’s web page at his current institution, May 2000.

[3] M.H. Escardó. The regular-locally-compact coreflection of stably locally compact locale. Journal of Pure and Applied Algebra, 157(1):41–55, 2001.

[4] M.H. Escardó. Notes on compactly generated locales. Unpublished research note, School of Computer Science, University of Birmingham, available at the author’s web page, 2001–2005.

[5] M.H. Escardó. Joins in the frame of nuclei. Applied Categorical Structures, 11(2):117–124, 2003.

[6] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. Continuous Lattices and Domains. Cambridge University Press, 2003.

[7] K.H. Hofmann and J.D. Lawson. On the order-theoretical foundation of a theory of quasicompactly generated spaces without separation axiom. J. Austral. Math. Soc. Ser. A, 36(2):194–212, 1984.

[8] K.H. Hofmann and M. Mislove. Local compactness and continuous lattices. In Continuous Lattices, volume 871 of Lect. Notes Math., pages 209–248, 1981.

[9] J.R. Isbell. Atomless parts of spaces. Math. Scand., 31:5–32, 1972.

[10] P.T. Johnstone. Stone Spaces. Cambridge University Press, 1982.

[11] P.T. Johnstone. Open locales and exponentiation. In Mathematical applications of category theory (Denver, Col., 1983), pages 84–116. Amer. Math. Soc., 1984.

[12] P.T. Johnstone. Vietoris locales and localic semilattices. In Continuous lattices and their applications (Bremen, 1982), pages 155–180. Dekker, 1985.

[13] P.T. Johnstone. Sketches of an Elephant: a Topos Theory Compendium. Oxford University Press, 2002.

[14] S. Mac Lane. Categories for the Working Mathematician. Springer, 1971.

[15] J.J.C. Vermeulen. Some constructive results related to compactness and the (strong) Hausdorff property for locales. In Category theory (Como, 1990), pages 401–409. Springer, 1991.

Martín H. Escardó School of Computer Science, University of Birmingham Birmingham B15 2TT, UK