   ## 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:{ΣNE}↣ΣN with Σ-splitting I. As in Lemma 12.9, the next task is to characterise its elements, i.e. those Γ⊢ξ:ΣN that are admissible:

 Γ,  Φ:ΣΣN  ⊢ Φξ  ⇔  E Φξ.

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

 Γ,  n:N  ⊢ ξ n  ⇔  ∃ m.ξ m∧ m≺≺ n.

Proof    Consider Φ≡λξ.ξ n, so AL Φ ⇒ (ev Ln) by Lemma 13.14. Then

 ξ n  ⇔  Φξ  ⇔  E Φξ ⇔ ∃ m.∃ L.ξ m∧ (m≺≺ev L)∧ AL Φ          Notation 14.2 ⇒ ∃ m.∃ L.ξ m∧ (m≺≺ev L≼ n)         above ⇒ ∃ m.ξ m∧ (m≺≺ n)         monotonicity

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

 ξ 0  ⇔  ⊥      ξ 1  ⇔  ⊤      ξ(n+m)  ⇔  ξ n∨ξ m      ξ(n⋆ m)  ⇔  ξ n∧ξ m.

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

 ξ n⊙ξ m ⇔ Φξ  ⇔  E Φξ ⇔ ∃ k.∃ L.ξ k∧ (k≺≺ev L)∧ AL Φ         Notation 14.2 ⇒ ∃ k.∃ L.ξ k∧ (k≺≺ev L≼ n⊙ m)         above ⇒ ∃ k.ξ k∧ (k≺≺ n⊙ m)  ⇔  ξ(n⊙ m)         roundedness

with equality by L≡{|{|nm|}|} in Lemma 13.14. Similarly, for the constants, consider Φ≡λξ.⊤, so AL Φ⇔⊤⇔(ev L≼ 1), and Φ≡λξ.⊥, so AL Φ⇔∀ℓ∈ 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

 Φξ ⇔ ∃ L.AL Φ ∧ BLξ         lattice basis on ΣN ⇔ ∃ L.AL Φ ∧ξ(ev L) ⇔ ∃ L.∃ n.AL Φ ∧ξ n∧ (n≺≺ev L)         rounded ⇔ E Φξ         Definition 14.2

where the second step exploits the definition of BL (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 βn ≡ λ x. i x n and An ≡ λφ.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

 i x  =  λ n.βn x   and   Iφ  =  λξ.∃ n.Anφ∧ξ n.

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

∃ n.Anφ∧βn x
∃ n.Iφ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
∧ i x n         defs βn, An

∃ n.(I·Σi) Φ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
∧ξ n         defs Φ, ξ

∃ n.E Φ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
∧ξ n         defs i, I
E Φξ         E Φ preserves ξ⇔∃ n.{n}∧ξ n
(Iφ)(i x)         defs Φ, ξ
φ x           {}η (Section B 8).         ▫

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

This is the generalisation of x=⋁{pn ∣ ξ 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 xUnKn in the spatial setting, cf. Definition 1.1.

Theorem 15.8 n,An) is a lattice basis, and its way-below relation is ≺≺.

Proof    Since x:X ⊢ ξ≡ i x≡λ nn xN is admissible, and therefore a homomorphism by Lemma 15.3, we have

 β0  =  λ x.⊥,   β1  =  λ x.⊤   and   βn⊙ m  =  βn⊙βm.

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

Anφ ⇔ Iφ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
⇔  Φ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
⇔ E Φ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭

Hence

A0φ
E Φ
 ⎧ ⎨ ⎩ 0 ⎫ ⎬ ⎭

∃ L.(0≺≺ev L)∧AL Φ         Notation 14.2
(0≺≺ 0)∧A0 Φ  ⇔  ⊤
Anφ∧ Amφ
E Φ
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
∧ E Φ
 ⎧ ⎨ ⎩ m ⎫ ⎬ ⎭

∃ L1 L2. (n≺≺ev L1)∧(m≺≺ev L2)∧AL1Φ∧AL2Φ         Def. 14.2
∃ L1 L2. (n+m≺≺ev L1+ev L2)∧AL1+L2Φ         Lemma 13.5
∃ L.(n+m≺≺ev L)∧AL Φ         Lemma 13.13

E Φ
 ⎧ ⎨ ⎩ n+m ⎫ ⎬ ⎭
⇔  An+mφ         Notation 14.2

using distributivity, L=L1+L2 and Lemma 13.6. But An+mφ⇒ Anφ, so we have equality. Finally,

Anβm
I(λ x.i x m)
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
⇔  (I·Σi)(λξ.ξ m)
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
Lemma 15.6

E(λξ.ξ m)
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭

∃ L.(n≺≺ev L)∧AL(λξ.ξ m)         Notation 14.2
∃ L.(n≺≺ev L≼ m)         Lemma 13.14
(n≺≺ m)          monotonicity

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

Corollary 15.9 If the object X and its lattice basis (βn,An) had been given, and ≺≺ and E derived from them, this construction would recover X and (βn,An) 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 Hnm in the next section, in order to generalise from points of X to continuous functions YX.   