   ## 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 SopAlg 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):SopAlg 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:AlgSop 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 Sop 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,

 X→pts(ΣX,ΣηX)     and     H:A→Σpts A,

are isomorphisms.         ▫

More particularly, without assuming that all objects are sober, the functor pts:AlgopS is full and faithful (making Algop 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 IX→Σ2 A such that

 i  is prime,     I;Σi=idΣX   and   Σi;I=α;ηA≡ηΣ2 A;Σ2α.

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 ≡ ηXH is prime, and we may put IH−1AΣX2 H−1. Then

 I;Σi   =  ηΣX;Σ2 H−1;Σ2 H;ΣηX  =  ηΣX;ΣηX  =  id
 Σi;I  =  Σ2 H;ΣηX;H−1;ηA  =  α; H;H−1;ηA  =   α; ηA.

Conversely, if i is prime then its double transpose H≡ηAi is a homomorphism, and H−1=I;α because

 ηA;Σi;I;α  =  ηA;α;ηA;α  =  id
 I;α;ηA;Σi  =  I;ηΣ2 A;Σ2α;Σi  =  I;ηΣ2 A;ΣηΣA;Σi  =  I;Σi  =  id

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

To show that X is the equaliser, consider P:Γ→ΣA⇉Σ3 A. The double transpose K:A≡ΣX→ΣΓ of P is a homomorphism, so, since X is sober, Kk, 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

 x:X,  φ:ΣX ⊢ (Iφ)(i x)   ⇔   φ(x)     (η) F:ΣA, F:Σ2 A ⊢ I(λ x.F(i x))(F)   ⇔   F(αF).     (β)

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 Σ2 A, Σ3 X, etc.

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

 J;Σu  =  idΣY     and     Σu;J;Σv  =  Σv;J;Σv.

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

u;
 J
=  id     and    v;
 J
;u  =  v;
 J
;v.

Mixing application with categorical composition, we have

 u;J(ψ)  =  ψ      and     v;J(u;θ)  =  v;J(v;θ).

Using the λ-calculus, the equations are

 y:Y,  ψ:ΣY ⊢ (Jψ)(u y)   ⇔   ψ(y) y:Y,   θ:ΣZ ⊢ J(λ y.θ(u y))(v y)   ⇔   J(λ y.θ(v y))(v y).

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

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:YY gives rise to a split pair (e,id), with JE ≡ Σ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 I3 i=id then Ii=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:YZ have splitting JZ→Σ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, Σ2 A is also a coequaliser, so the structure α may be obtained as the mediator; similar arguments involving Σ4A 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,α)→Σ4 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,α)→Σ2 Z are equal and ηZ is mono.

Any test map Γ→ Y having equal composites with u and v also has equal composites with Σ2 u and Σ2 v, since η is natural, so it factors through their equaliser, ΣA. For the same reasons it has equal composites with ΣA⇉Σ3 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 Σi≅α 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 XYZ is also an equaliser in HS, i.e. with respect to “second class” test maps F:Γ−× YZ (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.

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:YZ be a Σ-split pair in LKLoc. We follow it around the diagram of categories and functors above.

EJv 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:FrmSet, being monadic [Joh82, Theorem II 1.2], creates this coequaliser in Frm, so the lattice Q is actually a frame, and the map ΣYQ is a frame homomorphism. This means that Q≅ΣX for some locale X, which is locally compact since Q is continuous, and q ≡ Σi. 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=Aop·(n+1), where A· n is A×n with the lexicographic order: <a,i>≤<b,j> if a< b, or a=b and ij. The maps we’re interested in act as the identity on the real part, and as shown above on the numerical part.         ▫   