Constructive complete distributivity IV

Robert Rosebrugh^{∗} Department of Mathematics and Computer Science Mount Allison University Sackville, N. B. Canada

R. J. Wood^{∗}

Department of Mathematics, Statistics and Computing Science Dalhousie University Halifax, N. S. Canada

Abstract

A complete lattice L is constructively completely distributive, (CCD), when the sup arrow from down-closed subobjects of L to L has a left adjoint. The Karoubian envelope of the bicategory of relations is biequivalent to the bicategory of (CCD) lattices and sup-preserving arrows. There is a restriction to order ideals and “totally algebraic” lattices. Both biequivalences have left exact versions. As applications we characterize projective sup lattices and recover a known characterization of projective frames. Also, the known characterization of nuclear sup lattices in set as completely distributive lattices is extended to yet another characterization of (CCD) lattices in a topos.

∗Research partially supported by grants from NSERC Canada. Diagrams typeset using Michael Barr’s diagram package. AMS Subject Classification Primary: 06D10 Secondary 18B35, 03G10. Keywords: completely distributive, adjunction, projective, nuclear

Introduction

Idempotents do not split in the category of relations, rel, so it has a non-trivial idempotentsplitting completion, also called Karoubian envelope, kar(rel). Roughly speaking, this paper shows that kar(rel) is equivalent to the category of completely distributive lattices and supremum-preserving arrows and then derives related equivalences as corollaries. The rel we refer to though is rel = rel(E), where E is an arbitrary elementary topos that serves as the base for the entire discusssion and of course the result is proved for “constructively” completely distributive lattices, the subject of this series of papers: [6], [13], [14].

Now the categories of the equivalence mentioned above are both 2-categories, more precisely ord(= ord(E))-categories, so it is obvious that one should make this an ord-result — if it is one and indeed it is. This is not an extra chore. We use adjunction in the ordcategory kar(rel) systematically in our proofs and there is a sense in which these results are ineluctably 2-categorical. It does not even seem extravagant to say that any 1-categorical proof of these results is likely to be “lengthier”. However, because our subject is ordcategorical the reader does not need to be versed in the coherence complexities of general 2-categorical matters.

The objects of kar(rel) are not themselves categories but there is a sense in which they are only a slight generalization of ordered sets and this provides considerable motivation and direction for the use of adjunctions. For example, since each object of kar(rel) belongs to a related ord-category which has finite products we are able to say what it means for an idempotent in rel to have “finite meets” — using the calculus of adjunctions — and such idempotents characterize, in a way which we make precise, the lattices which were called “stably supercontinuous frames” in a recent paper by Banaschewski and Niefield [1]. Indeed this is one of the corollaries of the main result mentioned above. We consider that the point of view on idempotents presented here is likely to be useful elsewhere and while we do not burden this paper with aspects of the theory that are not reasonably germane to our characterizations of various categories of lattices, category theorists should infer a subtext that will appear explicitly in [15]. In particular we hope it is clear to such readers that one can, upon facing general 2-categorical matters, apply similar ideas to the study of categories which are not necessarily ordered sets.

Section 1 sets the stage for the paper by highlighting the ord-categorical aspects of kar(rel) that we need throughout. In particular we show that it is naturally an object of IF as studied in [2]. We do not assume familiarity with that paper but the reader who has read it will doubtless anticipate the direction of the present work. We find it convenient to prove at this early point that IDX = (kar(rel))(1, X) is (CCD) (our usual acronym for constructively completely distributive). In Section 2 we cover quickly some elementary properties of what has been called the “totally below” relation for a complete lattice [1], specializing for the most part to (CCD) lattices. The main result then appears in Section 3. We conclude that section with a construction of the real closed unit interval from the rationals.

An “element” of a complete lattice is said to be totally compact if it is totally below itself and a useful subcategory of (CCD) lattices are those in which each “element” is the supremum of the totally compact elements below it. Such lattices, which we call totally algebraic, are the subject of Section 4. We show that the equivalence of Section 3 restricts to yield an equivalence between totally algebraic lattices with sup preserving arrows and the category idl of ordered objects and order ideals. Also in that section we prove an “adjoint arrow theorem” concerning existence of a right adjoint to a right adjoint to an arrow between (CCD) lattices. It is fairly clearly a specialization to lattices of a more general result, of independent interest, that will be dealt with in [15]. In Section 5 we show that most of the results admit “lex” versions and this allows us to characterize the stably supercontinuous and supercoherent frames of [1]. We extend the work of these authors on projectivity in Section 6. In Section 7 we show that the interesting characterization of completely distributive lattices given by Higgs and Rowe in [7] is constructively equivalent to (CCD). Our proof uses the machinery developed in Section 3. Finally, in Section 8 we discuss briefly adjoint sequences which are longer than that defining (CCD).

Our ordered objects are reflexive and transitive but not necessarily antisymmetric. As in the other papers in this series we use the word “(complete) lattice” in the context of such orders but we define relations and hence ideals in terms of subobjects rather than monomorphisms when working over a topos — as we do here — so lattices such as PX, DX and the IDX, which we introduce here, are in fact antisymmetric. Our rationale for these conventions is explained in [13]. Some “equivalences” that we deal with are biequivalences in the absence of antisymmetry. We point this out as we go.

We are greatly indebted to Steve Vickers for stimulating correspondence on complete distributivity and for reminding us of Raney’s work on idempotent relations in [12]. It is difficult to overestimate Raney’s insights into complete distributivity. We have attempted in Sections 1 and 2 to acknowledge those results which, in non-categorical form, first appeared in [12]. We should also mention the work of Guitart and Riguet, [5], who have proved a constructive, but non-ord-enriched, version of Theorem 17 using methods quite different from ours. Vickers too has proved a version of our Theorem 17 [18]. The results here are fundamentally indebted to Eilenberg and Mac Lane, for without the language of categories Proposition 11, which separates our contributions from those of Raney, is difficult to state succinctly and, more importantly, difficult to even conjecture.

Finally we thank the referee for an inspiring report. In the course of replying to the questions raised we learned considerably more about our subject. We discussed those questions with Bob Paré and we thank him for his insights.

1 Idempotents in categories of relations

If R is a relation from X to A, we write R : X \overline{}A but if a in A is R-related to x in X, we write aRx. (This is consistent with the notational convention for profunctors and the like which holds that the contravariant variable comes from the codomain.)

A relation ⊏ : X \overline{}X is said to be interpolative if x ⊏ y implies (∃z)(x ⊏ z ⊏ y). In terms of relational composition this means that ⊏ ⊆ ⊏ · ⊏ . The containment ⊏ · ⊏ ⊆ ⊏ holds precisely if ⊏ is transitive so an idempotent in rel is a transitive interpolative relation. Of course any order relation, ≤, provides an example of an idempotent. Not all idempotents split in rel so the splitting completion, also known as the Karoubian envelope, kar(rel), is not equivalent to rel. Recall that the objects of kar(rel) are idempotents (X, ⊏) and an arrow R : (X, ⊏) \overline{}(A, ⊏) is a relation R : X \overline{}A such that R · ⊏ = R = ⊏ · R. Thus we have (∃y)(aRy ⊏ x) if and only if aRx if and only if (∃b)(a ⊏ bRx). Since rel is a 2-category, in fact an ord-category, so is kar(rel) — transformations being containments of arrows. This observation is central to our considerations.

Vickers [18] uses the term infosys for an object of kar(rel) and we adopt this name. We refer to the arrows as modules. For Vickers they are the lower approximable semimappings. If X and A are orders then a module is an (order-)ideal as studied in [3]. In the present context the conditions on R : X \overline{}A simplify to aRy ≤ x implies aRx and a ≤ bRx implies aRx. We have full and locally full containments rel[figure] idl[figure] kar(rel) where for the first we regard an object of the base, E, as a discrete ordered object. Recall that a 2-functor is locally fully faithful if each of its effects on hom categories is fully faithful. So an ord-functor F is locally fully faithful precisely when, for parallel f and g, f ≤ g if and only if F f ≤ F g. We also speak of the locally-full sub-ord-category determined by a class of arrows.

If (X, ⊏) and (A, ⊏) are infosyses then any relation R : X \overline{}A gives rise to a module, namely ⊏ · R · ⊏ : (X, ⊏) \overline{}(A, ⊏) which we denote by R_{#}. In particular, if R is f_{∗}, the graph of an arbitrary arrow f : X ⟶ A in E, then we have the module ⊏ · f_{∗} · ⊏ = (f_{∗})_{#} which we abbreviate by f_{#} . It is worth noting that af_{#}x if and only if (∃y)(a ⊏ fy and y ⊏ x). Say that f is below-preserving if y ⊏ x implies fy ⊏ fx. In this case we write f_{+} for f_{#}. If (X, ⊏) is an order and f is below-preserving then af_{+}x simplifies to a ⊏ fx. This is not true of a general below-preserving arrow but the condition that X be an order is not necessary as we will see in Section 4. We follow the convention of reserving the word map for an arrow with a right adjoint and write f^{∗} for the right adjoint of f_{∗} in rel. It is well known that map(rel) is isomorphic to E and we can freely identify the two, abbreviating f_{∗} to f. If f is below-preserving, we write f^{+} for (f^{∗})_{#}.

A general comment about kar(rel) is in order. It may at first seem that the notion of infosys, without reflexivity assumed, flies in the face of categorical practice. Consider, however, a general adjunction S ⊣ R : A \overline{}X in kar(rel). Since 1_{X} is ⊏ : X \overline{}X, the unit condition, 1_{X} ⊆ R · S, says x ⊏ y implies (∃a)(xRaSy), which is an “interpolativity” of sorts. Similarly, the counit condition, S ·R ⊆ 1_{A} , says aSxRb implies a ⊏ b , a “transitivity”. If adjunction is deemed to be the leading aspect of category theory then the notion of infosys is remarkably natural.

Proposition 1 If f : X ⟶ A is below-preserving then f_{+} ⊣ f^{+} in kar(rel).

Proof. That f is below-preserving means precisely that f · ⊏ ⊆ ⊏ · f. From f_{∗} ⊣ f^{∗} in rel we have also ⊏ · f^{∗} ⊆ f^{∗} · ⊏ . The required inequalities now follow easily.

Infosyses and below-preserving arrows clearly form a category. For f, g : X ⟶ A define f ≤ g if and only if f_{+} ⊆ g_{+} . It is easy to show that this definition gives an ord-category, which we call inf, and an ord-functor ( )_{+} : inf ⟶ kar(rel). By construction, ( )_{+} is the identity on objects, locally fully faithful and every arrow in inf gives an adjunction in kar(rel). By definition therefore, ( )_{+} is proarrow equipment [19] and an object of the 3-category IF studied in [2]. It restricts to ( )_{+} : ord ⟶ idl, well known to be an object of IF which as such contains ( )_{∗} : E ⟶ rel. As we said in the Introduction, familiarity with general proarrow equipments and [2] is not assumed but these observations ensure that ( )_{+} : inf ⟶ kar(rel) shares many 2-categorical properties with ( )_{+} : ord ⟶ idl. In fact ( )_{+} : inf ⟶ kar(rel) satisfies the stronger Axioms 4 and 5 of [20]. For reference later, note that if f : X ⟶ A and u : A ⟶ X in inf then f ⊣ u if and only if f^{+} = u_{+}. This follows immediately from the definition of the ord-structure of inf.

We denote the discrete infosys structure on the E terminal object by 1. For infosyses X and Y we understand X × Y to be the infosys with structure defined component-wise on the E product of the underlying objects. Just as for rel and idl , − × − can be defined component-wise on modules giving an ord-monoidal structure. Neither 1 nor X × Y are finite products in kar(rel) but ( )_{+} : inf ⟶ kar(rel) is a cartesian object of IF as described in Section 5 of [2]. Note though that finite meets of modules are not intersections in general.

We write IDX for the ordered object (kar(rel))(1, X) and find it convenient to speak set-theoretically of its “elements” as down-sets. For S ∈ IDX we have x ∈ S if and only if (∃y)(x ⊏ y ∈ S). Important examples of down-sets are those which are of the form ↓x = {y ∈ X | y ⊏ x}, for x ∈ X. If X is an order then IDX is just DX, the ordered object of down-closed subsets of X and ↓ is the usual Yoneda embedding. In general, however, the adjective “closed” is inappropriate. Writing |X| for the underlying E object of an infosys we see that the inclusion IDX[figure] P|X| is coreflective but fails in general to preserve even finite meets. The involution ( )^{op} for orders extends to infoyses in the obvious way and the same “variance” rules apply if one considers inf ⟶ kar(rel) as an object of IF. In other words, the following diagram commutes.

[figure: kar(rel)^{op}; kar(rel); ( )^{op}; inf^{co}; inf; ( )^{op}; ( )^{+}; ( )_{+}]

Now it should be clear that a module X \overline{}A can be identified with a down-set of X^{op} × A. In fact we can identify (kar(rel))(X, A) with ID(X^{op} × A) which both explains the remark about finite meets of modules and gives the following:

Proposition 2 (kar(rel), −×− ,1) is ord-symmetric-monoidal-closed with its closed structure given by − × X ⊣ X^{op} × −.

Recall that both rel and idl are biclosed ord-categories in that they have all right liftings and all right extensions. That is, for each R : X \overline{}A, each (kar(rel))(Y, R) has a right adjoint and each (kar(rel))(R, B) has a right adjoint.

Proposition 3 kar(rel) is a biclosed ord-category.

Proof. If R : X \overline{}A and S : Y \overline{}A in kar(rel) then the right lifting in rel, denoted R ⇒ S : Y \overline{}X, gives the module

(R ⇒ S)_{#} = ⊏ · (R ⇒ S) · ⊏ : Y \overline{}X

as right lifting in kar(rel). For if T is a module and T ⊆ ⊏ · (R ⇒ S) · ⊏ then RT ⊆ R · ⊏ · (R ⇒ S) · ⊏ = R · (R ⇒ S) · ⊏ ⊆ S · ⊏ = S. Conversely if R · T ⊆ S then T ⊆ R ⇒ S whence T = ⊏ · T · ⊏ ⊆ ⊏ · (R ⇒ S) · ⊏ .

If R : X \overline{}A and T : X \overline{}B in kar(rel) then the right extension in rel, T ⇐R : A \overline{}B, gives (T ⇐R)_{#} as the right extension in kar(rel) similarly.

We have already given an elemental characterization of adjunctions in kar(rel). It is now easy to characterize those S : X \overline{}A which are maps. For if S has a right adjoint then it must be (S ⇒ 1_{A})_{#} and the latter is the right adjoint of S precisely if 1_{X} ⊆ (S ⇒ 1_{A})_{#} · S. (These are generalities valid in any biclosed ord-category.) We leave it as an exercise for the reader to show that this simplifies to ⊏_{X} ⊆ (S ⇒ 1_{A}) · S. In elemental terms then, S is a map if and and only if x ⊏ y implies (∃a)(aSy and (∀b)(bSx implies b ⊏ a)). We are grateful to the referee for informing us of this simplified characterization which is attributed to Reinhold Heckmann. It shows clearly that maps in kar(rel) are more general than the modules of the form f_{+} for f an arrow in inf. However, there is a sense in which this generality is somewhat illusory as we will show at the end of Section 4.

We will be preoccupied by IDX so let us note that the coreflector for IDX[figure] P|X| is given by ( )^{o}, where B^{o} = ⋃{↓x | ↓x ⊆ B}.

Proposition 4 (Raney) For any infosys X, IDX is (CCD).

Proof. Consider ↓: IDX ⟶ DIDX. We know from the above that any union of downsets is a down-set. In particular the union of a ⊆-down-closed set of down-sets is a down-set so the left adjoint to ↓: IDX ⟶ DIDX is given by union. We show that ⋃ has a left adjoint, l, given by lS = {↓x | x ∈ S} ^{}, where ( ) ^{}indicates down-closure with respect to ⊆. This at least defines l : IDX ⟶ DIDX (order preserving). (Incidentally, it is necessary to take the “downclosure” above, as becomes apparent by considering an infosys of the form (X, =).) We show S ⊆ ⋃ lS for S ∈ IDX and l(⋃ S) ⊆ S for S ∈ DIDX. For the first it suffices to show that if x ∈ S then x ∈ ↓ y for some y ∈ S. But since S is a down-set we have x ∈ S if and only if (∃y)(x ⊏ y ∈ S) if and only if x ∈ ↓ y for some y ∈ S. So S = ⋃ lS. For the second let T ∈ l(⋃ S). We have T ⊆ ↓x for some x ∈ ⋃ S and for such x we have x ∈ S ∈ S for some S. Since S is a down-set we have ↓ x ⊆ S and hence T ⊆ ↓ x ⊆ S ∈ S. Since S is down-closed we have T ∈ S as required.

2 The totally-below relation

Let L denote a complete lattice. Thus we assume that ↓: L ⟶ DL has a left adjoint L ⟵ DL: ⋁. The Yoneda embedding ↓ is, in any event, full(y faithful) so we note that ⋁ ↓ ≅ 1_{L}. Write a ≪ b as an abbreviation for the relation on L which is defined by (∀S ∈ DL)(b ≤ ⋁ S ⇒ a ∈ S). Following [1] we call ≪ the totally-below relation. (We called it “way below” in [6] but we now think that term should be reserved for the case of filtered (directed) sups where it originated. For Raney it was the anonymous relation ρ and Vickers speaks of “completely below”.)

Lemma 5 For ≪ the totally-below relation on a complete lattice:

(i) a′ ≤ a ≪ b implies a′ ≪ b (ii) a ≪ b ≤ b′ implies a ≪ b′ (iii) a ≪ b implies a ≤ b (iv) a ≪ b ≪ c implies a ≪ c

By (i) and (ii) above we see that ≪ is an arrow in idl. It is of some interest to note that

[figure: DL; L; ⋁+; L; ↓^{+}; ≪; ⊇]

is a right extension in idl . This follows immediately from the definitions.

Since identity arrows in idl are given by the order relations of the objects in question, (iii) gives us ≪ ⊆ 1_{L}, while transitivity of ≪ (iv), is simply ≪ · ≪ ⊆ ≪. Thus ≪ has both a “counit” and a “multiplication”. A “unit” for ≪ is impossible (for in a complete lattice we never have 0 ≪ 0) but a (necessarily idempotent) “comultiplication” exists if and only if ≪ is interpolative.

From the natural bijection between arrows X \overline{}A in idl and arrows X ⟶ DA in ord, ≪ corresponds to ⇓ : L ⟶ DL given by ⇓ a = {b ∈ L | b ≪ a}. We have ⇓ ⊆ ↓ and hence ⋁ ⇓ ≤ 1_{L}.

Lemma 6 ⇓ ⋁ ⊆ 1_{DL}.

Proof. Let S ∈ DL. Let a ∈ ⇓ ⋁ S. Then a ≪ ⋁ S and ⋁ S ≤ ⋁ S implies a ∈ S. So ⇓ ⋁ S ⊆ S.

Say that L is totally continuous if for every a ∈ L , a ≅ ⋁ ⇓ a. That is to say, every element is a supremum of those elements totally-below it. (In [1] this condition is called supercontinuity.) In view of ⋁ ⇓ ≤ 1_{L} which we noted above, L is totally continuous if and only if 1_{L} ≤ ⋁ ⇓ .

Proposition 7 (Raney) For a complete lattice L, L is totally continuous if and only if L is (CCD) .

Proof. From the previous remark and Lemma 6, L is totally continuous if and only if ⇓ is left adjoint to ⋁ . So total continuity certainly implies (CCD), for recall that the latter is just the condition that ⋁ have a left adjoint. Conversely, assuming the latter condition, say f ⊣ ⋁, then to show total continuity the condition 1_{L} ≤ ⋁ ⇓ can be replaced by the equivalent f ⊆ ⇓ . So let b ∈ fa, take any S ∈ DL and assume a ≤ ⋁ S. Adjointness gives fa ⊆ S and hence b ∈ S. So b ≪ a, that is b ∈ ⇓ a which shows f ⊆ ⇓.

Lemma 8 (Raney) If L is (CCD) then ≪ is interpolative.

Proof. We merely have to simplify the proof given in [9] by deleting the “directedness” conditions. Assume a ≪ b. Define

S = {d | (∃c)(d ≪ c ≪ b)} = ⋃{⇓ c | c ≪ b}

which is down-closed. We have ⋁ S ≅ ⋁{⋁ ⇓ c | c ≪ b} ≅ ⋁{c | c ≪ b} ≅ b. Now a ≪ b and b ≤ ⋁ S gives a ∈ S so (∃c)(a ≪ c ≪ b).

So now Lemma 5 (iv) and Lemma 8 show that any (CCD) object L gives rise to an infosys, (L, ≪), and Lemma 5 (iii) says that the identity E arrow on |L| gives an arrow (L, ≪) ⟶ (L, ≤) = L in inf. For any infosys X, the preceding considerations apply to the lattice IDX which is (CCD) by Proposition 4. We prefer to write ⊂⊂ for the totallybelow relation on IDX. It follows from the second part of the proof of Proposition 4 that for down-sets S and T we have S⊂⊂T if and only if (∃t)(S ⊆ ↓t and t ∈ T).

Lemma 9 For any infosys X, ↓ provides an arrow X ⟶ (IDX, ⊂⊂) in inf.

Proof. Assume x ⊏ y. Then ↓x ⊆ ↓x and x ∈ ↓y shows that ↓x⊂⊂ ↓y.

Remark 10 We have throughout this series systematically used ↓: X ⟶ DX for the Yoneda embedding in ord of an ordered object X = (X, ≤) into the lattice of down-closed subsets DX = (DX, ⊆). For X an infosys we have ↓: X ⟶ IDX, where IDX = (IDX, ⊆) which specializes to the previous convention. The point of Lemma 9 is simply that in any event ↓ factors through (IDX, ⊂⊂) ⟶ IDX, an instance of the inf arrow mentioned after Lemma 8. We allow the symbol ↓ to serve double duty by being explicit about its codomain.

Proposition 11 ↓_{+}: X \overline{}(IDX, ⊂⊂) is an isomorphism in kar(rel).

Proof. By Proposition 1 we have 1_{X} ⊆ ↓^{+}↓_{+} and ↓_{+}↓^{+} ⊆ 1_{(IDX,⊂⊂)}. Assume x ↓^{+}↓_{+} y, that is to say (∃S)(x ↓^{+} S ↓_{+} y). Invoking the definitions gives

(∃S)((∃u)(x ⊏ u and ↓u⊂⊂S) and (∃v)(S⊂⊂ ↓v and v ⊏ y))

which immediately simplifies to x ⊏ y. So ↓^{+}↓_{+} ⊆ 1_{X}.

Now S ↓_{+}↓^{+} T holds if and only if (∃x)(S ↓_{+} x ↓^{+} T) if and only if (∃x)((∃u)(S⊂⊂ ↓ u and u ⊏ x) and (∃v)(x ⊏ v and ↓v ⊂⊂ T)).

On the other hand, if S⊂⊂T then we have S ⊆ ↓t for some t ∈ T which can be interpolated to S ⊆ ↓ t, with t ⊏ u ⊏ x ⊏ v ∈ T, since T is a down-set, giving S ⊂⊂ ↓ u and u ⊏ x ⊏ v and ↓ v ⊂⊂ T, the last from ↓ v ⊆ ↓ v, v ∈ T. From the display above it is clear that S ⊂⊂ T implies S ↓_{+}↓^{+} T so 1_{(IDX,⊂⊂)} ⊆ ↓_{+}↓^{+} .

Remark 12 It is not too surprising that 1_{X} = ↓^{+}↓_{+}. After all, the classical Yoneda embedding is full(y faithful). But having also 1_{(IDX,⊂⊂)} = ↓_{+}↓^{+} provides isomorphisms between objects in kar(rel) whose underlying E objects may be definitely not isomorphic. For example, if X is any object of E then, regarding it as a discrete infosys (X, =), Proposition 11 provides an isomorphism X ⟶ (PX, ⊂⊂) in kar(rel). Note too that while the totallybelow relation ≪: L \overline{}L for any complete lattice L is given as a right extension in idl , the second identity can be interpreted to express ⊂⊂ for DX , where X is an ordered object, as a composite in idl :

DX ^{\overline{}^{⊂⊂}} DX = DX ^{\overline{}^{↓^{+}}} X ^{\overline{}^{↓_{+}}} DX.

It says that for S, T ∈ DX, S ⊂⊂ T if and only if (∃x)(S ⊆ ↓x ⊆ T)

If L is any (CCD) object then the defining left adjoint to supremum, ⇓: L ⟶ DL given by ⇓ a = {b ∈ L | b ≪ a} factors through ID(L, ≪) = (ID(L, ≪), ⊆).

Proposition 13 For any (CCD) lattice L, ⇓: L ⟶ ID(L, ≪) is an ord equivalence.

Proof. We have ⋁ : ID(L, ≪) ⟶ L, the restriction of ⋁ : DL ⟶ L and ⋁ ⇓ ≅ 1_{L} as noted in the proof of Proposition 5 . Now consider ⇓ ⋁ S for S a down-set with respect to ≪. We have ⇓ ⋁ S ⊆ S by adjointness, so let x ∈ S. We want to show x ≪ ⋁ S. Since S is a down-set we have x ≪ y ∈ S for some y. Now y ≤ ⋁ S and x ≪ y ≤ ⋁ S gives x ≪ ⋁ S as required.

Remark 14 If the order on L is antisymmetric then the equivalence above is just an order isomorphism.

3 Categories of (CCD) lattices

We write ccd_{sup} for the ord-category of (CCD) lattices, sup-preserving arrows and pointwise inequalities. Let f : L ⟶ M be an arrow in ccd_{sup} . It does not follow that f preserves ≪ , so f does not define an arrow from (L, ≪) to (M, ≪) in inf but as in Section 1 we do have the module f_{#} : (L, ≪) ⟶ (M, ≪) in kar(rel).

Lemma 15 The construction above defines an ord-functor ccd_{sup} ⟶ kar(rel) .

Proof. Assume f ≤ g : L ⟶ M. Recall that we have xf_{#}a if and only if (∃b)(x ≪ fb and b ≪ a). Since x ≪ fb ≤ gb implies x ≪ gb we have f_{#} ⊆ g_{#}. Also, (1_{L})_{#} = ≪ = 1_{(L,≪)}. Now assume f : L ⟶ M and g : M ⟶ N in ccd_{sup} . Since f is sup-preserving we have f ⋁ ≅ ⋁ f_{!}, where f_{!} : DL ⟶ DM is the left adjoint to Df : DM ⟶ DL. Since L and M are (CCD) we have by adjointness ⇓ f ⊆ f_{!} ⇓ which means that x ≪ fa implies (∃b)(x ≤ fb and b ≪ a). Similarly, p ≪ gx implies (∃y)(p ≤ gy and y ≪ x). We have p(g_{#}f_{#})a if and only if (∃x)(∃b)(p ≪ gx and x ≪ fb and b ≪ a) which yields (∃x)(∃b)(∃c)(p ≪ gx and x ≤ fc and c ≪ b ≪ a) hence (∃x)(∃c)(p ≪ gx ≤ gfc and c ≪ a) and finally (∃c)(p ≪ gfc and c ≪ a) which is p(gf)_{#}a. Conversely starting with the latter and interpolating gives (∃q)(∃c)(p ≪ q ≪ gfc and c ≪ a) yielding (∃y)(∃q)(∃c)(p ≪ q ≤ gy and y ≪ fc and c ≪ a) and hence (∃y)(∃c)(p ≪ gy and y ≪ fc and c ≪ a) which is p(g_{#}f_{#})a. So g_{#}f_{#} = (gf)_{#}.

Given R : X \overline{}A in kar(rel) we define R_{!} : IDX ⟶ IDA by the formula R_{!}(T) = ⋃{{a | aRx} | x ∈ T }. This makes sense since each {a | aRx} is a down-set and a union of down-sets is a down-set. But viewing T as T : 1 \overline{}X in kar(rel) we see that R_{!}(T) is precisely the composite RT : 1 \overline{}A in kar(rel) which shows immediately that R ⊆ S implies R_{!} ⊆ S_{!}, (1_{X})_{!} = 1_{IDX} and (SR)_{!} = S_{!}R_{!}.

Lemma 16 The construction above defines an ord-functor kar(rel) ⟶ ccd_{sup} .

Proof. It suffices to show that each R_{!} has a right adjoint. Define IDR : IDA ⟶ IDX by IDR(S) = {x | (∃y)(x ⊏ y and {a | aRy} ⊆ S)}. Recall that since rel is biclosed, we have R ⇒ S : 1 \overline{}X, the right lifting of S : 1 \overline{}A through R : X \overline{}A in rel. It is easy to see that IDR(S) is the composite ⊏ · (R ⇒ S) : 1 \overline{}X and hence certainly a down-set. The adjunction R_{!} ⊣ IDR follows from ⊏ · (R ⇒ S) = ⊏ · (R ⇒ S) · ⊏ = (R ⇒ S)_{#} being the right lifting of S through R in kar(rel) as given in full generality in Proposition 3.

An ord-functor F : X ⟶ A and an ord-functor U : A ⟶ X underlie a biequivalence of ord-categories in the presence of equivalences η : 1_{X} ⟶ UF and ϵ : F U ⟶ 1_{A}. If equivalences in X and A are merely isomorphisms then such a biequivalence is merely an equivalence. In kar(rel), for example, equivalences are isomorphisms because transformations between modules are containments and containment is antisymmetric.

Theorem 17 The ord-functors of Lemmas 16 and 15 underlie a biequivalence of ordcategories, ccd_{sup} ⟶^{∼} kar(rel).

Proof. The isomorphism ↓_{+} : X ⟶ (IDX, ⊂⊂) of Proposition 11, for X an infoysys, and the equivalence ⇓: L ⟶ ID(L, ≪) of Proposition 13, for L a (CCD) lattice, are all that we need provided that they are natural with respect to the functors of Lemmas 15 and 16. Thus we require commutativity of the following diagrams:

[figure: (IDX, ⊂⊂); (IDA, ⊂⊂); (R_{!})_{#}; X; A; R; ↓_{+}; ↓_{+}; ID(L, ≪); ID(M, ≪); (f_{#})_{!}; L; M; f; ⇓; ⇓]

the first in kar(rel), the second in ccd_{sup}. The first follows from the observation that both composites reduce to the relation (∃a)(T ⊆ ↓ a and aRx) while in the second the value of each composite at a is ⇓fa.

From Remark 14 it follows that if one’s “lattices” are antisymmetric then the biequivalence above is merely an equivalence. For inspection of the proof of Proposition 13 shows that ⇓ is an isomorphism if ⋁ ⇓ ≅ 1_{L} is an equality. In any event, the result has many specializations which we pursue in the remaining sections. Let us note some simple corollaries.

Corollary 18 The ord-category ccd_{sup} is biclosed and has an ord-symmetric-monoidal-closed structure.

From the earlier papers in this series ([6],[13],[14]) it is clear that an important class of arrows between (CCD) lattices is that consisting of those arrows that preserve both sups and infs. We write ccd for the locally-full sub-ord-category of ccd_{sup} determined by these. If g : M ⟶ L is such an arrow then considered as an arrow of ord it has both left and right adjoints, say f ⊣ g ⊣ h. Now f also preserves sups and we have an adjunction f ⊣ g in ccd_{sup}. (So f is a map in ccd_{sup}.) Since taking adjoints reverses both the direction of arrows and the sense of inequalities, it follows that ccd^{coop} = map(ccd_{sup}). We study these arrows in more detail in the next section.

Corollary 19 The ord-functors of Lemmas 15 and 16 restrict to a duality ccd^{coop} ⟶^{∼} map(kar(rel)).

An interesting application of Theorem 17 arises by considering the closed unit interval II = [0, 1] in a Boolean topos. We showed in [6] that II is (CCD) with ≪ given by <, mere strict inequality. Thus we have II ≅ ID(II, <). Now let IK denote the intersection of II with the rationals and observe that (IK, <), < as above, is again an infosys and the inclusion i : (IK, <) ⟶ (II, <) is an arrow of inf. So we have i_{+} : (IK, <) ⟶ (II, <) in kar(rel) . But the unit for the adjunction i_{+} ⊣ i^{+} is an equality because i is “full” and the counit is an equality because i is “dense” in that between any two distinct reals there is a rational. Thus i_{+} is an isomorphism giving ID(II, <) ≅ ID(IK, <). Together with the isomorphism above we have II ≅ ID(IK, <) in ccd_{sup} . In an arbitrary topos one might want to consider the latter as a definition of II since it allows the development of < using only positive statements. The closed interval resulting from this construction is isomorphic to the closed interval in the semicontinuous reals. The semi-continuous reals is the “real numbers object” constructed from lower Dedekind cuts on the rationals and is isomorphic to the sheaf of lower semi-continuous functions in a spatial topos [4].

4 Totally algebraic lattices

For any i : X ⟶ L in ord, i is said to be dense if 1_{L} is the left extension of i along i. In terms of elements this means that for all a in L, a ≅ ⋁{i(x) | x in X and i(x) ≤ a}.

If c ≪ c in a complete lattice, we say that c is totally compact. (In [1] this is called super compactness.) Let X (L) = {c ∈ L | c ≪ c}. Since by (iii) of Lemma 5 we have ⇓ ⊆ ↓, we can identify X (L) as the inverter of ⇓ ⊆ ↓: L ⟶ DL. In [6] we showed that a (CCD) lattice L is equivalent to one of the form DX, for some X in ord , if and only if the inclusion X (L)[figure] L is dense, in which case L is equivalent to D(X (L)). But density of X (L) in L is just the statement that every a in L is the supremum of the totally compact elements c with c ≤ a. Such a lattice is said to be superalgebraic in [1]. We use the term totally algebraic. By Proposition 7 it is clear that every totally algebraic lattice is (CCD) and we note that the totally below relation for totally algebraic lattices simplifies to a ≪ b if and only if (∃c)(a ≤ c ≪ c ≤ b). We must comment on the nesessity of the density condition in order to correct a typographical error in [6].

In [6] Proposition 7 it was asserted that the inverter of ⇓ ⊆ ↓: DX ⟶ DDX is X. The proof is easily seen to invoke the axiom of choice and according to the convention of that paper the words “Proposition 7” should have been preceded by an asterisk to indicate that dependence. The point there was simply to show that not all (CCD) lattices are what we are here calling “totally algebraic.” The exhibited counterexample, namely the closed unit interval with its usual ordering, survives but careful clarification of this point will provide a deeper analysis of the main result of this paper.

For X an ordered object we write QX for the Cauchy completion of X as defined in [11] and studied explicitly in this context in [3]. It is defined as a representing object for map(idl)(−, X) : ord^{op} ⟶ ord. (So for each Y we have ord(Y, QX) ≅ map(idl)(Y, X).) It is a central result of [3] that QX ≅ map(ccd_{sup})(D1, DX). This follows easily from the definition and our Theorem 17 for we have

QX ≅ ord(1, QX) ≅ map(idl)(1, X) ≅ map(kar(rel))(1, X) ≅ map(ccd_{sup})(D1, DX).

The formula is useful but it exhibits QX as a subobject of (D(DX)^{op})^{op} (since DX ≅ ord(X^{op}, D1) and map(ccd_{sup})(D1, DX) = ccd^{coop}(D1, DX) = ccd(DX, D1)^{op}) and yet QX ⊆ DX, since DX is a representing object for idl(−, X) : ord^{op} ⟶ ord. In fact, we claim that QX is the reflection of X in the ord-category of antisymmetric orders and is obtained by identifying isomorphic elements of X. For antisymmetric X, X ⟶ QX is an order isomorphism and it is always a (strong) epimorphism in E. In the presence of the axiom of choice it is an equivalence in ord for any X. In [3] it is shown that the axiom of choice for E is equivalent to every ordered object X being Cauchy complete (meaning that X ⟶ QX is an equivalence). The following Proposition is helpful for establishing our claim and admits useful generalizations that will be considered in [15]. Recall that the order isomorphism ord(Y, DX) ≅ idl(Y, X) is given by composition with ↓^{+}: DX \overline{}X.

Proposition 20 For any X in ord, QX ⟶ DX is the inverter of ⇓ ⊆ ↓: DX ⟶ DDX.

Proof. An arrow r : Y ⟶ DX in ord inverts ⇓ ⊆ ↓ if and only if r ≪ r which as we pointed out in Remark 12 is the case if and only if (∃x)(r ⊆ ↓ x ⊆ r). The latter means that there exists an epi e : U → → Y in E and an arrow x : U ⟶ X such that re = ↓ x.

Now let R =↓^{+} r and note that ↓^{+}↓ x = x_{+}. It follows that r factors through the inverter of ⇓ ⊆ ↓, call it I, if and only if the corresponding ideal, R, satisfies Re = x_{+} for such e and x. According to [3] the latter is the case if and only if R is a map. Thus ord(Y, DX) ≅ idl(Y, X) restricts to ord(Y, I) ≅ map(idl)(Y, X) which shows that I ⟶ DX is order isomorphic to QX ⟶ DX.

Certainly, from its very definition, QX is antisymmetric and the full(y faithful) QX ⟶ DX is a monomophism in E. The full(y faithful) and dense ↓: X ⟶ DX is a monomorphism in E if and only if X is antisymmetric. In any event it inverts ⇓ ⊆ ↓ so that we have ↓: X ⟶ QX fully faithful and QX ⟶ DX dense. Moreover the proof of the Proposition also shows that ↓: X ⟶ QX is an epimorphism in E so that QX can also be seen as the image in E of ↓: X ⟶ DX, equipped with the induced order. Note that while antisymmetry implies Cauchy completeness, the converse is not true. For example, a complete lattice L is Cauchy complete — an inverse equivalence to ↓: L ⟶ QL is provided by the restriction of the supremum arrow.

We now specialize Theorem 17. Write tal_{sup}, for the full and locally-full sub-ord-category of ccd_{sup} determined by the totally algebraic objects. Since for X an order IDX = DX, the ord-functor kar(rel) ⟶ ccd_{sup} restricts to idl ⟶ tal_{sup}.

Theorem 21 The ord-functor above is the inverse of a biequivalence of ord-categories,

tal_{sup} ⟶^{∼} idl.

Proof. Let f : L ⟶ M be a sup preserving arrow between totally algebraic lattices. We define X (f) : X (L) \overline{}X (M) by xX (f)a if and only if x ≤ fa. If also g : M ⟶ N is sup preserving with N totally algebraic then pX (gf)a gives p ≪ p ≤ gfa and hence (∃x)(p ≤ gx and x ≪ fa). There is no reason to assume that x is totally compact but, from the simplification of ≪ here that we noted above, x ≪ fa yields (∃y)(x ≤ y ≪ y ≤ fa) so that we have (∃y)(p ≤ gy and y ≪ y ≤ fa) and hence pX (g)X (f)a. The other details showing that X is an ord-functor tal_{sup} ⟶ idl are trivial. Consider now

[figure: QX; QA; X (R_{!}); X; A; R; ↓_{+}; ↓_{+}; DX L; DX M; (X f)_{!}; L; M; f; k; k]

the first in idl, the second in tal_{sup} . For the first diagram we have used ↓: X ⟶ X DX ≅ QX, as discussed above, which by the universal property of QX induces an isomorphism in idl. The diagram is easily seen to commute. In the second diagram k is the left kan extension of ↓: X L ⟶ DX L along X L ⟶ L, an equivalence here as shown in [6], Theorem 8. Since f preserves sups commutativity can be shown by “chasing an element of X (L)” the details of which we also omit.

Remark 22 Of course we could have argued above that for L totally algebraic we have an inclusion (X L, ≪) ⟶ (L, ≪) in inf which induces a natural isomorphism in kar(rel). This follows immediately from the simplified description of ≪. This approach also shows that (DX, ⊂⊂) provides yet another description, up to isomorphism in kar(rel), of QX, albeit as an infosys. In fact, as we will show shortly, for X an infosys, (IDX, ⊂⊂) is the appropriate notion of Cauchy completion.

Corollary 23 The ord-category tal_{sup} is biclosed and the ord-symmetric- monoidal-closed structure of ccd_{sup} restricts to it.

Write tal for the full and locally-full sub-ord-category of ccd determined by the totally algebraic objects. Equivalently tal is the locally-full sub-ord-category of tal_{sup} determined by the arrows which preserve both sups and infs and we thus have tal^{coop} = map(tal_{sup}). Let cor denote the full and locally-full sub-ord-category of ord determined by the Cauchy complete objects. Then cor is biequivalent to map(idl).

Corollary 24 There is a duality tal^{coop} ⟶^{∼} cor with inverse given by D.

Proof. Apply map to the biequivalence established above and note that the biequivalence cor ∼ map(idl) identifies D : cor ⟶ tal^{coop} with map(idl ⟶ tal_{sup}).

To see what the map construction is hiding in both Corollaries 19 and 24 it is instructive to note the following Proposition which is of some independent interest.

Proposition 25 For (CCD) objects L and M and an adjunction f ⊣ g : M ⟶ L in ord, g has a right adjoint if and only if f preserves ≪. If L is totally algebraic then preservation of ≪ by f is equivalent to f preserving totally compact elements.

Proof. Write f_{!} for the left adjoint of Df : DM ⟶ DL. For any f in ord , f_{!} ↓ = ↓ f. Since L and M are complete we have the mate ⋁ f_{!} ≤ f ⋁ which is “invertible” (saying f preserves sups) since f ⊣ g. Now the inequality f ⋁ ≤ ⋁ f_{!} has mate ⇓f ⊆ f_{!} ⇓ since L and M are (CCD) objects. However, the containment f_{!} ⇓ ⊆ ⇓f is equivalent to ⇓g ⊆ g_{!} ⇓ which in turn is equivalent to g ⋁ ≤ ⋁ g_{!} (saying g preserves sups) and hence is equivalent to g having a right adjoint. On the other hand, direct translation of f_{!} ⇓ ⊆ ⇓f gives f· ≪ ⊆ f· ≪, which is preservation by f of ≪. The second clause of the Lemma holds in virtue of the simplification of ≪ in a totally algebraic lattice.

From the proof it follows that f has a right adjoint which has a right adjoint precisely if the following diagram “commutes”.

[figure: DL; DM; f_{!}; L; M; f; ⇓; ⇓]

That is to say, we can dispense with the assumption that f is part of an adjunction. While this is an apparently sensible categorical condition it is not ord-categorical because for a general f there need be no transformation (containment) of which the “=” above expresses the invertibility. This might seem inconsequential but many of our results generalize to Yoneda structures [17] on 2-categories that are not locally ordered. In that case “commutativity” is obviously too strong but we cannot simply replace equality by an isomorphism because the mates of both such an isomorphism and its inverse are required to be specific transformations. It seems to be difficult to prescribe the “right” isomorphism in advance.

The proposition shows that if we apply the ord-functor ccd_{sup} ⟶ kar(rel) to an adjunction f ⊣ g : M ⟶ L then we get f : (L, ≪) ⟶ (M, ≪) in inf and hence f_{+} ⊣ f^{+} in kar(rel). Corollaries 19 and 24 could be derived directly from this observation.

Moreover, inspection of the first diagram in the proof of Theorem 17 now shows that any diagram of maps in kar(rel) can be replaced by an isomorphic diagram of maps of the form f_{+} with f in inf. For if R is a map then R_{!} is a map in ccd_{sup} and so preserves ⊂⊂ giving (R_{!})_{#} = (R_{!})_{+}. We leave it as an exercise for the reader to show that (IDX, ⊂⊂) is a birepresenting object for map(kar(rel))(−, X) : inf^{op} ⟶ ord. Indeed, composition with ↓^{+}: (IDX, ⊂⊂) ⟶ X provides for each A, an equivalence inf(A, (IDX, ⊂⊂)) ⟶ map(kar(rel))(A, X). In the next section some of our definitions are given in terms of inf arrows where one might feel that maps in kar(rel) are more natural. The results above show that our approach is justified and certainly from a constructivist’s point of view the more deterministic inf arrows are a better starting point.

5 Left exactness

The main results of the previous two sections and their proofs admit “lexification”. Roughly speaking this means that if all objects are required to have finite meets which all arrows are required to preserve then the biequivalences of Theorems 17 and 21 and the dualities of Corollaries 19 and 24 restrict accordingly.

Write lex.ord for the locally-full sub-ord-category of ord determined by the finitely complete objects and arrows which preserve finite meets. In the terminology of [2], the objects of lex.ord are the cartesian objects of ord. Note that to ask for a left adjoint in lex.ord is to ask for a left adjoint in ord and further require that it preserve finite meets. For example, a complete lattice is an object L in ord for which ↓: L ⟶ DL has a left adjoint. To require this of an object L in lex.ord is to require that the left adjoint, ⋁, preserve finite meets — which is to require that L be a frame. Similarly, a lex (CCD) object is a (CCD) object for which the defining left adjoint, ⇓, is left exact. One could say that a lex (CCD) object is simply a (CCD) object relative to lex.ord and its inherited Yoneda structure, as in [17]. However, careful pursuit of that idea would take us too far afield for our present purposes. After all, the notion of (CCD) itself begs consideration as “completeness” relative to yet another Yoneda structure.

In terms of ≪, left exactness of ⇓ says precisely that

L1) 1 ≪ 1

L2) if c ≪ a and c ≪ b then c ≪ (a ∧ b).

Thus lex (CCD) is stable supercontinuity in the terminology of [1]. We write lex.ccd_{frm} for the locally-full sub-ord-category of ccd_{sup} determined by the lex (CCD) objects and frame homomorphisms. A frame homomorphism between frames, f : L ⟶ M, is a suppreserving arrow that satisfies

F1) f(1) ≅ 1 and

F2) f(a ∧ b) ≅ f(a) ∧ f(b). An object X in inf is cartesian precisely if

C1) t : X ⟶ 1 is a map in inf

C2) d : X ⟶ X × X is a map in inf.

Here of course t refers to the unique inf arrow to the terminal object and d refers to the product diagonal in inf. It should be noted that if X above is in ord then the conditions express that X is in lex.ord . In general, the notion of adjunction in inf, as noted in Section 1, allows us to translate the conditions as follows:

C1) There is an element 1 in X with 1 ⊏ 1 such that (∃y)(x ⊏ y) implies x ⊏ 1

C2) There is a binary operation − ∧ − on X with (c ⊏ a and d ⊏ b implies (c ∧ d) ⊏ (a ∧ b)) such that (∃y)(x ⊏ y and (y ⊏ a and y ⊏ b)) if and only if (∃c, d)(x ⊏ c ∧ d and (c ⊏ a and d ⊏ b)).

For X and A cartesian infosyses and R : X \overline{}A in kar(rel) we say that R is left exact if it satisfies

M1) 1R1

M2) if aRx and aRy then aR(x ∧ y).

We write lex.kar(rel) for the locally-full sub-ord-category of kar(rel) determined by the cartesian infosyses and left exact modules. Observe that if X and A are orders then a left exact module as above is precisely what one usually understands by a left exact order ideal.

Before proceding with the main results of this section it will be useful to spell out explicitly the finite meets of IDX = (IDX, ⊆), for X an infosys.

The top element is X^{o} = ⋃{↓ y | y ∈ X} while for S, T in IDX, S ∧ T = (S ∩ T)^{o}. Thus u is in S ∧ T if and only if there exists a v with u ⊏ v and such that if x ⊏ v then x is in S ∩ T.

Lemma 26 For X an infosys 1) If X satisfies C1) then X^{o} = ↓ 1. 2) If X satisfies C2) then for S, T ∈ IDX; if s ∈ S and t ∈ T then s ∧ t ∈ S ∧ T.

Proof. 1) is easy so consider the situation in 2). Since S and T are down-sets we can take s ⊏ s′ ∈ S and t ⊏ t′ ∈ T from which we get (s ∧ t) ⊏ (s′ ∧ t′). To show s ∧ t ∈ S ∧ T it suffices now to show that if x ⊏ (s′ ∧ t′) then x ∈ S ∩ T. But we can take s′ ⊏ s′′ ∈ S and t′ ⊏ t′′ ∈ T which with x ⊏ (s′ ∧ t′) and C2) gives y such that x ⊏ y and y ⊏ s′′ and y ⊏ t′′ from which it follows that x ∈ S ∩ T.

Lemma 27 For L a (CCD) lattice, i) If L satisfies L1) then (L, ≪) satisfies C1); ii) If L satisfies L2) then (L, ≪) satisfies C2). For X an infosys, iii) If X satisfies C1) then IDX satisfies L1); iv) If X satisfies C2) then IDX satisfies L2).

For f : L ⟶ M sup-preserving with L and M lex (CCD), v) If f satisfies F1) then f_{+} : (L, ≪) \overline{}(M, ≪) satisfies M1); vi) If f satisfies F2) then f_{+} : (L, ≪) \overline{}(M, ≪) satisfies M2).

For R : X \overline{}A a module with X and A cartesian, vii) If R satisfies M1) then R_{!} : IDX ⟶ IDA satisfies F1); viii) If R satisfies M2) then R_{!} : IDX ⟶ IDA satisfies F2).

Proof. iii) We recall from the paragraph preceding Lemma 9 that S ⊂⊂ T ∈ IDX if and only if (∃t)(S ⊆ ↓t and t ∈ T). If X satisfies C1) then by 1) of Lemma 26 we have X^{o} ⊆ ↓1 and also C1) implies that 1 ∈ X^{o} so X^{o} ⊂⊂ X^{o}.

iv) For R, S, T in IDX assume that R ⊂⊂ S and R ⊂⊂ T with the first witnessed by R ⊆ ↓s, s ∈ S and the second by R ⊆ ↓t, for t ∈ T. Let r ∈ R. We have r ⊏ r′ ∈ R and hence (r ⊏ r′ and (r′ ⊏ s and r′ ⊏ t)) to which we can apply C2) and get r ⊏ (s′ ∧ t′) for some s′ ⊏ s and t′ ⊏ t. Hence R ⊆ ↓(s′ ∧ t′) and since s′ ∧ t′ ∈ S ∧ T by Lemma 26 we have R ⊂⊂ (S ∧ T).

viii) For S, T ∈ IDX and R : X \overline{}A it suffices to show that RS ∧ RT ⊆ R(S ∧ T) assuming that aRx and aRy implies aR(x ∧ y). But if a ∈ RS ∧ RT then certainly a ∈ RS and a ∈ RT from which it follows that there exists s in S with aRs and there exists t in T with aRt. Now aR(s ∧ t) and by Lemma 26 s ∧ t ∈ S ∧ T so a ∈ R(S ∧ T) as required.

The proofs of the other clauses are left for the reader.

Theorem 28 The biequivalence ccd_{sup} ⟶^{∼} kar(rel) restricts to a biequivalence, lex.ccd_{frm} ⟶^{∼} lex.kar(rel).

It seems reasonable also to note the “map” version of the above theorem. Write lex.ccd for the ord-category of lex (CCD) objects and arrows g : M ⟶ L which are locale arrows which have right adjoints. From Proposition 25 it follows that the left adjoints, f : L ⟶ M, of such arrows are precisely frame homomorphisms that preserve ≪ and such arrows were of interest in [1].

Corollary 29 The duality ccd^{coop} ⟶^{∼} map(kar(rel)) restricts to a duality lex.ccd^{coop} ⟶^{∼} map(lex.kar(rel)).

Finally, we turn again to totally algebraic lattices. The following Lemma is surely known in much greater generality:

Lemma 30 The forgetful ord-functor lex.ord ⟶ ord creates inverters.

The Lemma shows that in a lex (CCD) object the totally compact elements are closed with respect to finite meets. Thus a lex totally algebraic lattice is what was called a supercoherent frame in [1] — a lattice that is both lex (CCD) and totally algebraic. We write lex.tal_{frm} for the full and locally full sub-ord-category of lex.ccd_{frm} determined by these and, similarly, lex.tal for the corresponding full and locally-full sub-ord-category of lex.ccd. Again by Proposition 25, it follows that the left adjoint, L ⟶ M, of an arrow M ⟶ L in lex.tal is precisely a frame homomorphism that preserves totally compact elements. (See [1].)

We write lex.idl for the ord-category of ordered objects with finite meets and left exact order ideals. In other words lex.idl is the full and locally-full sub-ord-category of lex.kar(rel) determined by those infosyses which are orders. We define Cauchy completeness for objects of lex.ord in terms of maps in lex.idl and it is easy to see that for X in lex.ord its Cauchy completion is given by QX as in Section 4. Indeed, as was noted in [6], ⇓: DX ⟶ DDX is given by ↓_{!} for ↓: X ⟶ DX, and if f : X ⟶ Y is any arrow in lex.ord then f_{!} : DX ⟶ DY is in lex.ord so that this remark follows from Lemma 30.

Write lex.cor for the full and locally-full sub-ord-category of lex.ord determined by the Cauchy complete objects. The results and proofs of Section 4 and the first part of this section now combine to give the following:

Theorem 31 The biequivalence tal_{sup} ⟶^{∼} idl restricts to a biequivalence lex.tal_{frm} ⟶^{∼} lex.idl.

Corollary 32 The duality tal^{coop} ⟶^{∼} cor restricts to a duality lex.tal^{coop} ⟶^{∼} lex.cor.

If E is the topos set and orders are assumed to be antisymmetric then the corollary states the equivalence given in [1], Remark 3.

6 Projectivity

It is a central result of [1] that the lex (CCD) lattices are precisely the regular projectives in frm, the (ord-)category of frames and frame homomorphisms. In view of our treatment of left exactness above it is natural to conjecture that, modulo antisymmetry, (CCD) lattices are precisely the (regular) projectives of sup and moreover that the proof of the result in [1] is the lexification of a proof of the latter. This is indeed the case as we show now, making some ord-theoretic refinements in the process.

Let e : L ⟶ M be an arrow in either sup or frm and assume for the moment that all objects are antisymmetric. Then, for well-known general reasons, e is a regular epimorphism if and only if |e| : |L| ⟶ |M| is an epimorphism in the base, where we are using | − | to denote underlying object functors to E. In either case e has a right adjoint, e_{∗}, (we switch to the notation of the subject) and it follows, again for general reasons, that e is a regular epimorphism if and only if ee_{∗} ≅ 1_{M}. Of course it is well-known that in sup this last condition characterizes epimorphisms. Said otherwise, epimorphisms are regular epimorphisms in sup. In either case, the adjunction characterization, which we call co-fully faithful is the relevant condition when antisymmetry is not assumed. (We have already had to distiguish carefully between arrows which are monomorphisms in the base and those which are fully faithful!) Except as noted, we now revert to our usual position that orders are not assumed to be antisymmetric.

We should point out that this notion of “cofully faithful” is best understood in terms of the proarrow equipment sup ⟶ sup_{ord}, where the latter ord-category of sup lattices is the full and locally-full sub ord-category of ord determined by the sup lattices and the ord-functor is just the inclusion. For e above is cofully faithful if and only if for all N, sup_{ord}(e, N) is full(y faithful). In other words, for all f, g : M ⟶ N in sup_{ord}, fe ≤ ge implies f ≤ g. Similar remarks apply to the frm case.

Lemma 33 For any X in ord, respectively lex.ord, and any diagram

[figure: L; M; e; DX; g]

in sup, respectively frm, with e co-fully faithful, the right lifting of g through e exists and the exhibiting inequality is an isomorphism.

Proof. Consider, exactly as in [1],

[figure: L; M; e; X; DX; ↓; h; g; k]

in ord, respectively lex.ord, where h is defined by h = e_{∗}g ↓ and k is the unique sup, respectively frm arrow that makes the top triangle commute in virtue of the fact that DX is the free sup lattice, respectively frame, on X. We claim that k is the required lifting. Observe that ek corresponds to eh = ee_{∗}g ↓ ≅ g ↓ which corresponds to g and hence we have ek ≅ g. This is because in either case of the Lemma, D is an ord-left adjoint so that we have an ord isomorphism ord(X, L) ≅ sup(DX, L), respectively lex.ord(X, L) ≅ frm(DX, L). Of course if all our ordered objects are antisymmetric then we do not need this two-dimensional aspect of the free functor to show that the triangle commutes but the stronger freeness property allows us to conclude the (apparently) stronger lifting property. For assume that l : DX ⟶ L is any arrow in sup, respectively frm, with el ≤ g. Then l ≤ e_{∗}g and hence l ↓ ≤ e_{∗}g ↓ = h = k ↓ which implies, by ord-universality, that l ≤ k.

Let us say that an object C is universally projective if for all

[figure: L; M; e; C; g]

with e co-fully faithful, the right lifting of g through e exists and the exhibiting inequality is an isomorphism.

Lemma 34 Full coreflective subobjects of universal projectives are universal projectives.

Proof. Assume i : C[figure] D with i ⊣ r, 1_{C} ≅ ri and D a universal projective and consider a configuration as in the definition above. Let h = e ⇒ gr, the right lifting of gr through e and consider k = hi. Then ek = ehi ≅ gri ≅ g, where we have the first isomorphism since D is a universal projective. If l : C ⟶ L satisfies el ≤ g then elr ≤ gr so that lr ≤ h and hence l ≤ hi = k

Remark 35 Symbolically, we have above e ⇒ g ≅ (e ⇒ gr)i. We have been deliberately non-committal about the hypotheses for Lemma 34. It is clearly abstract ord-nonsense and generalizes in a variety of ways. For example, there is no mention in the proof of co-fully faithfulness.

We have implicitly noted in [13] that the adjoint sequence of a (CCD) lattice, ⇓ ⊣ ⋁ ⊣ ↓, may extend arbitrarily to the left. For example, if C is in ord then D^{n}C has a sequence (terminating at ↓) of length 2n + 1. In particular, recall that ⇓ for DC is given by ⇓ = (↓_{C})_{!}, so if C is a sup lattice then (⋁_{C})_{!} ⊣ ⇓ . We always have ⇓ ⊆ ↓ for a (CCD) lattice, so whenever there is a further adjoint, \⋁ ⊣ ⇓, we have also ⋁ ≤ \⋁. We return to this in Section 8. Note that we use the phrase ”g : D ⟶ C has a section” to mean that there exists f : C ⟶ D with gf ≅ 1_{C}.

Theorem 36 For C in sup, respectively frm, the following are equivalent:

1) C is (CCD), respectively lex (CCD)

2) C is a universal projective in sup, repectively frm

3) Assuming orders are antisymmetric: C is a regular projective in sup, repectively frm 4) ⋁ : DC ⟶ C has a section in sup, repectively frm.

Proof. 1)⇒ 2) In either case ⇓: C[figure] DC exhibits C as a full coreflective subobject of a universal projective. 2)⇒3) Trivial. 2) or 3)⇒4) Follows immediately since ⋁ is co-fully faithful. 4)⇒1) Given any f with ⋁ f ≅ 1_{C} we argue that f is necessarily left adjoint to ⋁. It suffices to show that f ⋁ ⊆ 1_{DC}. But f preserves sups so we have

f ⋁ ≅ ⋃ f_{!} ⊆ ⋁_{!} f_{!} = (⋁ f)_{!} ≅ (1_{C})_{!} = 1_{DC} where the containment is an instance of the inequality that precedes the theorem statement.

7 Tensor products

In [16] it was shown that Grothendieck’s notion of nuclear object makes sense in a symmetric monoidal closed category. To wit, L is nuclear if and only if, for all M, the canonical arrow L^{∗} ⊗M ⟶ [L, M] is an isomorphism, where L^{∗} is [L, I], I being the unit object. The author noted that it suffices for the condition to hold for M = L. In a subsequent paper, [7], the condition was explored in the symmetric monoidal closed category sup = sup(set) and it was shown that the nuclear objects are precisely the completely distributive lattices. If the axiom of choice holds in set then completely distributive is equivalent to (CCD), [6], so it is reasonable to expect that nuclearity is constructively equivalent to (CCD) — of course over an arbitrary topos, E.

The monoidal structure of sup = sup(E) was used extensively in [10]. We recall that the unit object is Ω so that L^{∗} is [L, Ω] while L^{op} is isomorphic to [L, Ω^{op}]. There is a comparison L^{∗} ⟶ L^{op} in sup, namely [L, ¬] , where ¬ is negation for Ω. Thus ( )^{∗}, as used in [7], is isomorphic to ( )^{op}. if and only if the base is Boolean. Following [10] we define ( )^{0} : sup^{op} ⟶ sup by (f : L ⟶ M)^{0} = (f_{∗})^{op} : L^{op} ⟶ M^{op}. Note that various expressions involving ( )^{∗} in [7] become expressions involving ( )^{0} in the context of [10] but the definition of nuclearity is not one of them!

Temporarily confusing are the observations that ( )^{∗} for the monoidal category (kar(rel), − × −, 1) is ( )^{op} and that in this monoidal category every object is nuclear. Both follow from the adjunction − × X ⊣ X^{op} × − given in Proposition 2. Now the monoidal structure of ccd_{sup} as in Corollary 18 is that given by transport of structure along the biequivalence ccd_{sup} ⟶^{∼} kar(rel), so it follows that relative to this monoidal structure every (CCD) lattice is nuclear. Provisionally writing ( )^{#} for the transported ( )^{∗} and \overline{⊗} for the transported tensor, L^{#}\overline{⊗}M is the internal hom in ccd_{sup}.

Lemma 37 The usual monoidal structure of sup restricts to ccd_{sup} and the resulting structure is equivalent to the one above.

Proof. The unit for the transported structure is ID1(= D1 = P1) = Ω, which is the unit for the tensor in sup . It now suffices to show that the transported internal hom is equivalent to that of sup . So we have to show that for (CCD) lattices L and M, L^{#}\overline{⊗}M is suitably isomorphic to [L, M]. But the underlying ord-object functor, sup ⟶ ord, is given by sup(Ω, −) and we have

sup(Ω, L^{#}\overline{⊗}M) = ccd_{sup}(Ω, L^{#}\overline{⊗}M) ≅ ccd_{sup}(L, M) = sup(L, M) ≅ sup(Ω, [L, M])

from which the result follows.

In particular, ( )^{#} is just the restriction of the usual ( )^{∗} for sup and the following summarizing statements may be helpful:

i) ( )^{0} : sup^{op} ⟶ sup is an involution.

ii) ( )^{0} restricts to ccd_{sup}^{op} ⟶ ccd_{sup} if and only if E is Boolean.

iii) ( )^{∗} restricts to ccd_{sup}^{op} ⟶ ccd_{sup}.

iv) ( )^{∗} : ccd_{sup}^{op} ⟶ ccd_{sup} is an involution.

v) For any infosys X, (IDX)^{∗} ≅ ID(X^{op}).

Note that statement ii), which has not been discussed above, was a central result of [13].

Theorem 38 A complete lattice is nuclear if and only if it is (CCD).

Proof. If L is (CCD) then by Lemma 37 we have L^{∗} ⊗ L ≅ [L, L] which shows that L is a nuclear object of sup . Conversely, assume that for all M in sup we have L^{∗} ⊗M ≅ [L, M] and let e : M ⟶ N be cofully faithful in sup . Then L^{∗} ⊗ e : L^{∗} ⊗ M ⟶ L^{∗} ⊗ N is cofully faithful. (We skip the details of this claim. It is best understood at this level of generality in terms of the theory in [2]. Certainly though if orders are antisymmetric then it is clear. For in that case we are simply saying that the left adjoint, L^{∗} ⊗ −, preserves epimorphisms.) Hence [L, e] : [L, M] ⟶ [L, N] is cofully faithful in sup. Now the arrow sup(L, e) : sup(L, M) ⟶ sup(L, N), in ord has a right adjoint such that we can construct the requisite lifting which shows that L is a universal projective in sup. Thus, by Theorem 36, L is (CCD).

8 Adjoint Sequences

In this section we characterize DX for X a sup lattice and for X a (CCD) lattice in terms of extra adjoints. We will refer to the following situation:

[figure: L; DL; ⋁; ↓; ⇓; \⋁; ⊥; ⊥; ⊥]

This configuration was considered by R-E. Hoffmann [8] for continuous posets. There in place of down-closed subsets he considered down-closed and up-directed subsets. Some of our proofs below are similar to his but a more systematic use of adjointness makes them constructive.

For S ∈ DL we have S ⊆ ⇓b if and only if (∀s ∈ S)(s ≪ b) so that b is an “upper bound” with respect to ≪ of S. To say that there exists \⋁ ⊣ ⇓ is to say that every S ∈ DL has a ≤-least ≪-upper bound. We define \overline{a} = \⋁ ↓ a, so that \overline{a} is the smallest “element” x such that a ≪ x.

Lemma 39 \overline{a} is totally compact.

Proof. We have a ≪ \overline{a} which implies (∃b)(a ≪ b ≪ \overline{a}). Now \overline{a} ≤ b, by universality of \overline{a}, hence \overline{a} ≤ b ≪ \overline{a} and so \overline{a} ≪ \overline{a}.

As in Section 4, write X = X (L) for the inverter of ⇓ ⊆ ↓ i. e. {x ∈ L | x ≪ x}.

Lemma 40 There is an adjunction: [figure: X; L; ⊥; \overline{( )}] and hence X is a sup lattice.

Proof. From a ≪ \overline{a} we have a ≤ \overline{a}, so if \overline{a} ≤ x then a ≤ x. Conversely, for x ∈ X, if a ≤ x then a ≤ x ≪ x gives a ≪ x, whence \overline{a} ≤ x.

Theorem 41 For a sup lattice L, we have

[figure: L; DL; ⋁; ↓; ⇓; \⋁; ⊥; ⊥; ⊥]

if and only if L ≅ DX for some sup lattice X.

Proof. (if) For a sup lattice X we have [figure: X; DX; ↓_{X}; ⋁; ⊥] which, as noted prior to Theorem 36, gives

[figure: DX; DDX; D ↓_{X}; ↓_{DX}; (↓_{X})_{!}; ⋁!; ⊥; ⊥; ⊥; .]

(only if) Assuming \⋁ ⊣ ⇓ ⊣ ⋁ ⊣ ↓ for L we show first that L is totally algebraic. It suffices to show that (∀a)(a ≤ ⋁{x | x ≪ x ≤ a} ^{}).

We have a ≤ ⋁{b | b ≪ a} since L is (CCD)
≤ ⋁\{\overline{b} | b ≪ a\}  since b ≤ \overline{b}
≤ ⋁\{x | x ≪ x ≤ a\} since \{\overline{b} | b ≪ a\} ⊆ \{x | x ≪ x ≤ a\}.

From [6] and as noted at the beginning of Section 4 we have

[figure: X; L; X; DX; ↓; ≃; =]

where X = X (L). Lemma 40 already shows that X is a sup lattice and clearly the equivalence identifies \overline{( )} and ⋁_{X}.

Theorem 42 For a sup lattice L, we have

[figure: L; DL; ⋁; ↓; ⇓; \⋁; ∨; ⊥; ⊥; ⊥; ⊥]

if and only if L ≅ DX for some (CCD) lattice X.

Proof. (if) Applying D to the configuration of adjoints which defines (CCD) produces the configuration above.

(only if) By Theorem 41 we have L ≅ DX, (X = X (L)) X a sup lattice. It suffices to show that X is (CCD). Now consider

[figure: X; DX; ⋁; DX; DDX; ↓_{X}; ↓_{DX}; ∨; \⋁ = ⋁_{!}; ⊥; =]

which we have by assumption and general considerations. The left adjoint to ⋁ = ⋁_{X} is ⋁_{DX} · ∨· ↓_{X} .

Similar results for longer adjoint sequences terminating at ↓ follow by induction.

References

[1] B. Banaschewski and S. B. Niefield. Projective and supercoherent frames. Journal of Pure and Applied Algebra, 70:45–51, 1991.

[2] A. Carboni, G. M. Kelly, and R. J. Wood. A 2-categorical approach to change of base and geometric morphisms 1. Cahiers de topologie et géometrie différentielle catégoriques, XXXII:47–95, 1991.

[3] A. Carboni and R. Street. Order ideals in categories. Pacific Journal of Mathematics, 124(2):275–278, 1986.

[4] C.J.Mulvey. Intuitionistic algebra and representation of rings. Memoirs of the AMS, 148:3–57, 1974.

[5] R. Guitart et J. Riguet. Envelopes karoubiennes de catégories de kleisli. Cahiers de topologie et géometrie différentielle catégoriques, XXX:261– 266, 1992.

[6] B. Fawcett and R. J. Wood. Constructive complete distributivity I. Math. Proc. Cam. Phil. Soc., 107:81–89, 1990.

[7] D. A. Higgs and K. A. Rowe. Nuclearity in the category of complete semi-lattices. Journal of Pure and Applied Algebra, 57:67–78, 1989.

[8] R-E. Hoffmann. Continuous posets and adjoint sequences. Semigroup Forum, 18:173–188, 1979.

[9] P. T. Johnstone. Stone Spaces. Cambridge University Press, 1982.

[10] A. Joyal and M. Tierney. An Extension of the Galois Theory of Grothendieck. Memoirs of the American Mathematical Society No. 309, American Mathematical Society, 1984.

[11] F.W. Lawvere. Metric spaces, generalized logic and closed categories. Rendiconti del Seminario Matematico e Fisico di Milano, 43:135–166, 1973.

[12] G. N. Raney. A subdirect-union representation for completely distributive complete lattices. Proc. Amer. Math. Soc., 4:518–512, 1953.

[13] R. Rosebrugh and R. J. Wood. Constructive complete distributivity II. Math. Proc. Camb. Phil. Soc., 110:245–249, 1991.

[14] R. Rosebrugh and R. J. Wood. Constructive complete distributivity III. Canadian Mathematical Bulletin, 35:537–547, 1992.

[15] R. Rosebrugh and R. J. Wood. Constructive complete distributivity V. in preparation, 1993.

[16] Keith Rowe. Nuclearity. Canadian Mathematical Bulletin, 31:227–235, 1989.

[17] R. Street and R. F. C. Walters. Yoneda structures on 2-categories. Journal of Algebra, 50:350–379, 1978.

[18] S. Vickers. Information systems for continuous posets. Theoretical Computer Science B, 1993.

[19] R. J. Wood. Proarrows 1. Cahiers de topologie et géometrie différentielle catégoriques, XXIII:279–290, 1982.

[20] R. J. Wood. Proarrows 2. Cahiers de topologie et géometrie différentielle catégoriques, XXVI:135–168, 1985.