Previous Up Next

5  Compact subspaces

Returning from logic to topology, recall from Definition 1.5 that we need to represent points, open subobjects and compact subobjects in our calculus. These will be given by terms of type X, ΣX and ΣΣX respectively, but whilst the first two correspond exactly, the question of which second order terms denote compact subspaces is more complicated.

We pick up the treatment of compact objects from Section C 7, and show how this leads to the representation of compact subobjects as quantifiers or modal operators. Following [HM81], these should preserve finite meets and directed joins, but the basic idea of ASD is that the directed joins come for free. A compact subobject is therefore represented by a term AΣX for which A⊤⇔⊤ and A(φ∧ψ)⇔ Aφ∧ Aψ.

This abstract idea works very well as far as the relationship between compact and closed subspaces of a compact Hausdorff space. But then we run into some trouble, because at that point we actually need to use Scott continuity, but our logical structure will not be strong enough to do this until Section 9. There is an alternative treatment in [J] that avoids this problem by restricting to the Hausdorff case, and in particular ℝ and ℝn; you may prefer to read that instead of this section, or in parallel with it.

In the experimental spirit, we try to go further down the path laid by [HM81, JS96], but we stumble into more and more potholes, showing how much more work needs to be done in ASD to make it into a full theory of general topology. But Jung and Sünderhauf do have something interesting to show us when we make this excursion, namely a very close duality between compact and open subobjects of stably locally compact objects.

The abstract analogue of the way in which locale theory treats local compactness is much simpler than this. In that case any term AΣX may be used — it doesn’t have to preserve meets.

Remark 5.1 Traditionally2, a topological space K has been defined to be compact if every open cover, i.e. family {UssS} of open subspaces such that K=⋃s Us, has a finite subcover, FS with K=⋃sF Us. If the family is directed (Definition 1) then F need only be a singleton, i.e. there is already some sS with K=Us.

The Scott topology on the lattice |ΣK| offers a simpler way of saying that K is compact. In this lattice, ⊤ denotes the whole of K, so compactness says that if we can get into the subset {⊤}⊂|ΣK| by a directed join ⋃s Us then some member Us of the family was already there3. In other words, {⊤}⊂ΣK is an open subset in the Scott topology on the lattice.

Definition 5.2 In abstract Stone duality we say that an object K is compact if there is a pullback

Using the fact that Σ classifies open subobjects (Remark 3.2), together with its finitary lattice structure (but not the Scott principle), Proposition C 7.10 shows that ∀K exists with this property iff it is right adjoint to Σ!K (where !K is the unique map K1). It is then demonstrated that this map does indeed behave like a universal quantifier in logic (the corresponding existential quantifier was given by Definition 4.3).

Lemma 5.3 If K and L are compact objects then K+L is also compact, as is ∅.

Proof    K+L(φ,ψ)⇔∀Kφ∧∀Lψ and ∀=⊤:Σ1→Σ.         ▫

The following result is the well known fact that the direct image of any compact subobject is compact (whereas inverse images of open subobjects are open).

Lemma 5.4 Let K be a compact object and p:KX be Σ-epi4, i.e. a map for which ΣpX→ΣK is mono. Then X is also compact, with quantifier ∀X=∀X·Σp.

Proof    The given quantifier, Σ!K⊣∀K, satisfies the inequalities

id  ≤  ∀K·Σp·Σ!X  =  ∀K·Σ!K 
Σp·Σ!X·∀K·Σp  =  Σ!K·∀K·Σp  ≤  Σp

from which we deduce Σ!X⊣∀K·Σp, since Σp is mono.         ▫

What becomes of the quantifier ∀K when K no longer stands alone but is a subobject of some other object X? We see that any compact subobject KX defines a map AX→Σ or AΣX that preserves ⊤ and ∧. We shall call this a necessity (▫) modal operator, rather than a quantifier, since we have lost the instantiation or ∀-elimination rule Aφ⇒φ x.

Lemma 5.5 Let i:KX be any map, with K compact. Then A≡∀K·ΣiX→Σ preserves ⊤ and ∧. Moreover Aφ≡∀Kiφ)⇔⊤ iff Σiφ=⊤K.

Proof    Σi preserves the lattice operations and ∀K is a right adjoint.         ▫

Remark 5.6 In traditional language, for any open set UX classified by φ:ΣX, the predicate Aφ says whether KU. Just as ∀KK→Σ classifies {⊤}⊂ΣK, the map AX→Σ classifies a Scott-open family F of open subspaces of X, namely the family of neighbourhoods of K. Preservation of ∧ and ⊤ says that this family is a filter.

Notice that we have an example of the alternation KU of compact and open subobjects that we saw in Lemma 1.2. Also, recall from Definition 1.5 that we wanted to test xU and KU; these are expressed by the λ-applications φ x and Aφ respectively.

Lemma 5.7

  1. If K=∅ then A=λφ.⊤, so in particular A⊥⇔⊤.
  2. If K={p} then A=λφ.φ p≡ηX(p), which is prime (Axiom 2) and preserves all four lattice operations, in particular A⊥⇔⊥.
  3. If KL exists then AKLφ⇔ AKφ∧ ALφ.
  4. If KL then AKAL.
  5. Even when KL is compact, AKAL need not be its modal operator.


  1. ΣK=1 and ∀K=λψ.⊤, so A≡∀K·Σi=λφ.⊤.
  2. ΣK=Σ, ∀K=id and Σi=λφ.φ p.
  3. Since K+LKLX, we have AKL=AK+L=AKAL by Lemmas 5.3 and 5.4.
  4. This follows from the previous part, since KL=L.
  5. Classically, of course, KLU does not imply (KULU). For example, let K={p} and L={q}, where p,qX are incomparable points in the specialisation order (Definition 3.7), so KL=∅. Then AKL⊥⇔⊤ but ⊥⇔ AK⊥∨ AL⊥.         ▫

Corollary 5.8 AK⊥⇔⊤ if K is empty, ⊥ if it’s inhabited.         ▫

Remark 5.9 Classically, any compact (sub)space that satisfies AK⊥⇔⊥ must therefore contain a point, by excluded middle, but Choice is still needed to find it [Joh82, Exercise VII 4.3]. In the localic formulation, it is a typical use of the maximality principle to find a prime filter containing F, so AP in our notation.         ▫

The situation in which open and compact subobjects interact extremely well is that of a compact Hausdorff object (Definitions 4.2 and 5.2).

Lemma 5.10 Let X be a compact Hausdorff object and φ:ΣX. Then

  (x≠ y)∨φ x(x≠ y)∨φ y 
  φ x∀ y.(x≠ y)∨φ y 
  (x≠ x)
  (x≠ y)(y≠ x)
  (x≠ z)(x≠ y)∨(y≠ z)

Proof    These are the lattice duals of (x=y)∧φ x ⇔ (x=y)∧φ y, φ x ⇔ ∃ y.(x=y)∧φ y, reflexivity, symmetry and transitivity in any overt discrete object, and the following proof is just the dual of that in Lemma C 6.7.

The closed subobject Δ:XX× X is co-classified by (≠X), so the corresponding nucleus, in the senses of both locale theory (j≡Δ*·Δ*) and of abstract Stone duality (E≡∀Δ·ΣΔ, Axiom 3.3(c) and Lemma 3.8) takes

φ:ΣX× X   to   λ x y.(x≠ y)∨φ y

Consider in particular ψ≡Σp0φ, or ψ(x,y)≡φ x; then

Δφ  =   ∀Δ·ΣΔ·Σp0φ  =  ∀Δ·ΣΔψ  =  (∀Δ⊥)∨Σp0φ.

The same thing in λ-calculus notation, and its analogue for p1, are

(∀Δφ)(x,y)  ⇔  (x≠ y)∨ φ x  ⇔  (x≠ y)∨ φ y

Now apply ∀p0≡∀ y, so φ  =  ∀p0·∀Δφ  =  ∀p0(∀Δ⊥∨Σp0φ), i.e.  φ x  ⇔  ∀ y.(xy)∨φ y . Inequality is irreflexive by definition. We deduce symmetry by putting φ≡λ u.(yu) and the dual of the transitive law with φ≡λ u.(uz).         ▫

The idea of the following construction is that KU iff UV=X, and conversely xV iff KX∖{x}, where K is compact and V is its complementary open subobject, encoded by A and ψ respectively. The lattice dual of this result — that open and overt subobjects coincide in an overt discrete object — was proved for ℕ in Section A 10.

Proposition 5.11 In any compact Hausdorff object K, there is a retraction ΣK◁ΣΣK given by

  ψλφ.∀ x.ψ x ∨ φ x 
  Aλ x.A(λ y.x≠ y),

where, if A is so defined from ψ then it preserves ⊤ and ∧.

Later we shall show that closed and compact subobjects agree exactly.

Proof    ψ↦ A↦λ x.Ayyxy)=ψ, by the second part of the Lemma. Then A⊤⇔⊤ easily, whilst A1∧φ2)⇔ Aφ1Aφ2 by distributivity.

On the other hand, A↦ψ↦λφ.∀ x.Ayyxy), whilst the first part of the Lemma says that A=λφ.Ay.∀ xyxy), so for the bijection between closed and compact objects we need A to commute with ∀ x. To show this, we need to know about the Tychonov product topology on X× X (Remark 8.3), and to use Scott continuity (Theorem 9.6).         ▫

As we said, it is not obligatory that the As that we shall use to define locally compact objects in the next section actually satisfy these conditions, i.e. preserve ⊤ and ∧. Consider the localic situation.

Example 5.12 For β∈ L in a continuous lattice (Definition 3), the subset

↑β ≡ {φ ∣ β≪φ} ⊂  L 

is Scott-open, and therefore classified by some AL (Remark 3.2). However, ↑β need not be a filter (cf. Definition 2.9), so A need not preserve ⊤ or ∧.         ▫

We obtain similar behaviour even in traditional topology. The following may seem a strange thing to do, but it will fall into place as we start to use the λ-calculus.

Notation 5.13 In [A] we found it useful to regard any map FX→ΣY (not necessarily a homomorphism for the monad or of frames, but nevertheless Scott-continuous) as a “second class” map F:Y−× X, and to write HS for the category composed of such maps. The work cited there explains how they interpret “control effects” such as jumps in programming languages. We shall in particular meet IX→ΣY such that Σi· I=id, where i:XY.

Remark 5.14 Just as in Lemma 5.5 we formed the modal operator corresponding to the direct image i K of K along i:KX as the composite A=∀K·Σi, so we may form the direct image F A along a second class map F:K−× X as ∀K· F. Its open neighbourhoods are given, as in Remark 5.6, by

 K⊂φ)  ⇔   (∀K· F)φ  ⇔  A(Fφ)   ⇔   (K⊂ Fφ).

However, ∀K· F need only be a filter when F preserves ⊤ and ∧.

Even when A does preserve meets, and so classifies a Scott-open filter of open subspaces, it need not correspond to a (locally) compact subspace. (It does in a compact Hausdorff object, but even there we do not yet have to tools to prove it, cf. Proposition 5.11.) We make a brief excursion into classical topology to illustrate the duality of open and compact subspaces, and their alternating inclusions (Notation 1.3). Recall from Definition 1.1 that any open subspace is the union of the compact subspaces inside it: the first result answers the dual question of when a compact subspace is the intersection of the open subspaces that contain it.

Lemma 5.15 Using excluding middle in classical topology [HM81, p221 def 2.1],

{y∈ X ∣ ∃ x∈ K.x≤ y}  =  ⋂{U⊂ X  open ∣ K⊂ U}, 

where ≤ is the specialisation order (Definition 3.7). We call this the saturation of K. Hence compact subspaces of X can be recovered from their modal operators iff X is T1 (when ≤ is trivial). For a specific non-example, let X≡Σ and K≡{⊥}, so A≡λφ.φ⊥ and the saturation of K is Σ.         ▫

What we might hope to recover from the modal operator A, therefore, is the saturation of K, as Karl Hofmann and Michael Mislove did for sober spaces [HM81, Theorem 2.16], and Peter Johnstone did for locales [Joh85]. This result shows that we have identified enough of the properties of modal operators, at least in the classical model.

Lemma 5.16 Let F⊂|ΣX| be a Scott-open filter of open subspaces of a sober (but not necessarily locally compact) space. Then, assuming the axiom of choice, K≡⋂FX is a compact subspace, and F={UKU}.         ▫

Lemma 5.17 [HM81, p221 thm 2.16] Let K≡⋂s Ks be a co-directed intersection of compact saturated subspaces of a sober space. Then K is also compact saturated, and AK=⋁ AKs. If all of the Ks are inhabited then so is K.         ▫

Theorem 5.18 [Kel55, Problem 5 F(a)] Compact saturated subspaces of a locally compact sober space form a continuous preframe under reverse inclusion. That is, for any compact saturated subspace KX,

K  =  ⋂{L  compact saturated ∣ L≺≺ K}. 

Here L≺≺ K means that there is an open subspace U with KUL (sic — Notation 1.3), but this is equivalent to LK, the order-reversed analogue of Definition 2, i.e

K ⊃ ⋂s Ms  ⇒ ∃ sK⊃ Ms.                 ▫ 

Corollary 5.19 Using Choice in classical topology, stably locally compact sober spaces enjoy the dual Wilker property (cf. Lemma 1.10): if KLU then there are open subspaces V and W and compact ones K′ and L′ such that K′∩ L′⊂ U, KVK′ and LWL′ [JS96, Theorem 23].

Proof    Use Lemma 2.7 in the continuous lattice of compact saturated subspaces under reverse inclusion. It is significant in this that the abstract joins in the lattice be given by intersections of subspaces.         ▫

Remark 5.20 There is still a problem. Even when X itself is locally compact, and we have a filter F that is Scott-open and therefore classified by a term A of type ΣΣX, the compact subspace K that they define need not be locally compact. Therefore they need not be definable as actual objects in the theory that we describe in this paper. However, an extension to and beyond the category of all locales is envisaged for later work. Preliminary investigations in this suggest that any AΣX that preserves ⊤ and ∧ can be expressed as the universal quantifier of a compact subobject.

However, as we said at the beginning of this section, the “dual bases” that we shall introduce in the next section use the As and not the Ks. It is a desirable property of A that it be a filter, i.e. preserve ⊤ and ∧, because then we can fully exploit the intuitions of traditional topology. But it is not necessary: locale theory gives rise to bases that don’t have this property, and both ways of doing things have their advantages.

In fact Bourbaki [Bou66, I 9.3] relegated this formulation to Axiom C‴, also calling it “the axiom of Borel–Lebesgue”. The older intuitions from analysis involve the existence of cluster points of sequences or nets of points, or of filters of subsets.
This is therefore an externally defined join, cf. Remark 4.11.
In our category, where every object is a subobject of some ΣY, Σ-epi is the same as epi. The name has been inherited from synthetic domain theory, a model of which is a topos, only some of whose objects (namely the predomains) may be so embedded.

Previous Up Next