8  Every definable object has a basis

In Section 6, we justified the notion of effective basis in the classical models, i.e. for locally compact sober spaces and locales. This section considers the term model, showing by structural recursion that every definable object has an effective basis. We have already dealt with the base cases (ℕ, Σ^ℕ) in Example 6.7, and with Σ-split subobjects in Lemma 7.5. So we consider binary products first (leaving the reader to define the 1-indexed basis for 1), but devote most of the section to the exponential Σ^X.

Lemma 8.1 If X and Y have effective bases then so does X× Y, given by Tychonov rectangles.

Proof    We are given (βⁿ,A_n) and (γ^m,D_m) on X and Y. Then, on X× Y, we define

Notice that the formula for F_(n,m) is not symmetrical in X and Y, though we have learned to expect properties of binary products to be asymmetrical and problematic [A]. In fact, if A_n and D_m are filter bases, we have another example of the same problem that held us back in Proposition 5.11, along with the core of its solution.

Lemma 8.2 If A:Σ^ΣX and D:Σ^ΣY both preserve either ⊤ and ∧ or ⊥ and ∨ then

whenever θ:Σ^{X× Y} is a finite union of rectangles.

Proof    Applying the Phoa principle (Axiom 3.6) to a single rectangle,

This would have the required symmetry if we had

If A⊤⇔⊤⇔ D⊤ then both sides are A⊥∨ D⊥, whilst if A⊥⇔⊥⇔ D⊥ then they are both ⊥. Under either hypothesis, the lattice dual argument shows the similar result

for a cross. The result uses equational induction [E, §2], but we shall just illustrate this with the case where θ is a union of three rectangles,

If A and D preserve ⊥ and ∨ then A Dθ is also a union of three terms, to each of which the first part applies.

We may also use distributivity of ∨ over ∧ to re-express the union θ as an intersection of eight crosses,

So if A and D preserve ∧ then A Dθ is a conjunction of eight factors, to each of which the second part applies, for example with φ=φ₁∨φ₂ and ψ=ψ₃. In both cases, A Dθ⇔ D Aθ as required.         ▫

Remark 8.3 This still awaits Theorem 9.6 on Scott continuity to extend finite unions of rectangles to infinite ones, but once we have that we may draw the corollaries that

1. if X and Y have filter bases then Lemma 8.1 provides a filter basis for X× Y, which is symmetrical in X and Y;
2. Proposition 5.11 yields a bijection between closed and compact subobjects of a compact Hausdorff object. Moreover, despite the other problems discussed in Section 5, preserving finite meets is enough to characterise ▫ modal operators.         ▫

We shall need to be able to turn any effective basis into a ∨-basis, which we do in the obvious way using finite unions of basic open subobjects. The corresponding unions of compact subobjects give rise to conjunctions of As by Lemma 3. Unfortunately, the result is topologically rather messy, both for products and for objects such as ℝ that we want to construct directly.

Lemma 8.4 If X has an effective basis indexed by N then it also has a ∨-basis indexed by Fin(N). If we were given a filter basis, the result is one too.

Proof    Given any basis (βⁿ,A_n), define

Then φ = ∃ n.A_nφ∧βⁿ ≤  ∃ℓ.D_ℓφ∧γ^ℓ using singleton lists. Conversely,

Then (γ^ℓ,D_ℓ) is a ∨-basis, using list concatenation for +. The imposed order ≼ on Fin(N) is list or subset inclusion,

Finally, if the A_n were filters then so are the D_ℓ, since ∀ m∈ℓ preserves ∧ and ⊤.         ▫

Remark 8.5 Computationally, it may be better to see this as an embedding i:X↣Σ^ΣN rather than into Σ^{Fin N}, as this gives a very simple representation of the basis and dual basis. Using the notation π_ℓ≡λ n.n∈ℓ and [ℓ]≡∀ n∈ℓ.ψ n from [E], which also provides a fixed-point equation for ∃ℓ, this is:

Lemma 8.6 If an ∧-basis was given, Lemma 8.4 yields a lattice basis.

Proof    We are given β¹=⊤ and βⁿ∧β^m=β^{n⋆ m}.

Let ℓ⋆ℓ′ be the list (it doesn’t matter in what order) of all n⋆ m for n∈ℓ and m∈ℓ′. In functional programming notation, this is

where map applies a function to each member of a list, returning a list, and flatten turns a list of lists into a simple list. Categorically, map is the effect of the functor List (−) on morphisms, and flatten is the multiplication for the List  monad. Using the corresponding notions for K(−), ⋆ can similarly be defined for finite subsets instead.

Now let

by distributivity in Σ^X, whilst γ^{|1|}≡β¹ and D_{|1|}≡ A₁ (where {|1|} is the singleton list) serve for γ¹ and D₁. (This uses equational induction, [E, §2].)         ▫

Remark 8.7 By switching the quantifiers, we may similarly obtain ∧-bases, and turn an ∨-basis into a lattice basis. In fact, this construction featured in the proof of Theorems 7.8 and 7.14. This time the filter property is not preserved, since if A_nφ means Kⁿ⊂ U then A_ℓφ means that ∃ n∈ℓ.Kⁿ⊂ U, which is not the same as testing containment of a single compact subobject. Proposition 12.14 shows how to define an ∧-basis for a locally compact object in which A_{n⋆ m} actually captures the intersection of the compact subobjects.

Proposition 8.8 N and Σ^N have effective bases as follows:

indexed by n:N, ℓ:Fin(N) or L:Fin(Fin(N)). The interchange of sub- and superscripts means that we’re reversing the imposed order on these indexing objects (Remark 4.12).         ▫

The last of these also provides a basis for Σ^ΣN, using Axiom 4.10 twice.

Lemma 8.9 Σ^ΣN has a Fin(Fin N)-indexed prime ∧-basis with

so, using Σ³ N as a shorthand for a tower of exponentials, Σ^ΣΣN≡ (((N→Σ)→Σ)→Σ),

Proof    The prime ∧-basis on Σ^N makes Σ^ΣN◁Σ^Fin(N) by

so Σ³ N◁Σ²Fin(N) by

For any F:Σ³ N and Ψ:Σ^Fin(N), let G be obtained from F in this way, and use the prime ∧-basis on Σ^Fin(N):

so F  =  λ Φ.G(λℓ.Φβ^ℓ)  =  λ Φ.∃ L. F A_L ∧ ∀ℓ∈ L.Φβ^ℓ.         ▫

Lemma 8.10 If an object X has an effective basis (βⁿ,A_n) then its topology Σ^X has a prime lattice basis (D^L,λ F.Fγ_L), indexed by L:Fin(Fin N), where

Proof    By Lemma 7.4, there is an embedding i:X↣Σ^N with Σ-splitting I by

For F:Σ^ΣX, let F ≡ F·Σⁱ ≡ λΨ.F(λ x.Ψ(i x)) :Σ³ N, so F· I=F·Σⁱ· I=F. Then

since the given formulae are γ_L=Σⁱ A_L and D^L=λφ.∀ℓ∈ L.Iφβ^ℓ.         ▫

Theorem 8.11 Every definable (or locally compact, cf. Remark 6.3) object X has a lattice basis, indexed by Fin(Finℕ), and is a Σ-split subobject of Σ^ℕ. Moreover, Σ^X is stably locally compact, as it has a prime lattice basis (cf. Proposition 6.16).         ▫

Remark 8.12 This is a “normal form” theorem, and, like all such theorems, it can be misinterpreted. It is a bridge over which we may pass in either direction between λ-calculus and a discrete encoding of topology, not an intention to give up the very pleasant synthetic results that we saw in [C]. In particular, we make no suggestion that either arguments in topology or their computational interpretations need go via the list or subset representation (though [JKM99] seems to have this in mind). Indeed, subsets may instead be represented by λ-terms [E]. It is simply a method of proof, and is exactly what we need to connect synthetic abstract Stone duality with the older lattice-theoretic approaches to topology, as we shall now show.