   ## 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 (βn,An) and (γm,Dm) on X and Y. Then, on X× Y, we define

 є(n,m) ≡ λ x y.βn x∧γm y F(n,m) ≡ λθ:ΣX× Y.Dm(λ y.An(λ x.θ(x,y))), Then         θ(x,y) ⇔ ∃ n.An(λ x′.θ(x′,y))∧βn x ⇔ ∃ n m. Dm(λ y′.An(λ x′.θ(x′,y′))) ∧γm y∧βn x ⇔ ∃ (n,m). F(n,m)θ∧є(n,m)(x,y)         ▫

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 An and Dm 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

 A(λ x.D(λ y.θ x y))  ⇔  D(λ y.A(λ x.θ x y))

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

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

 A(λ x.D(λ y.φ x∧ψ y)) ⇔ A(λ x.D⊥∨φ x∧ Dψ)         Phoa for D wrt φ x ⇔ A(λ x.φ x∧ Dψ)∨ (D⊥∧ A⊤)         Phoa for A wrt D⊥ ⇔ A⊥∨(Dψ∧ Aφ)∨(D⊥∧ A⊤)         Phoa for A wrt Dψ.

This would have the required symmetry if we had

 A(D⊥)  ≡  A⊥∨(D⊥∧ A⊤)  ⇔  (A⊥∧ D⊤)∨ D⊥   ≡  D(A⊥).

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

 A(λ x.D(λ y.φ x∨ψ y))   ⇔  D(λ y.A(λ x.φ x∨ψ y))

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,

 θ x y  ⇔  (φ1 x∧ψ1 y)  ∨  (φ2 x∧ψ2 y)  ∨  (φ3 x∧ψ3 y).

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,

 θ x y ⇔ (φ1 x∨φ2 x∨φ3 x)  ∧  (φ1 x∨φ2 x∨ψ3 y)  ∧ (φ1 x∨ψ2 y∨φ3 x)  ∧  (φ1 x∨ψ2 y∨ψ3 y)  ∧ (ψ1 y∨φ2 x∨φ3 x)  ∧  (ψ1 y∨φ2 x∨ψ3 y)  ∧ (ψ1 y∨ψ2 y∨φ3 x)  ∧  (ψ1 y∨ψ2 y∨ψ3 y).

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 φ=φ1∨φ2 and ψ=ψ3. 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 (βn,An), define

 γℓ ≡  λ x.∃ n∈ℓ.βn x      Dℓ ≡  λφ.∀ n∈ℓ.Anφ.

Then φ = ∃ n.Anφ∧βn ≤  ∃ℓ.Dφ∧γ using singleton lists. Conversely,

 ∃ℓ.Dℓφ∧γℓ = ∃ℓ.(∀ n∈ℓ.Anφ)∧(∃ m∈ℓ.βm) = ∃ℓ.∃ m∈ℓ.(∀ n∈ℓ.Anφ)∧βm ≤ ∃ℓ.∃ m∈ℓ.Amφ∧βm  =  φ.

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

 (ℓ≼ℓ′)  ≡  (ℓ⊂ℓ′)  ≡  ∀ n∈ℓ.n∈ℓ′.

Finally, if the An 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:

 i x = λξ.∃ n.βn x ∧ ξ n I φ = λΦ.∃ℓ.Φ(λ n.n∈ℓ) ∧ ∀ n∈ℓ.Anφ γℓx ⇔ ∃ n∈ℓ.βn x  ⇔  i x (λ n.n∈ℓ)  ⇔  i xπℓ Dℓφ ⇔ ∀ n∈ℓ.Anφ  ⇔  Iφ (λψ.∀ n∈ℓ.ψ n)  ⇔  Iφ[ℓ] φ x ⇔ ∃ℓ.Iφ[ℓ]∧ i x πℓ        ▫

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

Proof    We are given β1=⊤ and βn∧βmnm.

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

 ℓ⋆ℓ′  ≡  flatten  (map ℓ (λ n.map ℓ′(λ m.n⋆ m))),

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

 βℓ⋆ℓ′  ≡  (∃ n∈ℓ.∃ m∈ℓ′.βn⋆ m)  =  (γℓ∧γℓ′)

by distributivity in ΣX, whilst γ{|1|}≡β1 and D{|1|}A1 (where {|1|} is the singleton list) serve for γ1 and D1. (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 Anφ means KnU then Aφ means that ∃ n∈ℓ.KnU, 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 Anm actually captures the intersection of the compact subobjects.

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

Nprime
βn
 ⎧ ⎨ ⎩ n ⎫ ⎬ ⎭
≡λ m.(n=m)
An≡ηN(n)≡λξ.ξ n
Nfilter ∨β≡λ m.m∈ℓA≡λξ.∀ m∈ℓ.ξ m
NlatticeβL≡λ m.∀ℓ∈ L.m∈ℓAL≡λξ.∃ℓ∈ L.∀ m∈ℓ.ξ m
ΣNprime ∧B≡ AA≡ ηΣNβ≡ λ Φ.Φ(λ m.m∈ℓ)
ΣNfilter latticeBL ≡ ALAL ≡ λ Φ.∀ℓ∈ L.Φ(λ m.m∈ℓ)

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

 BL≡AL≡λ Φ.∀ℓ∈ L.Φβℓ  and   AL ≡ ηΣ2 NAL ≡λF.F AL,

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

 F:Σ3 N,  Φ:ΣΣN  ⊢    F Φ  ⇔  ∃ L:Fin(Fin N).  F AL ∧ ∀ℓ∈ L. Φβℓ.

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

 Φ↦λℓ.Φβℓ  and   λξ.∃ℓ.Ψℓ∧∀ n∈ℓ.ξ n↤ Ψ,

so Σ3 N◁Σ2Fin(N) by

 F↦λ Ψ.F(λξ.∃ℓ.Ψℓ∧∀ n∈ℓ.ξ n)   and   λ Φ.G(λℓ.Φβℓ)↤G.

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

 G Ψ ⇔ ∃ L:FinFin(N).G(λℓ.ℓ∈ L)∧∀ℓ∈ L.Ψℓ ⇔ ∃ L. F(λξ.∃ℓ. (λℓ.ℓ∈ L)ℓ∧∀ n∈ℓ.ξ n) ∧  ∀ℓ∈ L.Ψℓ ⇔ ∃ L. F(λξ.∃ℓ∈ L.∀ n∈ℓ.ξ n)  ∧  ∀ℓ∈ L.Ψℓ ⇔ ∃ L. F AL ∧  ∀ℓ∈ L.Ψℓ

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

Lemma 8.10 If an object X has an effective basis (βn,An) then its topology ΣX has a prime lattice basis (DLF.FγL), indexed by L:Fin(Fin N), where

 γL ≡ λ x.∃ℓ∈ L.∀ n∈ℓ.βn x   and   DL ≡ λφ.∀ℓ∈ L.∃ n∈ℓ.Anφ.

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

 i x  ≡  λ n.βn x   and   Iφ ≡  Φ  ≡  λξ.∃ n.Anφ∧ξ n,   so   φ  =  λ x.Φ(i x).

For FΣX, let FF·Σi ≡ λΨ.Fx.Ψ(i x)) :Σ3 N, so F· I=F·Σi· I=F. Then

 Fφ  ⇔  F(Iφ) ⇔ ∃ L. F AL ∧  ∀ℓ∈ L.Iφβℓ        Lemma 8.9 ⇔ ∃ L. F(Σi AL) ∧  ∀ℓ∈ L.Iφβℓ ⇔ ∃ L. FγL ∧  DLφ

since the given formulae are γLi AL and DL=λφ.∀ℓ∈ 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.   