   ## 9  Basic corollaries

Making use of the availability of bases for all definable objects, this section establishes the basic properties that justify the claim that abstract Stone duality is an account of domain theory and general topology, at least in so far as its morphisms are continuous functions. We first prove something that was claimed in Remark 4.8.

Proposition 9.1 Let M be an overt discrete object with effective basis (βn,An) indexed by an overt discrete object N. Then M is the subquotient of N by an open partial equivalence relation.

Proof    Write nx for n:Nx:MAn{x}∧ βn x (using discreteness of M) and N′={n ∣ ∃ x.nx}⊂ N, which is open, using overtness.

Then, using the basis expansion of open {x},

⊤ ⇔ (x=M x)  ⇔
 ⎧ ⎨ ⎩ x ⎫ ⎬ ⎭
(x)  ⇔ ∃ n.An
 ⎧ ⎨ ⎩ x ⎫ ⎬ ⎭
∧βn x  ⇔ ∃ n.n⊩ x,

so every point x:M has some code n:N′. The latter belongs only to x since

n⊩ x∧ n⊩ y
An
 ⎧ ⎨ ⎩ x ⎫ ⎬ ⎭
∧βn x∧ An
 ⎧ ⎨ ⎩ y ⎫ ⎬ ⎭
∧βn y

An
 ⎧ ⎨ ⎩ x ⎫ ⎬ ⎭
∧ βn y

(∃ n.An
 ⎧ ⎨ ⎩ x ⎫ ⎬ ⎭
∧βny

 ⎧ ⎨ ⎩ x ⎫ ⎬ ⎭
y  ⇔  (x=M y).

Hence N′→ΣM by n↦λ x.nx factors through {}:M↣ΣM, and M is N/∼ where (mn)≡(∃ x.mxnx) [C].         ▫

We leave it as an exercise to define partial equivalence relations on List (N) whose quotients are List (M) and K(M).

Corollary 9.2 Every definable overt discrete object is a subquotient of ℕ by an open partial equivalence relation.         ▫

This does not restrict how “big” overt discrete objects can be in general models of ASD: for example, ℵ1 still belongs to the classical model. It simply says that, having required certain base types to be overt discrete, as we did with ℕ in Axiom 4.4, the additional overt discrete objects that can be constructed from them are no bigger.

Corollary 9.3 In the free model, if an object X has a basis indexed by any overt discrete object M then it has one indexed by ℕ.

Proof    Let n:ℕ,  m:Mnm be the relation defined in the Proposition and (βm,Am) the basis on X. Define

 γn  ≡  λ x.∃ m.n⊩ m∧βm x   and   Dn  ≡  λφ.∃ m.n⊩ m∧ Amφ.

So γnm and Dn=Am if nm, but γn=⊥ and Dn=⊥ if nN′. Then, using the properties of ⊩, (γn,Dn) is an effective basis because

 ∃ n. Dnφ ∧ γn x ⇔ ∃ n m m′.n⊩ m∧ Amφ∧ n⊩ m′∧βm′ x ⇔ ∃ m. Amφ∧βm x  ⇔ φ x          ▫

The next goal is Scott continuity, i.e. preservation of directed joins. Recall from Definition 4.13 that these are defined in terms of a structure (S,0,+) that indexes two families

 s:S ⊢ αs:Σ  and   φs:ΣX.

Lemma 9.4 Γ, ℓ:Fin(M) ⊢ (∀ m∈ℓ.∃ s:Ss∧φs m)  ⇔  (∃ s:Ss∧∀ m∈ℓ.φs m) .

Proof    We have to show ⇒, as ⇐ is easy. For the base case, ℓ≡ 0, put s≡ 0. For the induction step, ℓ′=m::ℓ, suppose by the induction hypothesis that

 αt∧φt m    ∧   αs∧∀ m∈ℓ.φs m

Put us+t:S, so αu⇔αs+t⇔αs∧αt and φst≤φu, so we have αu∧∀ mm::ℓ.φu m.

This proof is for lists, but a similar induction scheme works for subsets too, cf. [Tay99, Section 6.5]. Since this equational hypothesis is of the form σ⇔⊤, it can be eliminated in favour of an open subobject of the context [E, §2].         ▫

Lemma 9.5 Any Γ⊢F3 N preserves the directed join Γ⊢∃ ss∧ ΦsΣN.

Proof    Using the previous lemma for X≡ ΣN and MFin N,

 F(∃ s.αs∧ Φs) ⇔ ∃ L.F AL∧∀ℓ∈ L.∃ s.αs∧Φsβℓ        Lemma 8.9 ⇔ ∃ L.F AL∧∃ s.αs∧∀ℓ∈ L.Φsβℓ ⇔ ∃ s.αs∧∃ L.F AL∧∀ℓ∈ L.Φsβℓ ⇔ ∃ s.αs∧ F Φs         Lemma 8.9         ▫

Theorem 9.6 Any Γ⊢ FΣX preserves the directed join ∃ ss∧φsX.

Proof    Making the same substitutions as in Lemma 8.10,

 F(λ x.∃ s.αs∧φs x) ⇔ F· I(λ x.∃ s.αs∧ Φs(i x)) ⇔ (F· I·Σi)(∃ s.αs∧ Φs) ⇔ ∃ s.αs∧(F· I·Σi) Φs         Lemma 9.5 ⇔ ∃ s.αs∧ Fφs         similarly         ▫

Corollary 9.7 All FY→ΣX preserve directed joins.         ▫

We can now see the construction in Lemma 8.10 as a composite, of Lemma 8.4 twice and the following result. In order to apply FΣX to the basis decomposition of φ:ΣX, the decomposition must be a directed join.

Lemma 9.8 If X has a ∨-basis then ΣX has a prime ∧-basis.

Proof    For FΣX and φ:ΣX, since the ∨-basis gives a directed join,

 Fφ  ⇔  F(∃ n.Anφ∧βn)  ⇔  ∃ n.Anφ∧ Fβn.

This is the decomposition of F with respect to the prime ∧-basis with

 Bn ≡ An   and   An ≡ λ F.Fβn.

Notice that it reverses the imposed order on the indexing object.         ▫

We can also go up to the second exponential with just one level of lists.

Lemma 9.9 Let (βn,An) be a ∨-basis for X. Then

 Bℓ≡λ F.∀ n∈ℓ.Fβn   and   Aℓ≡λF.F(λφ.∃ n∈ℓ.Anφ)

define a prime ∧-basis for ΣΣX, i.e. we have a basis decomposition

 F:Σ3 X  ⊢ F  =  λ F.∃ℓ. F(λφ.∃ n∈ℓ.Anφ)∧∀ n∈ℓ.Fβn.

Proof    (AnF.Fβn) is a basis and (λφ.∃ n∈ℓ.Anφ,  λ F.∀ n∈ℓ.Fβn) an ∨-basis for ΣX by Lemmas 9.8 and 8.4. Finally, Lemma 9.8 gives the prime ∧-basis for ΣΣX.         ▫

As a corollary, we have another result similar to Corollary 9.2, although this one does restrict the size of overt discrete compact objects. Such objects are called Kuratowski finite: see [E] for more detail. Beware that even finiteness is not the same as being a numeral, for example a Möbius band has a finite set of edges that is locally equal to 2, but this set is not a numeral.

Theorem 9.10 An object N is overt discrete compact iff it is listable, and therefore a quotient of a numeral by an open equivalence relation.

Proof    Expanding the quantifier ∀N using the filter ∨-basis for N indexed by List  N,

 ∀Nφ  ⇔  ∃ℓ.∀ n.n∈ℓ∧∀ m∈ℓ.φ m,

so ⊤⇔∀N⊤⇔∃ℓ.∀ n.n∈ℓ. The numeral is (the length of) ℓ, though we require the Existence Property (cf. Remark 4.11) to pin down its order and so make it a quotient of a numeral.         ▫

As another corollary, we can complete the business of Proposition 5.11 and Lemma 8.2.

Theorem 9.11 Let AY→ΣX and BV→ΣU.

1. If A and B both preserve ⊤ and ∧ then the squares commute. Hence × is a symmetric monoidal structure in the category whose objects are those of S and whose morphisms A:X−× Y are the A that preserve ⊤ and ∧, cfSection A 3. In particular, these maps commute with ∀K, for any compact K.

2. If instead A and B both preserve ⊥ and ∨ then again the squares commute, so × is a symmetric monoidal structure in that category too, and these maps commute with ∃N, for any overt N.

Proof    Lemma 8.2 and Theorem 9.6.         ▫

Corollary 9.12 Closed and compact subobjects coincide in any compact Hausdorff object, whilst open and overt ones agree in any overt discrete object.         ▫   