6  Effective bases

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 point-set topology and locale theory.

Remark 6.1 Recall that we call a system (Uⁿ) 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ⁿ) 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

where

1. ∑ denotes linear sum, union, disjunction or existential quantification;
2. “scalars” in the case of topology range over the Sierpiński space;
3. the dot denotes
   • inner product of a dual vector with a vector to yield a scalar,
   • that V is an element of the family classified by A_n, or
   • λ-application; and
4. ‘*’ denotes multiplication by a scalar of a vector, or conjunction.

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

where N is an overt discrete object (Section 4), such that every “vector” φ:Σ^X has a basis decomposition,

This is a join ⋁{βⁿ ∣ α_n} over a subset, with α_n≡ A_nφ, in the sense of Remark 4.12. In more traditional topological notation, this equation says that

where βⁿ,φ:Σ^X and A_n:Σ^ΣX classify open Uⁿ,V⊂ X and F_n⊂Σ^X in the sense of Remark 3.2.

We call (βⁿ) 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ⁿ⊂ Kⁿ (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 Γ⊢ βⁿ≤φ.

Proof    Since A_nφ⇔⊤, the basis decomposition for φ includes βⁿ as a disjunct.         ▫

Lemma 6.5 If ⊢ A_nβⁿ ⇔ ⊤ then βⁿ classifies a compact open subobject.

Proof    The equation A_nβⁿ ⇔ ⊤ says that the square commutes. Any test map φ:Γ→Σ^X↓βⁿ that (together with !:Γ→1) also makes a square commute must satisfy Γ⊢ A_nφ⇔⊤ and Γ⊢φ≤βⁿ , but then φ=βⁿ by the previous result. Hence the square is a pullback, whilst βⁿ=⊤_Σ^K, so the lower composite is ∀_K, making K compact.         ▫

The following jargon will be useful:

Definition 6.6 An effective basis (βⁿ,A_n) for an object X is called

1. a directed or ∨-basis if there is some element (that we call 0∈ N) such that

   β0=λ x.⊥   and   A0=λφ.⊤

   (though A₀=⊤ entails β⁰=⊥ by Lemma 6.4) and a binary operation +:N× N→ N such that

   βn+m  =  βn∨βm     and     An+m   =  An∧ Am;

   this definition is designed to work with Definition 4.13; it is used first in Lemma 9.8 and then extensively in Sections 11–16;
2. an intersection or ∧-basis if β¹=λ x.⊤ for some element (that we call 1∈ N), and there is a binary operation ⋆ such that

   βn⋆ m  =  βn∧βm      An ≤  An⋆ m   and   Am ≤  An⋆ m,

   so the intersection of finitely many basic opens is basic; this is a positive way of saying that we do have a basis instead of what is traditionally known as a sub-basis;
3. a lattice basis if it is both ∧ and ∨;
4. a filter basis if each A_n preserves ∧ and ⊤, and so corresponds in classical topology to a compact saturated (though not necessarily locally compact) subspace Kⁿ, by Lemma 5.16;
5. a prime basis if each A_n of the form A_nφ⇔φ pⁿ for some pⁿ:X (cf. Axiom 2), the corresponding compact subobject being Kⁿ={pⁿ}.

Any effective basis can be “up-graded” 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₁⊤⇔⊤ then the object is compact, with ∀_X=A₁, 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

1. N has an N-indexed prime basis given by

   βn ≡

   ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭

   ≡ λ x.(x=N n)   and   An ≡ ηN(n) ≡ λφ.φ n,

   because ∃ n.A_nφ∧βⁿ x  ≡  ∃ n.η nφ∧{n} x  ⇔  ∃ n.φ n∧ (x=n)  ⇔  φ x; and
2. Σ^N has a Fin(N)-indexed prime ∧-basis given by

   Bℓ≡ λξ.∀ m∈ℓ.ξ m   and   Aℓ≡ λ Φ.Φ(λ m.m∈ℓ),

   because Φξ ⇔ ∃ℓ.Φ(λ m.m∈ℓ)∧∀ m∈ℓ.ξ m by Axiom 4.10. (The convention that superscripts indicate covariance (Remarks 3.9 and 4.12) means that the imposed order on Fin(N) here is reverse inclusion of lists.)

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ⁿ) and (Uⁿ) of compact and open subspaces such that

As the subspace Kⁿ is compact, Remark 5.6 defines A_n:Σ^X→Σ such that Kⁿ⊂ V iff A_nφ⇔⊤, where βⁿ and φ:Σ^X classify Uⁿ and V⊂ X, so φ = ∃ n.A_nφ∧βⁿ.         ▫

Notice how the basis decomposition “short changes” us, for individual basis elements: we “pay” Kⁿ⊂ V but only receive Uⁿ⊂ Kⁿ 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ⁿ may be chosen to be interior of Kⁿ, and Kⁿ the closure of Uⁿ. 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 (βⁿ,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ⁿ, where

βⁿ and φ being the classifiers for Uⁿ and V as usual. Since Kⁿ=⋂_↓{V ∣ Kⁿ⊂ V}, we must have Uⁿ⊂ Kⁿ. Then, given x∈ V, so φ x⇔⊤, the basis decomposition φ x⇔∃ n.A_nφ∧βⁿ x, means that x∈ Uⁿ⊂ Kⁿ⊂ 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 re-deploy 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|<δ,

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) classify a sufficient computable family (Uⁿ⋔ 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 (βⁿ,A_n) is a filter basis for X. It is a lattice basis if the families (βⁿ) and (γ_n) are sublattices, with γ₀=⊤, γ₁=⊥, γ_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

and by Example 5.12, ↑β≡{φ ∣ β≪φ} is classified by some A:Σ^L.

This means that there is a basis decomposition

so (βⁿ,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 βⁿ≪φ in the sense of Definition 2. For suppose that φ≤⋁_s^↑θ_s, so ⊤  ⇔  A_nφ  ⇒  A_n⋁_s^↑θ_s  ⇔  ⋁_s^↑ A_nθ_s. Then⁵ A_nθ_s⇔⊤ for some s, so βⁿ≤θ_s by Lemma 6.4.

Now suppose that a locale carries an effective basis in our sense. Then

in which the second join is directed, by Lemma 2.6. Hence the frame L is continuous.         ▫

Remark 6.15 Notice that β^m≤βⁿ 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 λφ.βⁿ≪φ, cf. Remark 1.8.

Proposition 6.16 A locale is stably locally compact iff it has a lattice filter basis.

Proof    [⇒] Let A_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≤βⁿ and A_nφ⇔⊤, so β^m≪⊤. Also, if β^m≪φ and β^m≪ψ then, for some p, 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≤βⁿ and A_n(φ∧ψ)⇔⊤, so β^m≪φ∧ψ.         ▫

Remark 6.17 In summary, the dual basis A_nφ essentially says that there is a compact subobject Kⁿ lying between βⁿ and φ, but Kⁿ 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:

1. in the localic one, β ranges over a lattice, but ↑β need not be a filter;
2. in the spatial one we have filters, but the basis need only be indexed by a semilattice.

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.

5

This involves the same confusion of internally and externally defined joins as in Definition 5.2, cf. Remark 4.11.