Points disappeared from the discussion right at the beginning, and we saw in Example 1.4 that it is easier to specify ℝ with the Euclidean topology using open and compact subspaces than using open subspaces and points. Arguably, topology should be axiomatised in this way, just as traditional geometry was axiomatised in terms of lines and circles that were entities in themselves, rather than being sets of points.
Locale theory reduces the description further, to one involving open subspaces alone. To do this for locally compact spaces, we must represent compact subspaces in terms of their systems of neighbourhoods. We also have to characterise the situation (U≺≺ V)≡∃ K.(U⊂ K⊂ V). We shall see that the way in which this is done for locales is subtly different from that for spaces, especially in the non-stably locally compact case (Remark 6.17).
Definition 2.1 Let L be a complete lattice.
Proposition 2.2 The topology of any locally compact space is a
distributive continuous lattice, in which U≺≺ V iff U≪ V
[HM81, p. 212].
Proof U≺≺ V implies U≪ V by compactness of K with U⊂ K⊂ V, and
| V = ⋃ {W ∣ W≺≺ V} |
by Definition 1.1. This union is directed by Lemma 1.9, so it may be used in the definition of U≪ V, giving U⊂ W≺≺ V for some W, but then U≺≺ V too. Hence U≪ V iff U≺≺ V, but notice that the proof does not supply an interpolating compact subspace U⊂ K⊂ V. ▫
Conversely, every distributive continuous lattice is the lattice of open subspaces of some locally compact sober space. However, this result relies on the axiom of choice, and even then it is not a trivial matter to prove it (Remark 17.6, [HL78]).
Definition 1.5 for spaces has a simpler analogue for locales, since it’s all lattice theory.
Definition 2.3
A computable basis (N,0,1,+,⋆,≺≺)
for a continuous distributive lattice L
is a set N with constants 0,1∈ N,
computable binary operations +,⋆:N× N→ N,
a recursively enumerable binary relation ≺≺
and an interpretation β(−):N→ L
that takes (0,1,+,⋆) to the lattice structure in L, such that
n≺≺ m iff βn≪βm and
| for each φ∈ L, φ = ⋁↑{βn ∣ βn≪φ}. |
If L1 and L2 have bases (βm) and (γn) then H:L2→ L1 is a computable frame homomorphism if H preserves ⊤, ∧ and ⋁, and the relation (βm≪ Hγn) is recursively enumerable. The interested reader may like to translate the abstract conditions on this relation that are set out in Section 16 into locale theory, and thereby recover the frame homomorphism H.
Once again we seek to remove the locale or continuous lattice from the definition, this time with the goal of eliminating the infinitary joins in favour of finitary properties of the way-below relation. Of course, since ≪ was itself defined using directed joins, in Section 11 it will have to be replaced by an abstract relation ≺≺. This will satisfy axioms based on the following properties, which are the analogues of Lemmas 1.2, 1.9 and 1.10:
Lemma 2.4 If β′≤β≪φ≤φ′ then
β′≪φ′. ▫
Lemma 2.5 The relation ≪ is
transitive and interpolative:
if α≪β≪γ then α≪γ,
and conversely given α≪γ, there is some β with
α≪β≪γ. ▫
Lemma 2.6 ⊥≪φ, and
if α≪φ and β≪φ then (α∨β)≪φ. ▫
The Wilker property in Lemma 1.10 used excluded middle, but its analogue for continuous lattices is both intuitionistic and very simple: it follows from the observation that binary joins distribute over joins of inhabited, and in particular directed, families.
Lemma 2.7 In any continuous lattice, if
α≪β∨γ then α≪β′∨γ′ for some
β′≪β and γ′≪γ.
Proof Since any directed set is inhabited,
| β∨γ = ⋁↑{β′∨γ ∣ β′≪β} = ⋁↑{β′∨γ′ ∣ β′≪β, γ′≪γ}. |
Then if α≪β∨γ, we have α≪β′∨γ′ for some term in this join. ▫
The relationship between ≪ and ∧ is more subtle.
Lemma 2.8
If α≪β≪φ and β≪ψ then α≪φ∧ψ.
▫
Definition 2.9
A stably locally compact locale is one in which ⊤≪⊤,
and if β≪φ and β≪ψ then β≪φ∧ψ.
Examples 1.12 can be adapted to yield locally compact locales that are not stably locally compact, and therefore only obey the weaker rule in the Lemma.
Remark 2.10 Stably locally compact objects enjoy many superior properties,
illustrating the duality between compact and open subspaces.
Jung and Sünderhauf [JS96] set out “consistency
conditions” for them that are similar to ours,
except that they choose to make (0,1,+,⋆)
a genuine (“strong proximity”) lattice.
However, as Examples 1.12 illustrated, not all of the locally compact objects that we wish to consider are stably so, either in geometric topology or recursion theory. Most obviously for the former, in ℝ, the whole space (the trivial intersection) is not compact.
Another reason why we consider the more general situation is that it corresponds to the monadic Axiom 3 that was the fundamental idea behind the research programme of which this paper is a part. This correspondence, which has no counterpart in [JS96], is the main technical goal of this paper; the consistency conditions are just an intermediate step.
We shall see at the end of Section 6 that the non-stable situation also highlights an interesting difference (separate from the usually mentioned ones of constructivity) between locales and sober spaces as ways of presenting topological information.
Applying G.H. Hardy’s test [Har40], we may wonder which of the stable and non-stable theories is “beautiful” and which is “ugly”. My suspicion is that stably locally compact spaces and the “relational” morphisms that they describe ([JKM01] and our 9.11, 12.13, 15.5 and 16.15) play a different role in the bigger picture, whilst we are right to study “functional” morphisms in the non-stable case.
The logic that we use is a very weak computational one, but on closer examination, we see that a great deal of the work that has been done in domain theory, using many notions of “basis” or “information system” could actually be formulated in such a logic.