Previous Up Next

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.


  Φξ∃ 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  =  λ nn 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φ


∧ i x n         defs βn, An
∃ n.(I·Σi) Φ


∧ξ n         defs Φ, ξ
∃ n.E Φ


∧ξ n         defs i, I
 E Φξ         E Φ preserves ξ⇔∃ n.{n}∧ξ n
 Φξ         ξ admissible
 (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φ


  ⇔  Φ


 ⇔ E Φ





 ∃ L.(0≺≺ev L)∧AL Φ         Notation 14.2
 (0≺≺ 0)∧A0 Φ  ⇔  ⊤ 
  Anφ∧ Amφ


∧ E Φ


 ∃ 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


  ⇔  An+mφ         Notation 14.2

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

I(λ x.i x m)


   ⇔  (I·Σi)(λξ.ξ m)


             Lemma 15.6
E(λξ.ξ m)


 ∃ 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.

Previous Up Next