   ## 10  Primes and nuclei

In this section we prove the finitary lattice-theoretic characterisations of primes and nuclei that we announced in Remark 3.4.

Since homomorphisms of the four lattice connectives also preserve directed joins, we might expect them to be frame homomorphisms. However, they only preserve joins indexed by overt objects, not “arbitrary” ones. On the other hand, objects and inverse image maps are defined in Abstract Stone Duality as algebras and homomorphisms for the monad corresponding to Σ(−)⊣Σ(−), rather than for an infinitary algebraic theory.

We actually consider “Curried” homomorphisms.

Definition 10.1 The term Γ⊢ PΣX is prime (Definition A 8.1) if

 Γ,F:Σ3 X ⊢ F P ⇔ P (λ x.F(λφ.φ x)).

Axiom 2 says that we may then introduce a=focusP such that P=λφ.φ a.

Plainly if P≡λφ.φ a for some a then

 P⊤  ⇔⊤,      P(φ∧ψ)  ⇔  φ a∧ψ a  ⇔  Pφ∧ Pψ

and similarly for ⊥ and ∨. We know that frame homomorphisms (as defined externally using infinitary lattices) agree with Eilenberg–Moore homomorphisms in the case of the classical models [A, B]. Now we can use bases to prove a similar result for the internal finitary lattice structure in our category. This means that we can import at least some of the familiar lattice-theoretic arguments about topology into our category.

Theorem 10.2 PΣX is prime iff it preserves ⊤, ⊥, ∧ and ∨.

Proof    [⇒] Put F≡λ F.Fφ∧ Fψ, so F PPφ∧ Pψ, whilst

 P(λ x.F(λφ.φ x))  ⇔  P(λ x.φ x∧ψ x)  ⇔  P(φ∧ψ).

The other connectives are handled in the same way.

[⇐] First note that, using Axiom 3.6 for P and α, and P⊥⇔⊥,

 P(α∧φ)  ⇔   P⊥∨α∧ Pφ  ⇔  α∧ Pφ.

Second, P commutes with ∃ by Theorem 9.11(b), so

 F P ⇔ ∃ℓ. F(λφ.∃ n∈ℓ.Anφ)∧∀ n∈ℓ.Pβn         Lemma 9.9 ⇔ ∃ℓ. F(λφ.∃ n∈ℓ.Anφ)∧ P(∀ n∈ℓ.βn)         P preserves ∧, ⊤ ⇔ ∃ℓ.P(F(λφ.∃ n∈ℓ.Anφ) ∧∀ n∈ℓ.βn)         above ⇔ P(∃ℓ.F(λφ.∃ n∈ℓ.Anφ) ∧∀ n∈ℓ.βn) ⇔ P(λ x.∃ℓ.F(λφ.∃ n∈ℓ.Anφ) ∧∀ n∈ℓ.(λφ.φ x)βn) ⇔ P(λ x.F(λφ.φ x)).         Lemma 9.9         ▫

Corollary 10.3 HX→ΣY is an Eilenberg–Moore homomorphism iff it is a lattice homomorphism. In this case, it is of the form Hf for some unique f:YX.         ▫

We have in particular a way of introducing points of an object by finitary lattice-theoretic arguments. By this method we can derive a familiar domain-theoretic result, but beware that, as the objects of our category denote locally compact objects and not merely domains, the order by no means characterises the objects and morphisms.

Theorem 10.4 Every object has and every morphism preserves directed joins.

Proof    [Joh82, Lemma II 1.11] Let Γ,  s:Sas:X be a directed family in X with respect to the intrinsic order (Definition 3.7), then

 Γ,  s:S  ⊢ λφ.φ as :ΣΣX

is a directed family of primes. But primes are characterised lattice-theoretically, and the property is preserved by directed joins (Theorem 9.6 for F), so

 Γ  ⊢ P ≡ λφ.∃ s.φ as :ΣΣX

is also prime, and P=λφ.φ a, where afocusP:X.

I claim that this is the join of the given family. By Definition 3.7, the order relation asX a means λφ.φ as≤λφ.φ aP, which we have by the definition of P, whilst similarly if Γ,  s:Sasb then λφ.φ as≤λφ.φ b so P≤λφ.φ b as P is the join, and then ab.

By a similar argument, given f:XY, we have f(as)≤Y f a since ψ:ΣY provides ψ· fX, and if f(as)≤ b then f(a)≤ b, so f preserves the join.         ▫

Corollary 10.5 Suppose that an object X has a least element ⊥ in its intrinsic order. Then any f:XX has a least fixed point, namely

 a ≡ focus(λφ.∃ n.φ an),   where    a0 ≡ ⊥  and    an+1 ≡  f an.                 ▫

Finally, we show that the equations in Lemma 7.15 that characterised the Scott-continuous functions E that are of the form I·Σi for a Σ-split sublocale are also valid for Σ-split subobjects in abstract Stone duality.

Definition 10.6 Recall from Definition B 4.3 that EX→ΣX is called a nucleus if

 F:Σ3 X ⊢  E(λ x.F(λφ. φ x))  =  E(λ x.F(λφ. Eφ x)):ΣX.

(This equation arises from Beck’s monadicity theorem, and is applicable without assuming any lattice structure on Σ.)

Lemma 10.7 If E is a nucleus then

 φ,ψ:ΣX  ⊢    E(φ∧ψ) = E(Eφ∧ Eψ)   and   E(φ∨ψ)=E(Eφ∨ Eψ).

Proof    Putting F≡λ F.Fφ∧ Fψ,

 E(λ x.F(λφ.φ x))  =  E(λ x.φ x∧ ψ x)  =  E(φ∧ψ)          LHS
 E(λ x.F(λφ.Eφ x))  =  E(λ x.Eφ x∧ Eψ x)  =  E(Eφ∧ Eψ),          RHS

are equal. The argument for ∨ is the same.         ▫

For the converse, first observe that the equations allow us to insert or remove Es as we please in any sub-term of a lattice expression, so long as E is applied to the whole expression. In particular, Eφ=E(Eφ) and E(φ∨ψ∨θ)=E(Eφ∨ Eψ∨θ) (sic).

Lemma 10.8 Although we needn’t have E⊤=⊤ or E⊥=⊥, we may extend the binary ∨-formula to finite (possibly empty) sets ℓ:Fin(N):

 E(∃ n∈ℓ.αn∧φn)  =   E(∃ n∈ℓ.αn∧ Eφn),

where n:N⊢ αn:Σ and φnX. Similarly but more simply, from the ∧-equation,

 E(∀ n∈ℓ.φn)  =  E(∀ n∈ℓ. Eφn).

Proof    The base case of the induction, ℓ≡ 0, is E⊥=E⊥, and the next case is

 E(α∧φ)  =  E⊥∨α∧ Eφ  =  E⊥∨α∧ E(Eφ)  =  E(α∧ Eφ)

by the Phoa principle. For the induction step [E, §2],

 E(∃ n∈m::ℓ.αn∧φn) = E((∃ n∈ℓ.αn∧φn)∨(αm∧φm)) = E(E(∃ n∈ℓ.αn∧φn)∨ E(αm∧φm))         ∨-equation = E(E(∃ n∈ℓ.αn∧ Eφn)∨ E(αm∧ Eφm))         ind. hyp. = E((∃ n∈ℓ.αn∧ Eφn)∨ (αm∧ Eφm))         ∨-equation = E(∃ n∈m::ℓ.αn∧ Eφn)         ▫

Lemma 10.9 The ∃ equation extends by Scott continuity (Proposition 9.6).

Proof

 E(∃ n:N.αn∧φn) = E(∃ℓ:Fin N.∃ n∈ℓ.αn∧φn) = ∃ℓ.E(∃ n∈ℓ.αn∧φn)         Proposition 9.6 = ∃ℓ.E(∃ n∈ℓ.αn∧ Eφn)         Lemma 10.8 = E(∃ n:N.αn∧ Eφn)         similarly         ▫

Theorem 10.10 E is a nucleus iff it satisfies

 φ,ψ:ΣX  ⊢    E(φ∧ψ) = E(Eφ∧ Eψ)   and   E(φ∨ψ)=E(Eφ∨ Eψ).

Proof    We expand F3 X in the defining equation for a nucleus

 E(λ x.F(λφ.Eφ x)) = E(∃ L.F AL ∧∀ℓ∈ L. Eβℓ)         Proposition 9.8 = E(∃ L.F AL ∧ E(∀ℓ∈ L.Eβℓ))         Lemma 10.9 = E(∃ L.F AL ∧ E(∀ℓ∈ L.βℓ))         Lemma 10.8 = E(∃ L.F AL ∧∀ℓ∈ L.βℓ)         Lemma 10.9 = E(λ x.F(λφ.φ x))         Proposition 9.8         ▫   