3  Beck’s theorem

Now we relate subspaces as we have just described them to Stone duality as presented in Section 1. In the abstract setting, the diagrams shown there are as follows, where Alg is the category of Eilenberg–Moore algebras for the monad induced by the adjunction Σ⁽⁻⁾⊣Σ⁽⁻⁾.

We shall show that subspaces (i.e. certain equalisers) exist in S and carry the subspace topology iff (idempotents split and) the functor S^op→Alg is an equivalence of categories. This functor is full and faithful iff all objects are sober (Theorem A 4.10), so our task in this paper is to say when it is essentially surjective. In fact we shall construct the pseudo-inverse functor. The argument works though the proof of Beck’s theorem in our special case.

Definition 3.1 An algebra (A,α) is spatial if there is some algebra isomorphism

Recall from Lemma A 4.3 that a map H:A→Σ^U (not necessarily an isomorphism) is a homomorphism iff its double exponential transpose P has equal composites

so our first attempt at spatiality of (A,α) is to form this equaliser [Fak70]. Afterwards we have to find out when H is an isomorphism.

Proposition 3.2 The contravariant functor X↦(Σ^X,Ση_X):S^op→Alg has a symmetric adjoint on the right, called pts, so

iff for each algebra (A,α) the equaliser

exists in S.

Proof    By the foregoing argument, there must also be a correspondence with maps

but this is just the universal property of the equaliser.         ▫

The inverse functor pts:Alg→S^op takes the algebra A to the “set” Alg(A,Σ) of homomorphisms, just as the forward one took the object X to the function-space S(X,Σ). (Remark 7.4 explains how Alg(A,B) can sometimes be defined as an object of S, rather than as an external hom-set.)

Theorem 3.3 The contravariant adjunction of Σ⁽⁻⁾ and pts is an equivalence between S^op and Alg iff all objects of S are sober and all algebras in Alg are spatial.

Proof    Sobriety and spatiality merely say that the units of the symmetric adjunction,

are isomorphisms.         ▫

More particularly, without assuming that all objects are sober, the functor pts:Alg^op→S is full and faithful (making Alg^op reflective in S) iff all algebras are spatial. Joachim Lambek and Basil Rattray considered this situation abstractly (writing Q A for our Σ^{pts A}), together with applications to Abelian categories and elementary toposes [LR75]. More recently, Giuseppe Rosolini connected their results with topos models of synthetic domain theory [BR98a].

We can characterise spatiality in terms more like those of the previous section.

Proposition 3.4 (A,α)≅Σ^X iff there are i:X→Σ^A and I:Σ^X→Σ² A such that

In this case, i:X=pts(A,α)→Σ^A is the equaliser in Proposition 3.2, and Σ⁽⁻⁾ takes it to a split coequaliser.

Proof    If H:A≅Σ^X is an isomorphism of algebras then its double exponential transpose i ≡ η_X;Σ^H is prime, and we may put I ≡ H⁻¹;η_A=η_Σ^X;Σ² H⁻¹. Then

Conversely, if i is prime then its double transpose H≡η_A;Σⁱ is a homomorphism, and H⁻¹=I;α because

since i, being prime, has equal composes with Σ^α and η_Σ^A.

To show that X is the equaliser, consider P:Γ→Σ^A⇉Σ³ A. The double transpose K:A≡Σ^X→Σ^Γ of P is a homomorphism, so, since X is sober, K=Σ^k, where k:Γ→ X mediates to the equaliser. The image of the equaliser diagram under Σ⁽⁻⁾ is the split coequaliser shown above.         ▫

Remark 3.5 In the λ-calculus, these equations are

The η-equation, which says that Σ^X is a retract of A, was discussed in the previous section: it makes X a Σ-split subspace of Σ^A.

The β-equation makes H:A↣Σ^X a subalgebra that is “U-split” in Beck’s language, i.e. split by a function that need not be a homomorphism. This property says that there are enough points to distinguish the elements of A, considered as “open subsets” of X.

Remark 3.6 The same caveat applies to our definition of “spatial” algebras as to that of “sober” spaces in Remark A 5.10: the correspondence with the lattice-theoretic notion in [Joh82, Section II 1.5] is a conceptual one rather than a theorem. In particular, recall from [Joh82, Theorem VII 4.3] that (using the axiom of choice) any distributive continuous lattice A has enough points (completely coprime filters) in the classical sense. All algebras over LKLoc are spatial in the constructive sense that there are enough generalised “points” Γ→pts(A,α), cf. [Vic95].

Beck’s theorem and our treatment of subspaces consider the maps and equations in the main equaliser diagram, without requiring the objects to be Σ² A, Σ³ X, etc.

Definition 3.7 A parallel pair u,v:Y⇉ Z in S is called a Σ-split pair if there is some map (not necessarily a homomorphism) J:Σ^Y→Σ^Z such that

Notice that we just mark one of the maps with a hook, to emphasise the fact that the conditions are not symmetrical in u and v.

It is helpful to see these equations expressed in other ways. Using Notation 2.11, they are

Mixing application with categorical composition, we have

Using the λ-calculus, the equations are

We shall need the equaliser i:X→ Y of u and v, for which we would like Σⁱ:Σ^Y→Σ^X also to be the coequaliser of Σ^u and Σ^v. In this case there is a (unique) map I:Σ^X→Σ^Y with I;Σⁱ=id_Σ^X and Σⁱ;I=J;Σ^v.

Reversing the arrows, there is a similar notion of Σ-split coequaliser (Section 11), whilst (unqualified) split equalisers and coequalisers also arise, in which the equations already hold at the base level, without applying the functor Σ⁽⁻⁾. Split (co)equalisers are absolute in the sense that, being equationally defined, they are preserved by all functors. Absolute coequalisers were first studied by Robert Paré [Par71]. Examples of absolute pushouts may be found in Section 7, [Tay99, Exercise 5.3] and [D].

We construct the equaliser of a split pair by splitting an idempotent (Remark 4.1). In particular, Σ^X splits E ≡ Σ^v;J. Conversely, any idempotent e:Y→ Y gives rise to a split pair (e,id), with J ≡ E ≡ Σ^e, so such splittings are necessary.

There is no greater generality in supposing that i is split only after further iteration of the functor Σ⁽⁻⁾, since if I;Σ³ i=id then I;Σⁱ=id by the unit law, where I ≡ η_Σ^X;I;Σ^η_Y.

Proposition 3.8 If the functor pts exists, all objects are sober and idempotents split, then S has equalisers of all Σ-split pairs. If, additionally, all algebras are spatial, Σ⁽⁻⁾ takes these equalisers to (split) coequalisers.

Conversely, if S has equalisers of all Σ-split pairs, and Σ⁽⁻⁾ takes them to coequalisers, then all algebras are spatial.

Proof    Let u,v:Y⇉ Z have splitting J:Σ^Z→Σ^Y, so that E ≡ Σ^v;J is an idempotent on Σ^Y, and let A be its splitting, as in the top rows of the diagrams. Since this coequaliser is absolute, Σ² A is also a coequaliser, so the structure α may be obtained as the mediator; similar arguments involving Σ⁴A show that it satisfies the equations for an Eilenberg–Moore algebra.

I claim that pts(A,α) is the equaliser of u and v.

All composites pts(A,α)→Σ⁴ Y are equal, so they factor through η_Y since Y is sober. This defines the dotted map. It has equal composites with u and v because all composites pts(A,α)→Σ² Z are equal and η_Z is mono.

Any test map Γ→ Y having equal composites with u and v also has equal composites with Σ² u and Σ² v, since η is natural, so it factors through their equaliser, Σ^A. For the same reasons it has equal composites with Σ^A⇉Σ³ A, and so factors through their equaliser pts(A,α). The mediator is unique because i and Σ^q are mono.

Now apply Σ⁽⁻⁾ to the left-hand diagram, so Σ^pts(A,α)≅ A and Σⁱ≅α by Theorem 3.3 since A is spatial. Then Σ⁽⁻⁾ takes the top two rows of the diagram on the left to the one on the right.

Since pts is itself a Σ-split equaliser, the converse follows from Proposition 3.4.         ▫

Remark 3.9 Because of the fact that Σ⁽⁻⁾ takes it to the coequaliser of Σ^Y⇇Σ^Z, the diagram X→ Y⇉ Z is also an equaliser in HS, i.e. with respect to “second class” test maps F:Γ−× Y⇉ Z (Notation 2.11).

This is in contrast to the situation for products, where the failure of the extension of the universal property from S to HS is essentially related to the interpretation of computational effects [Thi97a]. The fact that equalisers are valid even in the presence of such effects may be regarded as the categorical justification of the use of Floyd–Hoare logic for imperative as well as functional programs.

It is still not clear precisely what the exactness properties of Σ⁽⁻⁾ should be, as not all equalisers are taken to coequalisers:

Example 3.10 (Steven Vickers) Suppose that S has disjoint coproducts, as is the case for Set and LKSp, and also in the abstract situation by Theorem 11.8. Then

is an equaliser (where swap interchanges the elements of 2), but Σ⁽⁻⁾ takes it to

where swap interchanges the components of the product.         ▫

We can now prove the intuitionistic form of Stone duality for locally compact locales.

Theorem 3.11 LKLoc is monadic.

Proof    We must show that every object is sober, that equalisers of Σ-split pairs exist, and that Σ⁽⁻⁾ takes them to coequalisers. Recall from the theory of locales and continuous lattices [GHK++80, Joh82] that the topology on a locally compact locale is a distributive continuous lattice, whilst the category Cont of continuous lattices and Scott continuous functions is fully embedded (via the Scott topology) as a subcategory of LKLoc that is closed under retracts.

The equaliser diagram of locales involved in the definition of sobriety gives rise to diagram of frames shown above, where ↞ denotes a frame homomorphism and ↣ a Scott continuous function. This is a split coequaliser in Cont and so ā fortiori a coequaliser in LKFrm, i.e. an equaliser in LKLoc.

Now let u,v:Y⇉ Z be a Σ-split pair in LKLoc. We follow it around the diagram of categories and functors above.

E ≡ J;Σ^v is a Scott continuous idempotent on the continuous frame Σ^Y, so it is split by some continuous lattice Q. Hence

is a split coequaliser diagram in LKLoc, although we may just as well see it as being in Cont or Set.

The forgetful functor U:Frm→Set, being monadic [Joh82, Theorem II 1.2], creates this coequaliser in Frm, so the lattice Q is actually a frame, and the map Σ^Y↠ Q is a frame homomorphism. This means that Q≅Σ^X for some locale X, which is locally compact since Q is continuous, and q ≡ Σⁱ. Hence the diagram is a coequaliser in LKFrm, so X is the equaliser in LKLoc, which Σ⁽⁻⁾ takes to the original split coequaliser.         ▫

We conclude our introductory discussion with an example of a non-spatial algebra.

Classically, the two-point set classifies subsets in Set, open subsets in LKSp (when it is given the Sierpiński topology), and upper subsets in Pos (when it is given the order ⊥<⊤). The monad may therefore be defined on Pos using this object, which we call Υ.

Example 3.12 In (Pos,Υ), all objects are sober classically but not intuitionistically (Remark C 5.10(c)). Pos does not have the monadic property, because the unit interval, A=[0,1] with the usual arithmetical order, is an Eilenberg–Moore algebra (in a unique way) that does not have enough points.

This discussion of [0,1] extends that in [FW90, Example 9]. In fact, the algebras for this version of the monad are constructively completely distributive lattices [MRW02].

Proof    Classically, the upper sets of A are of the form (a,1] or [a,1]. Indeed Σ^{A· n}=A^op·(n+1), where A· n is A×n with the lexicographic order: <a,i>≤<b,j> if a< b, or a=b and i≤ j.

The maps we’re interested in act as the identity on the real part, and as shown above on the numerical part.         ▫