10 Primes and nuclei

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:Σ³ 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 P⇔ Pφ∧ 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∈ℓ.A_nφ)∧∀ n∈ℓ.Pβⁿ Lemma 9.9
	⇔	∃ℓ. F(λφ.∃ n∈ℓ.A_nφ)∧ P(∀ n∈ℓ.βⁿ) P preserves ∧, ⊤
	⇔	∃ℓ.P(F(λφ.∃ n∈ℓ.A_nφ) ∧∀ n∈ℓ.βⁿ) above
	⇔	P(∃ℓ.F(λφ.∃ n∈ℓ.A_nφ) ∧∀ n∈ℓ.βⁿ)
	⇔	P(λ x.∃ℓ.F(λφ.∃ n∈ℓ.A_nφ) ∧∀ n∈ℓ.(λφ.φ x)βⁿ)
	⇔	P(λ x.F(λφ.φ x)). Lemma 9.9 ▫

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

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:S ⊢ a_s:X be a directed family in X with respect to the intrinsic order (Definition 3.7), then

Γ, s:S ⊢ λφ.φ a_s :Σ^{Σ^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.φ a_s :Σ^{Σ^X}

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

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

By a similar argument, given f:X→ Y, we have f(a_s)≤_Y f a since ψ:Σ^Y provides ψ· f:Σ^X, and if f(a_s)≤ 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:X→ X has a least fixed point, namely

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

Finally, we show that the equations in Lemma 7.15 that characterised the Scott-continuous functions E that are of the form 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 E:Σ^X→Σ^X is called a nucleus if

F:Σ³ 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∧φⁿ) = E(∃ n∈ℓ.α_n∧ Eφⁿ),

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

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

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∧φⁿ)
	=	E((∃ n∈ℓ.α_n∧φⁿ)∨(α_m∧φ^m))
	=	E(E(∃ n∈ℓ.α_n∧φⁿ)∨ E(α_m∧φ^m)) ∨-equation
	=	E(E(∃ n∈ℓ.α_n∧ Eφⁿ)∨ E(α_m∧ Eφ^m)) ind. hyp.
	=	E((∃ n∈ℓ.α_n∧ Eφⁿ)∨ (α_m∧ Eφ^m)) ∨-equation
	=	E(∃ n∈m::ℓ.α_n∧ Eφⁿ) ▫

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

Proof

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

Theorem 10.10 E is a nucleus iff it satisfies

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

Proof We expand F:Σ³ X in the defining equation for a nucleus

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