15  The points of the new space

Now we can characterise the (parametric) points of the object that we constructed from an abstract basis in the previous section. Then we define a lattice basis on it, just as we did for continuous dcpos in Theorem 12.11.

Notation 15.1 We are again in the situation of Definition 12.8, that we have defined a nucleus E from an abstract basis, so the monadic calculus (Section B 8) provides a subobject i:{Σ^N ∣ E}↣Σ^N with Σ-splitting I. As in Lemma 12.9, the next task is to characterise its elements, i.e. those Γ⊢ξ:Σ^N that are admissible:

Lemma 15.2 If Γ⊢ξ:Σ^N is admissible then it is rounded in the sense that

Proof    Consider Φ≡λξ.ξ n, so A_L Φ ⇒ (ev L≼ n) by Lemma 13.14. Then

where ⇒ is actually equality, as we may put L≡{|{|n|}|} in Lemma 13.14 to obtain ⇐.         ▫

Lemma 15.3 If Γ⊢ξ:Σ^N is admissible then it is a lattice homomorphism in the sense that

Proof    Consider Φ≡λξ.ξ n⊙ξ m, so A_L Φ  ⇒  (ev L≼ n⊙ m) by Lemma 13.14. Then

with equality by L≡{|{|n⊙ m|}|} in Lemma 13.14. Similarly, for the constants, consider Φ≡λξ.⊤, so A_L Φ⇔⊤⇔(ev L≼ 1), and Φ≡λξ.⊥, so A_L Φ⇔∀ℓ∈ L.⊥⇔(L=0).         ▫

Notice that it is the fact that ξ is rounded (for ≺≺), rather than a homomorphism (for 0,1,+,⋆), that distinguishes the particular object X from the ambient Σ^N into which it is embedded, cf. Remark 13.2.

Lemma 15.4 If Γ⊢ξ:Σ^N is a rounded lattice homomorphism then it is admissible.

Proof    

where the second step exploits the definition of B^L (Lemma 13.5) and ev L when ξ is a homomorphism.         ▫

Remark 15.5 Hence the rounded lattice homomorphisms ξ:Σ^N are the points of X, whilst the rounded filters (∧-homomorphisms) correspond to its compact saturated subspaces, at least when X is a classical stably locally compact space (Example 12.13).

Lemma 15.6 βⁿ ≡ λ x. i x n and A_n ≡ λφ.Iφ{n} provide an effective basis for X.

Proof    First note that ξ↦ Jφξ preserves joins in ξ, and therefore so do ξ↦E Φξ and ξ↦ Iφξ, as required by Lemma 7.7, so we recover

For the basis expansion, let φ:Σ^X and x:X. Then ξ≡ i x:Σ^N is admissible, and φ=Σⁱ Φ, where Φ≡ Iφ:Σ^ΣN.

Corollary 15.7 x  =  focus(∃ n. A_n ∧ ξ n).         ▫

This is the generalisation of x=⋁^↑{p_n ∣ ξ n} in domain theory (Proposition 12.3), and the version in ASD of {x}=⋂_↓K{x}≺≺ K in Theorem 5.18. The predicate ξ n means x∈ Uⁿ⊂ Kⁿ in the spatial setting, cf. Definition 1.1.

Theorem 15.8 (βⁿ,A_n) is a lattice basis, and its way-below relation is ≺≺.

Proof    Since x:X ⊢ ξ≡ i x≡λ n.βⁿ x:Σ^N is admissible, and therefore a homomorphism by Lemma 15.3, we have

Next we check the equations on A_n for an ∨-basis. Let φ:Σ^X and Φ≡ Iφ:Σ^ΣN. Then E Φ=I·Σⁱ· Iφ=Iφ=Φ, so

Hence

using distributivity, L=L₁+L₂ and Lemma 13.6. But A_n+mφ⇒ A_nφ, so we have equality. Finally,

where we also obtain ⇐ by putting L≡{|{|m|}|} in Lemma 13.14.         ▫

Corollary 15.9 If the object X and its lattice basis (βⁿ,A_n) had been given, and ≺≺ and E derived from them, this construction would recover X and (βⁿ,A_n) up to unique isomorphism. In particular, if we had started with a filter lattice basis, we would get it back.         ▫

We have shown that the notion of “abstract basis” is a complete axiomatisation of the way-below relation, and is therefore the formulation of the consistency requirements in Definitions 1.5 and 2.3, without using a classically defined topological space or locale as a reference.

This completes the proof of the equivalence amongst the characterisations of local compactness that we listed in the Introduction

In Lemmas 15.2ff, we have also characterised points x:X as rounded lattice homomorphisms ξ:Σ^N. We shall replace the predicate ξ m by a binary relation H_n^m in the next section, in order to generalise from points of X to continuous functions Y→ X.