In this section we prove that focus and description are inter-definable, for the natural numbers. In the following notation, we need to show that φ is a description iff P is prime.
Lemma 10.1 This is a retraction,
cf. the connection between {} and η in [BW85, Lemma 5.1.3] and Lemma C 6.12. ▫
[In fact there is an adjunction or coclosure as shown, since
|
using the Euclidean principle (Remark 2.4) and the substitution rule for equality.]
First, we characterise the image of Σℕ↣ΣΣℕ.
Lemma 10.2 Γ⊢ P:Σ2ℕ is of the form
λ ψ.∃ n.φ[n] ∧ ψ[n]
for some Γ⊢φ:Σℕ
iff it preserves ∃ℕ.
In this case, φ=λ n.P(λ m.n=m).
Proof Suppose that P preserves ∃. Then
|
by the Euclidean principle (Remark 2.4). The other way is easy. ▫
For the rest of this section, P and φ will be related in this way.
Lemma 10.3 P preserves ⊤ iff φ satisfies the existence condition,
and P preserves ∧ iff φ satisfies the uniqueness condition.
Proof For the first, observe that P⊤ ⇔ ∃ n.φ[n]. For the second, if φ[n1]∧ψ1[n1] and φ[n2]∧ψ2[n2] then n1=n2=n by uniqueness. ▫
Proposition 10.4 If P is prime then φ is a description,
and the n.φ[n] satisfies the rules for focusP
(Definition 8.2).
Proof As P is prime, it preserves ⊤, ∧ and ∃ because its double exponential transpose is a homomorphism, in particular with respect to ⊤, ∧ and ∃, as in Proposition 5.5. Also, P=λψ.∃ n.φ[n]∧ψ[n] by the Lemma, so Pψ⇔ψ[the n.φ[n]], which means that the β-rules agree. For the η-rules,
φ= |
| ≡(λ m.m=n) iff P=thunkn≡λψ.ψ[n], |
which are respectively a description and prime, and then (the m.φ[m])=(focusP)=n. ▫
Corollary 10.5
Any overt discrete object that admits definition by description is sober.
In particular, all sets and all objects of any topos are sober.
▫
The converse is the case X=ℕ of Theorem 5.7, that if H:Σℕ→ΣU is a frame homomorphism (i.e. it preserves ⊤, ∧ and ∃) then it is an Eilenberg–Moore homomorphism. Of course, we showed that for LKLoc, by re-interpreting results from the literature, not for our abstract calculus. The proof below depends on (primitive) recursion, so only applies to ℕ rather than to discrete overt spaces in general, although when the whole theory is in place the result will hold for them too. [It is easy to show that if φ is a description then P preserves ⊤, ⊥, ∧ and ∨; then it is prime by Theorem G 10.2.]
But before considering ℕ we have to deal with 2≡{0,1}. As we did not ask for this as a base type in Section 2, ψ:Σ2 may be replaced by <ψ0,ψ1>∈Σ×Σ, and similarly for the type of P. (Alternatively, one could formulate a result with ψ:Σℕ to capture the same point.) See B 11 for further discussion of disjoint unions in abstract Stone duality.
Proposition 10.6 Let α:Σ be decidable,
with β⇔¬α (Definition 9.11). Then
P ≡ λψ.(α∧ψ[0])∨(β∧ψ[1]) |
is prime. This justifies definition by cases: (if α then 0 else 1)≡focusP.
Proof Let Pαβ be the obvious generalisation, so
γ∧ Pαβ = P(γ∧α)(γ∧β) |
by distributivity. The equation that we have to prove for Definition 8.1 may be written
(α∨β)∧F Pαβ ⇔ (α∧F P⊤⊥) ∨ (β∧F P⊥⊤). |
By the Euclidean principle (Remark 2.4) and the lattice laws, we have
|
Lemma 10.7 For any description φ, we define, by primitive recursion,
φ≥[0]≡⊤ φ>[n]≡φ≥[n+1]≡φ≥[n]∧¬φ[n] |
φ<[0]≡⊥ φ≤[n]≡φ<[n+1]≡φ<[n]∨φ[n]. |
Then φ<[n] has the properties of the ordinary arithmetic order, that is, (the m.φ[m])< n, and similarly for the others. ▫
Proposition 10.8 If φ is a description then P is prime,
and focusP satisfies the rules for the n.φ[n].
Proof The idea of the proof is to define a permutation f:ℕ≅ℕ that cycles the witness to 0 and any smaller values up by 1, leaving bigger numbers alone. The function f itself is defined by (cases and) primitive recursion, but it only has an inverse with general recursion. Let
f(n) ≡ | ⎧ ⎪ ⎨ ⎪ ⎩ |
| δ(n,m) ≡ | ⎧ ⎪ ⎨ ⎪ ⎩ |
|
so δ(n,m) ⇔ f(n)=m. The operations Σf and I, defined by
|
are mutually inverse, because, by expanding disjunctions,
|
Thus Σf is a homomorphism, as is its inverse I by Proposition 3.5. But so too is evaluation at 0, so
ψ ↦ θ[0] ≡ ∃ n.δ(0,n) ≡ ∃ n.φ[n]∧ψ[n] |
is a homomorphism, and P is prime. The β- and η-rules agree as before. ▫
Remark 10.9
Sobriety says that the functor Σ(−):Cop→A
in Definition 4.1 is full and faithful.
But in this proof we only used the fact that it reflects invertibility,
so it suffices to assume that ℕ is replete.
Then f−1 is the diagonal mediator that is provided by
the orthogonality property
[Hyl91, Tay91].
Corollary 10.10 H:Σℕ→ΣU is an Eilenberg–Moore
homomorphism iff it preserves ⊤, ∧ and ∃. ▫
This result can be extended from ℕ to higher types on the assumption of the continuity axiom (Remark 2.6). Hence there is a version of Theorem 5.7 that links the notions of homomorphism and sobriety that we have introduced entirely abstractly using the λ-calculus with those that arise from the ℕ-indexed lattice structure in Remarks 2.4ff. Although the proof would only require one more section, it begins to make serious use of domain-theoretic ideas, and so properly belongs in a discussion of that subject [F][G]. Besides, surprisingly much progress can be made with the development of topology without the extra axiom.