This section introduces the first of our abstract characterisations of local compactness ((d) in the Introduction) and explores its relationship to the traditional definitions in pointset topology and locale theory.
Remark 6.1 Recall that we call a system (U^{n}) of vectors in a vector space
a basis if any other vector V can be expressed as a sum of
scalar multiples of basic vectors. Likewise, we say that a system
(U^{n}) of open subspaces of a topological space is a basis
if any other open set V can be expressed as a “sum” (union or
disjunction) of basic opens.
How do we find out which basis elements contribute to the sum, and (in the case of vector spaces) by what scalar multiple? By applying the dual basis A_{n} to the given element V, giving A_{n}· V. Then
V = 
 A_{n}· V * U^{n} 
where
In abstract Stone duality, since the application of A_{n} to a predicate V:Σ^{X} yields a scalar, it must have type Σ^{ΣX}. In the previous section we saw that (some) such terms play the role of compact subobjects.
Definition 6.2 An effective basis for an object
X is a pair of families
n:N ⊢ β^{n}:Σ^{X} n:N ⊢ A_{n}:Σ^{ΣX}, 
where N is an overt discrete object (Section 4), such that every “vector” φ:Σ^{X} has a basis decomposition,
φ = ∃ n. A_{n}φ ∧ β^{n}. 
This is a join ⋁{β^{n} ∣ α_{n}} over a subset, with α_{n}≡ A_{n}φ, in the sense of Remark 4.12. In more traditional topological notation, this equation says that
for all V⊂ X open, V = ⋃{U^{n} ∣ V∈F_{n}}, 
where β^{n},φ:Σ^{X} and A_{n}:Σ^{ΣX} classify open U^{n},V⊂ X and F_{n}⊂Σ^{X} in the sense of Remark 3.2.
We call (β^{n}) the basis and (A_{n}) the dual basis. The reason for saying that the basis is “effective” is that it is accompanied by a dual basis, so that the coefficients are given effectively by the above formula — it is not the computational aspect that we mean to stress at this point. The sub and superscripts indicate the co and contravariant behaviour of compact and open subobjects respectively with respect to continuous maps.
Remark 6.3
We shall find in Section 8 that every object that is definable
in the ASD calculus
(as we set it out in Sections 3–4)
has an effective basis.
However, there are plans to extend this calculus to and beyond general locales,
where those results will no longer apply.
Then we shall define a locally compact object
to be one that has an effective basis in the above sense.
The first observation that we make about this definition expresses the inclusion U^{n}⊂ K^{n} (cf. Definition 6). After that we see some suggestion of the role of compact subobjects, although Lemma 6.5 is too specific to be of much use, unless X happens to have a basis of compact open subobjects, i.e. it is a coherent object [Joh82, Section II 3].
Lemma 6.4 If Γ⊢φ:Σ^{X} satisfies
Γ⊢ A_{n}φ⇔⊤ then Γ⊢ β^{n}≤φ.
Proof Since A_{n}φ⇔⊤, the basis decomposition for φ includes β^{n} as a disjunct. ▫
Lemma 6.5 If ⊢ A_{n}β^{n} ⇔ ⊤ then β^{n}
classifies a compact open subobject.
Proof The equation A_{n}β^{n} ⇔ ⊤ says that the square commutes. Any test map φ:Γ→Σ^{X}↓β^{n} that (together with !:Γ→1) also makes a square commute must satisfy Γ⊢ A_{n}φ⇔⊤ and Γ⊢φ≤β^{n} , but then φ=β^{n} by the previous result. Hence the square is a pullback, whilst β^{n}=⊤_{ΣK}, so the lower composite is ∀_{K}, making K compact. ▫
The following jargon will be useful:
Definition 6.6
An effective basis (β^{n},A_{n}) for an object X is called
β^{0}=λ x.⊥ and A_{0}=λφ.⊤ 
β^{n+m} = β^{n}∨β^{m} and A_{n+m} = A_{n}∧ A_{m}; 
β^{n⋆ m} = β^{n}∧β^{m} A_{n} ≤ A_{n⋆ m} and A_{m} ≤ A_{n⋆ m}, 
Any effective basis can be “upgraded” to a lattice basis by formally adding unions and intersections (Lemma 8.4ff). It can be made into a filter ∨basis instead (Remark 17.6). Some of the other terminology is only applicable in special situations: if A_{1}⊤⇔⊤ then the object is compact, with ∀_{X}=A_{1}, whilst a sober topological space has a prime basis iff it is a continuous dcpo with the Scott topology (Theorem 12.11). Even when the intersection of two compact subobjects is compact, there is nothing to make A_{n⋆ m} correspond to it, but we shall rectify this in Proposition 12.14.
Examples 6.7 Let N be an overt discrete object. Then
β^{n} ≡ 
 ≡ λ x.(x=_{N} n) and A_{n} ≡ η_{N}(n) ≡ λφ.φ n, 
B^{ℓ}≡ λξ.∀ m∈ℓ.ξ m and A_{ℓ}≡ λ Φ.Φ(λ m.m∈ℓ), 
We devote the remainder of this section to showing that every locally compact sober space or locale has an effective basis in our sense. We start with traditional topology.
Proposition 6.8
Any locally compact sober space has a filter basis.
Proof Definitions 1.1 and 6 provide families (K^{n}) and (U^{n}) of compact and open subspaces such that
for each open V⊂ X, V = ⋃ {U^{n} ∣ K^{n} ⊂ V}. 
As the subspace K^{n} is compact, Remark 5.6 defines A_{n}:Σ^{X}→Σ such that K^{n}⊂ V iff A_{n}φ⇔⊤, where β^{n} and φ:Σ^{X} classify U^{n} and V⊂ X, so φ = ∃ n.A_{n}φ∧β^{n}. ▫
Notice how the basis decomposition “short changes” us, for individual basis elements: we “pay” K^{n}⊂ V but only receive U^{n}⊂ K^{n} as a contribution to the union. Nevertheless, the interpolation property (Lemma 1.2) ensures that we get our money back in the end.
In many examples, U^{n} may be chosen to be interior of K^{n}, and K^{n} the closure of U^{n}. However, this may not be possible if we require an ∨basis. For example, such a basis for ℝ would have as one of its members a pair of touching intervals, (0,1)∪(1,2), which is not the interior of [0,1]∪[1,2].
Remark 6.9 It is difficult to identify a substantive
Theorem by way of a converse to this in traditional topology,
since the λcalculus can only by interpreted in topological spaces
if they are already locally compact, and therefore have effective bases.
Nevertheless, we can show that a filter basis (β^{n},A_{n})
can only arise in the way that we have just described.
By Lemma 5.16, each A_{n} corresponds to some compact saturated subspace K^{n}, where
(K^{n}⊂ V) ⇔ A_{n}φ =⇒(U^{n}⊂ V), 
β^{n} and φ being the classifiers for U^{n} and V as usual. Since K^{n}=⋂_{↓}{V ∣ K^{n}⊂ V}, we must have U^{n}⊂ K^{n}. Then, given x∈ V, so φ x⇔⊤, the basis decomposition φ x⇔∃ n.A_{n}φ∧β^{n} x, means that x∈ U^{n}⊂ K^{n}⊂ V, as in Definition 1.1. ▫
Example 6.10 The closed real unit interval has a filter
∧basis with

where є,δ>0 and q are rational, and we redeploy the interval notation of Example 1.4 in our λcalculus. We also write <q±δ> for a variable that ranges over the codes, as opposed to the open (q±δ) and compact [q±δ] intervals that it names. The imposed order is given by comparison of the radii є or δ.
Proof Let x∈ U⊂[0,1]; then, for some є> 0, ∀ y.x−y<є⇒ y∈ U. So with δ≡1/2є, and q rational such that x−q<δ,
∀ y. 
 ⇒ y∈ U ∧ x∈ 
 , 
which is ∃<q±δ>.A_{q±δ}φ∧β^{q±δ}x in our notation. ▫
Example 6.11
Recall that any compact Hausdorff space X has a stronger property
called regularity: if C⊂ X is closed with x∉ C
then there are x∈ U⋔ V⊃ C with U,V⊂ X open and
disjoint.
Writing K=X∖ V and W=X∖ C for the complementary
compact and open subspaces, this says that given x∈ W,
we can find x∈ U⊂ K⊂ W, as in Definition 1.1.
Let (β^{n},γ_{n}) classify a sufficient computable family
(U^{n}⋔ V_{n}) of disjoint open pairs,
and put A_{n}≡λφ.∀ x.φ x∨γ_{n} x,
which corresponds to the compact complement of V_{n}
(Proposition 5.11).
Then (β^{n},A_{n}) is a filter basis for X.
It is a lattice basis if the families (β^{n}) and (γ_{n})
are sublattices, with γ_{0}=⊤, γ_{1}=⊥,
γ_{n+m}=γ_{n}∧γ_{m} and
γ_{n⋆ m}=γ_{n}∨γ_{m}. ▫
Remark 6.12 In these idioms of topology, where we say that there
“exists” an open or compact subobject within certain bounds,
that subobject may typically be chosen to be basic,
and the existential quantifier in the assertion ranges over
the set (overt discrete object) N of indices for the basis,
rather than over the topology Σ^{X} itself.
For example, this is the case with the Wilker property in
Lemmas 1.10 and 2.7.
Now we turn to locale theory.
Proposition 6.13 Any locally compact locale has a lattice
basis.
Proof The localic definition is that the frame L be a distributive continuous lattice (Definition 3), so
for all φ∈ L, φ = ⋁ {β∈ L ∣ β≪φ}, 
and by Example 5.12, ↑β≡{φ ∣ β≪φ} is classified by some A:Σ^{L}.
This means that there is a basis decomposition
φ = ∃ n. β^{n} ∧ A_{n}φ, where A_{n} ≡ λφ.(β^{n}≪φ), 
so (β^{n},A_{n}) is a lattice basis.
Recall, however, from Remark 3.9 that we must consider this basis to be indexed by the underlying set, L, of the frame L. Thus N≡L, whilst β^{(−)}:N→ L is the couniversal map from an overt discrete object N to L.
In fact it is enough for the image of N to generate L under directed joins (Definition 2.3). There is no need for N to be the couniversal way of doing this, and so no need for the underlying set functor −. ▫
Remark 6.14
The first part of the converse to this is Lemma 6.5,
but with the relative notion ≪ in place of compactness itself:
if A_{n}φ⇔⊤ then β^{n}≪φ
in the sense of Definition 2.
For suppose that φ≤⋁_{s}^{↑}θ_{s}, so
⊤ ⇔ A_{n}φ ⇒ A_{n}⋁_{s}^{↑}θ_{s}
⇔ ⋁_{s}^{↑} A_{n}θ_{s}.
Then^{5}
A_{n}θ_{s}⇔⊤ for some s,
so β^{n}≤θ_{s} by Lemma 6.4.
Now suppose that a locale carries an effective basis in our sense. Then
φ = ∃ n.A_{n}φ∧β^{n} ≡ ⋁{β^{n} ∣ A_{n}φ} ≤ ⋁^{↑}{β^{n} ∣ β^{n}≪φ} ≤ φ, 
in which the second join is directed, by Lemma 2.6. Hence the frame L is continuous. ▫
Remark 6.15
Notice that β^{m}≤β^{n} does not
imply any relationship between n,m∈ N,
because the function β^{(−)}:N→ L need not be injective.
This is the reason why A_{n} need not be exactly λφ.β^{n}≪φ,
cf. Remark 1.8.
Proposition 6.16
A locale is stably locally compact iff it has a lattice
filter basis.
Proof [⇒] Let A_{n}=λφ.β^{n}≪φ as before. [⇐] As we have an ∨basis, the basis expansion is a directed join, to which we may apply the definition of β^{m}≪φ. In this case there is some n with β^{m}≤β^{n} and A_{n}φ⇔⊤, so β^{m}≪⊤. Also, if β^{m}≪φ and β^{m}≪ψ then, for some p, q,
β^{m}≤β^{p}, β^{m}≤β^{q}, A_{p}φ⇔⊤ and A_{q}ψ⇔⊤, 
so β^{m}≤β^{p}∧β^{q}≡β^{p⋆ q}. As we have a filter ∧basis, A_{p⋆ q}φ∧ A_{p⋆ q}ψ⇔ A_{p⋆ q}(φ∧ψ)⇔⊤. Hence, with n=p⋆ q, β^{m}≤β^{n} and A_{n}(φ∧ψ)⇔⊤, so β^{m}≪φ∧ψ. ▫
Remark 6.17
In summary, the dual basis A_{n}φ essentially says that
there is a compact subobject K^{n} lying between β^{n} and φ,
but K^{n} seems to play no actual role itself,
and the localic definition in terms of ≪ makes it redundant,
cf. Proposition 2.2.
Nevertheless, each definition actually has its technical advantages:
Effective bases in our sense can be made to behave in either fashion, though we shall only consider lattice bases (cf. the localic situation) in this paper (Remark 17.6 sketches how filter bases may be obtained). Stably locally compact objects have lattice filter bases, whose properties will be improved in Proposition 12.14 to take advantage of the intersections of compact subobjects.