Theory and Applications of Categories, Vol. 22, No. 1, 2009, pp. 1–23.

DUALITY FOR CCD LATTICES

FRANCISCO MARMOLEJO, ROBERT ROSEBRUGH, AND R.J. WOOD

Abstract. The 2-category of constructively completely distributive lattices is shown to be bidual to a 2-category of generalized orders that admits a monadic schizophrenic object biadjunction over the 2-category of ordered sets.

1. Introduction

1.1. Constructively completely distributive (CCD) lattices were introduced in [F&W] and further studied in the series of papers [RW2], [RW3], [RW4], [P&W], [MRW], [RWb], and [CMW] . For background not explicitly given here, we refer the reader to [RW4]. For an ordered set (A, ≤), a subset S of A is said to be a downset if b ≤ a ∈ S implies b ∈ S. The downsets of the form ↓a = {b | b ≤ a} are said to be principal. Denote by DA the lattice of downsets ordered by inclusion. Recall that an ordered set (A, ≤) is said to be complete if the embedding of principal downsets ↓: A [figure]DA has a left adjoint ⋁ : DA [figure]A. If ⋁ has a left adjoint ⇓ : A [figure]DA then A is said to be constructively completely distributive. Recall too that, for any complete ordered set (A, ≤), the totally below relation is defined by b ≪ a if and only if (∀S ∈ DA)(a ≤ ⋁S ⟹ b ∈ S). To say that A is CCD is equivalent to

(∀a ∈ A)(a = ⋁{b | b ≪ a})

A restricted class of CCD lattices, called totally algebraic in [RW4], are those complete A for which

(∀a ∈ A)(a = ⋁{b | b ≪ b ≤ a})

1.2. At the International Category Theory Conference held in Vancouver in 1997, Paul Taylor raised two questions about the adjunction

ord(−, Ω)^{op} ⊣ ord(−, Ω) : ord^{op} [figure]ord

Here ord is the 2-category of ordered sets, order-preserving functions, and inequalities and Ω is the subobject classifier of the base topos S, which is not assumed to be Boolean. i) What are the algebras for the generated monad?

The authors gratefully acknowledge financial support from the Canadian NSERC. Diagrams typeset using M. Barr’s diagxy package

Received by the editors 2008-10-06 and, in revised form, 2009-01-25.

Transmitted by Susan Niefield. Published on 2009-01-28.

2000 Mathematics Subject Classification: 18A25.

Key words and phrases: adjunction, completely distributive, idempotent, monadic, proarrow equipment, cauchy complete.

\begin{matrix}c \\ ◯ \end{matrix} Francisco Marmolejo, Robert Rosebrugh, and R.J. Wood, 2009. Permission to copy for private use granted.

ii) Is ord(−, Ω) monadic?

Taylor had conjectured that the answer to his first question is ccd, the 2-category of CCD lattices, order preserving functions that have both left and right adjoints and inequalities. In [MRW] this was affirmed and the second question was answered negatively by recalling from [RW4] that ord^{op} is biequivalent to the full subcategory of ccd determined by the totally algebraic lattices described in 1.1. (More precisely, we should say that ord_{cc}^{op}, the ord-category of antisymmetric ordered sets, is biequivalent to that of totally algebraic lattices. The (−)_{cc} terminology will be explained in the sequel.)

1.3. Nevertheless, there is value in expanding on the second question, which sought to generalize Paré’s celebrated result in [PAR] that Ω^{(−)} : S^{op} [figure]S is monadic, for S any elementary topos. However, since ord is a 2-category and earlier results on CCD lattices fully exploited the extra dimension we asked:

iii) Is there a bimonadic schizophrenic object biadjunction whose domain is biequivalent to ccd?

The answer we give here was anticipated in [RW4] but is somewhat subtle. Write idm for a certain 2-category in which the objects (X, <) consist of a set together with a transitive, interpolative relation and the arrows are functions that preserve the relation. The 2-category ccd is biequivalent to idm_{cc}^{op}, where idm_{cc} is the full sub-2-category of idm consisting of the Cauchy complete objects. The emphasized term refers to a slight generalization of the concept given by F.W. Lawvere in [LAW]. What is truly new here is that idm_{cc}(−, iΩ) : idm_{cc}^{op} [figure]ord, where iΩ is the subobject classifier seen as an object of idm, is bimonadic.

1.4. Lawvere’s definition of Cauchy completeness was given for categories enriched over a symmetric monoidal category V, in terms of the pseudofunctor (−)_{∗}: V-cat [figure]V-prof which sends a V-functor f : A [figure]B to the V-profunctor f_{∗} = B(−, f−) : A [figure]B. The 2-category idm, is not of the form V-cat for some V. However, there is a a pseudofunctor (−)_{#} : idm [figure]krl, where krl is the idempotent splitting completion of rel, the 2-category of sets, relations, and containments, such that (−)_{#} shares important properties with the (−)_{∗}: V-cat [figure]V-prof. Such pseudofunctors were called proarrow equipments in [Wd1] and [Wd2] and already in [RW4] they were used to study CCD lattices. Moreover, it was recognized in [RW4] that Cauchy completeness could be defined in the generality of proarrow equipment and that applied to (−)_{#} : idm [figure]krl it expressed results about left adjoints in krl in terms of arrows in idm. We refer here to Remark 22 and the last paragraph of Section 4 in [RW4]. What was not understood in [RW4] was that the ordered set of (strong) downsets DX of an object of idm is equivalent to the ordered set idm(X^{op}, iΩ) and that iD provides a very special right biadjoint to (−)_{#} : idm [figure]krl. The use of equivalences, as opposed to isomorphisms, of ordered sets is critical throughout this paper.

1.5. In Section 2 we review proarrow equipment in a general way and give examples, before introducing the idea of a KZ-adjunction. These are to KZ-doctrines what ordinary adjunctions are to ordinary monads. We define existence of power objects relative to a proarrow equipment (−)_{∗}: K [figure]M to mean the existence of a right KZ-adjoint for (−)_{∗}: K [figure]M. The general KZ-adjunction simplifies considerably in this case and we explore precisely what is needed to provide power objects. Any proarrow equipment (−)_{∗}: K [figure]M factors to give (−)_{∗} : K [figure]mapM, where mapM is the locally full subbicategory of M determined by the left adjoints. In Section 3 we define existence of Cauchy completions relative to (−)_{∗} to mean the existence of a strong right KZ-adjoint for (−)_{∗}: K [figure]mapM. Strong KZ-adjunctions are to KZ-adjunctions what pseudo idempotent pseudomonads are to KZ-doctrines. We prove some basic results about the relationship between power objects and Cauchy completions, noting in particular that power objects are Cauchy complete. In Section 4 we introduce (−)_{#} : idm [figure]krl formally and provide a full context for it, especially relative to ordered sets and order ideals. The most important result of this section is Proposition 4.12 which, together with power objects for (−)_{#} : idm [figure]krl, provides the essential ingredients setting this work apart from earlier CCD papers. In Section 5 we apply the results of Sections 2 and 3 to (−)_{#} : idm [figure]krl, identifying some additional features present in this example, notably that the dual, Y^{op}, of a Cauchy complete object Y is also Cauchy complete. Finally, in Section 6 we assemble what we have developed so as to state and prove the main bimonadicity result.

2. Proarrow Equipments Redux and Power Objects

2.1. For K and M bicategories, a pseudofunctor (−)_{∗}: K [figure]M is said to be proarrow equipment in the sense of [Wd1] and [Wd2] if

i) (−)_{∗} is the identity on objects;

ii) (−)_{∗} is locally fully faithful;

iii) (for all f : A [figure]B in K) (there is an adjunction f_{∗} ⊣ f^{∗}: B [figure]A in M).

We can regard K via (−)_{∗} as a locally-full subbicategory of M. In the context of proarrow equipment, an arrow in K is representably fully faithful if and only if its given adjunction in M has an invertible unit. It is in fact unambiguous in this context to call such an arrow in K fully faithful.

2.2. As examples of proarrow equipment we mention:

i) (−)_{∗}: V-cat [figure]V-prof, for a cocomplete symmetric monoidal category V. Here for a V-functor f : B [figure]A, the V-profunctor f_{∗}: B [figure]A is given by f_{∗}(a, b) = A(a, fb).

ii) (−)_{#} : V-tax [figure]V-dist, for a cocomplete symmetric monoidal category V. The objects of V-tax are V-taxons (called V-taxonomies in [KOS]). Taxons are similar to categories except that the existence of identity data is replaced by the requirement that the associativity of composition diagram (suitably expressed) be a coequalizer. The arrows are what might be called V-semi-functors. The arrows of V-dist, that we call V-distributors, are the i-modules of [KOS]. The 2-cells of V-tax are defined by generalizing Mac Lane’s “arrows only” description of natural transformations. (See [MAC], page 19.) This paper will involve a very special case of this example and we forego further mention of the general case, referring the interested reader to [KOS].

iii) (−)_{∗} : TOP_{geo} [figure]TOP_{lex}^{co}, in which a geometric morphism between toposes is sent to its direct image. This example was studied extensively in [RWp] and [RWc].

iv) The previous example is a special case of mapM [figure]M which is proarrow equipment, for M an arbitrary bicategory. Here mapM is the locally full subbicategory of M determined by the left adjoint arrows. We follow the convention of calling a left adjoint arrow a map.

v) (−)_{∗}: set [figure]rel, which sends a function f : B [figure]A to its graph f_{∗}: B [figure]A so that af_{∗}b if and only if a = fb.

2.3. In [LAW] an object B in V-cat was said to be Cauchy complete if, for all A, every adjunction L ⊣ R : B [figure]A in V-prof arises as one of the form f_{∗} ⊣ f^{∗} : B [figure]A for an f : A [figure]B in V-cat. It is clear immediately that for any proarrow equipment (−)_{∗}: K [figure]M one can define an object Y in K to be Cauchy complete if, for every map L: X [figure]Y in M, there is an arrow f : X [figure]Y in K and an isomorphism f_{∗} ≅ L in M. If V is complete, the question of Cauchy completeness of an object B in V-cat can be concentrated in a single V-functor, the inclusion of B in its Cauchy completion B [figure]QB, making the condition far more tractable. We turn shortly to the possibility of doing this for a general proarrow equipment (−)_{∗}: K [figure]M.

2.4. It will be convenient to write S: K [figure]M for a general pseudofunctor and recall the concept of a right biadjoint P : M [figure]K for S. In addition to the pseudofunctors S and P, a biadjunction (S ⊣ P; y, e; η, ϵ) consists of a unit y: 1_{K} [figure]PS, a counit e: SP [figure]1_{M}, and invertible constraints ϵ and η as shown below.

[figure: S; SPS; Sy; S; S; 1_{S}; SPS; S; eS; ϵ; PSP; P; yP; PSP; P; Pe; P; P; 1_{P}; η]

The constraints ϵ : eS.Sy [figure]1_{S} and η : 1_{P} [figure]Pe.yP for a biadjunction are required to satisfy coherence equations, for which [S&W] is a convenient reference. But since our application will be to locally ordered M, the coherence equations are not relevant for this paper. In [M&W] it was shown that to give an adjunction Sy ⊣ eS, with unit ϵ^{−1} (and components in M), is to give an adjunction Pe ⊣ yP, with counit η^{−1} (and components in K). Moreover, Sy ⊣ eS is an adjoint equivalence if and only if Pe ⊣ yP is an adjoint equivalence. A biadjunction (S ⊣ P; y, e; η, ϵ) satisfying either of the equivalent conditions

Sy ⊣ eS with unit ϵ^{−1}  (1)

or

Pe ⊣ yP with counit η^{−1}  (2)

is called a KZ-adjunction. It should be noted that for such a biadjunction, for each object X in K, the component SyX is necessarily fully faithful in M and, for each object Y in M, the component yPY is necessarily fully faithful in K. A KZ-adjunction will be said to be strong if the counit for the adjunction Sy ⊣ eS is also invertible, equivalently the unit for the adjunction Pe ⊣ yP is also invertible. It was shown in [M&W] that a KZ-adjunction generates a KZ-doctrine on K and that a strong KZ-adjunction generates a pseudo-idempotent pseudomonad on K.

2.5. A proarrow equipment (−)_{∗}: K [figure]M is said to have power objects if it has a right KZ-adjoint. Since (−)_{∗} is the identity on objects, the notion of KZ-adjunction simplifies in this case. We will show in the next four subsections that to give a right KZ-adjoint for a proarrow equipment (−)_{∗}: K [figure]M is to give, for each object Y, an arrow y_{Y} : Y [figure]PY in K with invertible unit 1_{Y} [figure]y_{Y} ^{∗}y_{Y} _{∗} in M so that, for each object X, composition with y_{Y} ^{∗}: PY [figure]Y preceded by (−)_{∗} provides an equivalence of categories

K(X, PY) [figure: y_{Y}^{∗} (−)_{∗}] M(X, Y)  (3)

2.6. Lemma. The equivalence (3) provides, for each M : X [figure]Y in M, a diagram

[figure: PY; Y; y_{Y}^{∗}; X; PY; m_{∗}; X; Y; M; μ]

with m in K and invertible μ, universal among diagrams of the form

[figure: PY; Y; y_{Y}^{∗}; X; PY; n_{∗}; X; Y; M; ν]

for n in K and arbitrary ν. Moreover if ν is invertible then the induced n [figure]m is invertible.

Proof. Given M : X [figure]Y in M we find m : X [figure]PY in K and invertible μ as shown using the essential surjectivity of y_{Y}^{∗} (−)_{∗}. For the universal property, assume that we have n: X [figure]PY in K and arbitrary ν: y_{Y}^{∗} n_{∗} [figure]M. In this event we have μ^{−1}.ν: y_{Y}^{∗} n_{∗} [figure]y_{Y}^{∗} m_{∗}. By fully faithfulness of y_{Y}^{∗} (−)_{∗} there is a unique 2-cell τ : n [figure]m in K so that the whisker composite y_{Y}^{∗} τ_{∗} is equal to the pasting of μ^{−1} to ν along M. Of course this immediately says that τ is unique with the property that τ_{∗} pasted to μ along m^{∗} is equal to ν. If ν is invertible then invertibility of τ follows from fully faithfulness of y_{Y}^{∗} (−)_{∗}.

2.7. It is now standard that P: M [figure]K is given on arrows by requiring, for M : X [figure]Y in M, that PM be obtained from the procedure of Lemma 2.6 applied to My_{X}^{∗} as in the diagram

[figure: PY; Y; y_{Y}^{∗}; PX; PY; (PM)_{∗}; PX; Y; PX; X; y_{X}^{∗}; X; Y; M; ≅]  (4)

(with the universal property of that in Lemma 2.6). From the universal property, we deduce the effect of P on 2-cells. Moreover, pseudofunctoriality of P with respect to composition follows from consideration of

[figure: PY; Y; y_{Y}^{∗}; PX; PY; (PM)_{∗}; PX; Y; PX; X; y_{X}^{∗}; X; Y; M; ≅; Y; Z; N; PY; PZ; (PN)_{∗}; PZ; Z; y_{z}^{∗}; ≅; PX; PZ; (P(NM))_{∗}; X; Z; NM]

Here each of the smaller triangle, the trapezoid, and the entire region are as provided by Lemma 2.6. It follows from the universality of P(NM) that we have an isomorphism (PN)(PM) [figure]P(NM) in K. Pseudofunctoriality with respect to identities is even easier and left for the reader.

2.8. The un-named isomorphisms given by (4) provide the pseudonaturalities for a pseudonatural transformation y^{∗}: (−)_{∗}P [figure]1_{M}, playing the role of e in 2.4. Taking mates we have, for each M : X [figure]Y in M, a 2-cell y_{Y} _{∗}M [figure](PM)_{∗}y_{X}_{∗} in M. In particular, for each k: X [figure]Y in K we have

y_{Y} _{∗}k_{∗} [figure](Pk_{∗})_{∗}y_{X}_{∗} and y_{X}_{∗}k^{∗} [figure](Pk^{∗})_{∗}y_{Y} _{∗}

For each k in K, the first of these gives, by pseudofunctoriality and local fully faithfullness of (−)_{∗}, a 2-cell y_{Y} k [figure](Pk_{∗})y_{X} in K, the second has a mate (Pk_{∗})_{∗}y_{X}_{∗} [figure]y_{Y} _{∗}k_{∗} in M (using (Pk^{∗})_{∗} ≅ (Pk_{∗})^{∗} via pseudofunctoriality of P) and this last gives a 2-cell (Pk_{∗})y_{X} [figure]y_{Y} k in K, provably inverse to y_{Y} k [figure](Pk_{∗})y_{X}. Again, it follows that the isomorphisms y_{Y} k [figure](Pk_{∗})y_{X} provide the pseudonaturalities for a pseudonatural transformation y : 1_{K} [figure]P(−)_{∗}. Turning again to the terminology of subsection 2.4, we can construct the invertible constraint ϵ by using the inverses for the unit of the family of adjunctions y_{X}_{∗} ⊣ y_{X}^{∗} since we have y fully faithful. To construct the constraint η, consider

[figure: PY; Y; y_{Y}^{∗}; PPY; PY; (P(y_{Y} ^{∗})_{∗}; PPY; Y; PPY; PY; ^{y_{PY} ^{∗}}; PY; Y; ^{y_{Y} ^{∗}}; ≅; PY; PPY; ^{y_{PY} ^{∗}}; PY; PY; ^{1_{PY} ^{∗}}; PY; PY; ^{1_{PY} ^{∗}}; ≅]

The triangle is as provided by Lemma 2.6 while the other displayed isomorphism is another instance of the fully faithfulness of y. Finally since the entire region can also be seen as an instance of the diagram in Lemma 2.6, universality provides us with a unique isomorphism P(y_{Y} ^{∗})y_{PY} [figure]1_{PY} in K whose image under (−)_{∗} coheres with the pasting of the other isomorphisms in the diagram. This completes the exhibition of the data needed for a biadjunction (−)_{∗} ⊣ P. Again we point out that since our application will be to locally ordered bicategories, verification of 2-cell equations will not be considered here.

2.9. By the very construction of the counit e as y^{∗} we have (1) so that the biadjunction (−)_{∗} ⊣ P has the KZ-property. Finally, we note that the defining fully faithful adjoint string, in the sense of [MAR], showing that (P(−)_{∗}, y) is a KZ-doctrine on K is given by

[figure: PY; PPY; P(y_{Y} _{∗}); PY; PPY; P(y_{Y} ^{∗}); PY; PPY; y_{PY}; ⊥; ⊥]  (5)

2.10. Remark. It should not be supposed that all proarrow equipments with right biadjoints provide KZ-adjunctions. For example, the proarrow equipment (−)_{∗}: set [figure]rel which sends a function to its graph has the power set construction as right adjoint. The unit is singleton with components {−}_{Y} : Y [figure]PY; the counit is membership with components ∈_{Y} : PY [figure]Y and ∈_{Y} is not the right adjoint of the graph of {−}_{Y} in rel.

3. Cauchy Completion Relative to Proarrow Equipments

3.1. We now consider the question of existence of a strong right KZ-adjoint Q for (−)_{∗} : K [figure]mapM. From the general discussion in Section 2 we see that to give such a biadjunction (−)_{∗} ⊣ Q it suffices to give, for each object Y, an arrow z_{Y} : Y [figure]QY in K with invertible unit 1_{Y} [figure]z_{Y} ^{∗}z_{Y} _{∗} and invertible counit z_{Y} _{∗}z_{Y} ^{∗} [figure]1_{QY} in mapM so that, for each object X, composition with e: QY [figure]Y preceded by (−)_{∗} provides an equivalence of categories

K(X, QY) [figure: z_{Y} ^{∗}(−)_{∗}] mapM(X, Y)  (6)

It should be noted that to say z^{∗} is the counit for the biadjunction (−)_{∗} ⊣ Q makes the components z_{Y} ^{∗} themselves maps in M. The proof of the following Lemma is easily adapted from that of Lemma 2.6.

3.2. Lemma. The equivalence (6) provides, for each map L: X [figure]Y in M, a diagram

[figure: QY; Y; z_{Y}^{∗}; X; QY; l_{∗}; X; Y; L; λ]

with l in K and invertible λ, universal among diagrams of the form

[figure: QY; Y; z_{Y}^{∗}; X; QY; n_{∗}; X; Y; L; ν]

for n in K and arbitrary ν.

3.3. Just as we did for (P, y), we can carry out a similar discussion for (Q, z) to show that our assumptions about z_{Y} : Y [figure]QY lead to a strong KZ-adjunction (−)_{∗} ⊣ Q : mapM [figure]K which in turn leads to a string of adjoint equivalences

[figure: QY; QQY; Q(z_{Y} _{∗}); QY; QQY; Q(z_{Y} ^{∗}); QY; QQY; z_{QY}; ⊥; ⊥]  (7)

showing that (Q(−)_{∗}, z) is a pseudo-idempotent pseudo monad on K. In this generality we refer to z_{Y} : Y [figure]QY as the Cauchy completion of Y and we say that the proarrow equipment (−)_{∗}: K [figure]M has Cauchy completions if (−)_{∗}: K [figure]mapM has a strong right KZ-adjoint. In any bicategory K, an arrow s: X [figure]Y is a pseudo section if there is an arrow r: Y [figure]X and an isomorphism 1_{X} ≅ rs. For a pseudo-idempotent pseudo monad (T , t) on any bicategory K, it is standard that an object Y in K underlies a (T , t)-algebra if and only if t_{Y} : Y [figure]T Y is an equivalence if and only if t_{Y} : Y [figure]T Y is a pseudo section. We recall from 2.3 that an object Y in K is Cauchy complete if, for every map L: X [figure]Y in M, there is an arrow f : X [figure]Y in K and an isomorphism f_{∗} ≅ L in M. Since (−)_{∗} : K(X, Y) [figure]mapM(X, Y) is in any event fully faithful, we see that Y is Cauchy complete if and only if, for all X, (−)_{∗} : K(X, Y) [figure]mapM(X, Y) is an equivalence of categories.

3.4. Proposition. For a proarrow equipment (−)_{∗}: K [figure]M such that (−)_{∗}: K [figure]mapM has a strong right KZ-adjoint Q with unit z, an object Y in K is Cauchy complete if and only if it is a (Q(−)_{∗}, z) algebra if and only if z_{Y} : Y [figure]QY is a pseudo section in K.

Proof. Only the first part of the statement requires comment. Consider

[figure: K(X, QY); mapM(X, QY); (−)_{∗}; K(X, Y); K(X, QY); K(X,z_{Y} ); K(X, Y); mapM(X, QY); mapM(X, QY); mapM(X, Y); mapM(X,z_{Y} ^{∗}); K(X, Y); mapM(X, Y); (−)_{∗}; ≅]

which commutes to within isomorphism since z_{Y} is fully faithful. Our global assumption ensures that the bottom side of the triangle is an equivalence of categories (and we use here that z_{Y} ^{∗} is also a map in M). Now Y is Cauchy complete if and only if, for all X, the hypotenuse is an equivalence of categories which is so if and only if, for all X, K(X, z_{Y}) is an equivalence of categories if and only if z_{Y} : Y [figure]QY is an equivalence in K.

3.5. We assume now that we have both P and Q as above. Because mapM(X, Y) is a full subcategory of M(X, Y), for all X, we have K(X, QY) a full subcategory of K(X, PY), for all X, so that by the bicategorical Yoneda lemma we have i_{Y} : QY [figure]PY in K representably fully faithful. Hence 1_{QY} [figure]i_{Y} ^{∗}i_{Y} _{∗}. is invertible. From pseudonaturality we have

[figure: mapM(QY, Y); M(QY, Y); K(QY, QY); mapM(QY, Y); z^{∗}(−)_{∗}; K(QY, QY); K(QY, PY); K(QY,i); K(QY, PY); M(QY, Y); y^{∗}(−)_{∗}; ≅]

and

Chasing the identity on QY around the first diagram and z_{Y} around the second diagram we have isomorphisms with the first in M and the second in K (since it results from y^{∗}(iz)_{∗} ≅ z^{∗}(z)_{∗} ≅ 1_{Y} ≅ y^{∗}(y)_{∗} and y^{∗}(−)_{∗} being an equivalence is a fully faithful functor). It follows immediately that i(−)_{∗} : Q(−)_{∗} [figure]P(−)_{∗} is a morphism of pseudomonads. It will be a convenient abuse of notation to omit (−)_{∗} in such contexts and speak of P and Q as pseudomonads on K and i: Q [figure]P as a morphism of pseudomonads. An example is our usage in:

[figure: mapM(Y, Y); M(Y, Y); K(Y, QY); mapM(Y, Y); z^{∗}(−)_{∗}; K(Y, QY); K(Y, PY); K(Y,i); K(Y, PY); M(Y, Y); y^{∗}(−)_{∗}; ≅] [figure: Y; QY; ^{z_{Y} ^{∗}}; Y; PY; ^{y_{Y} ^{∗}}; QY; PY; ^{i_{Y} ^{∗}}; ≅; and; Y; QY; z_{Y}; Y; PY; y_{Y}; QY; PY; i_{Y}; ≅]

3.6. Proposition. The morphism of pseudofunctors zP: P [figure]QP is an equivalence.

Proof. By Proposition 3.4, it suffices to show that each zPY : PY [figure]QPY is a pseudo section. But from

(y^{∗}PY.iPY).zPY ≅ y^{∗}PY.(iPY.zPY) ≅ y^{∗}PY.yPY ≅ 1_{P}Y

(using the second triangle in 3.5 instantiated at Py) we see this is so.

3.7. Corollary. Any object of the form PY in K is Cauchy complete.

3.8. We denote by K_{cc} the full sub 2-category of K determined by the Cauchy complete objects. Any object of the form QY is Cauchy complete (since Q is a pseudo-idempotent pseudomonad). If, for each Y in K, the Cauchy completion of Y exists then it is a formality that (−)_{∗}: K_{cc} [figure]mapM is a biequivalence with inverse given by Q.

4. Proarrow Equipments for Orders and Idempotents

4.1. As with earlier papers on CCD lattices, we would like to make our work constructive so that in the sequel the word set refers to an object of the base topos S. The words ordered set refer to a set together with a reflexive and transitive relation, what some authors call a preordered set. Many of the ordered sets (A, ≤) that we consider are definitely not anti-symmetric. We write ord for the 2-category of ordered sets, orderpreserving functions, and inequalities. We always have in mind that ord is a symmetric monoidal 2-category via its finite products and most categories occurring in the rest of this paper are ord-categories in the sense of enriched category theory. In fact, ord is itself Ω-cat. (The subobject classifier Ω is an ordered set with finite products which endow it with symmetric monoidal structure.) For much of this paper it would be possible to replace Ω by a general symmetric monoidal category V. However, we limit further mention of Ω-cat to this section while we clarify the relationship of ord, especially in the context of proarrow equipment, with a more general ord-category of sets equipped with a relation.

4.2. The bicategory of order ideals idl has objects those of ord and an arrow R: A [figure]B in idl is a relation R: A [figure]B for which ((b′ ≤ bRa ≤ a′) ⟹ (b′Ra′)). We have a 2-cell from R: A [figure]B to S: A [figure]B in idl if and only if the relation R is contained in S. It is easy to see that idl is Ω-prof and that idl is an ord-category. We have (−)_{∗}: ord [figure]idl, given by the identity on objects and, for f : A [figure]B in ord, we have f_{∗} : A [figure]B in idl given by bf_{∗}a if and only if b ≤ fa. For f : A [figure]B in ord, there is also f^{∗}: B [figure]A in idl, where af^{∗}b if and only if fa ≤ b. It is standard that f_{∗} ⊣ f^{∗} in idl and (−)_{∗}: ord [figure]idl is precisely the proarrow equipment of example i) of subsection 2.2 for the case of V = Ω. Moreover, (−)_{∗} : ord [figure]idl has a right KZ-adjoint that we call D, with DB being the lattice of downsets of B ordered by inclusion. Clearly

DB = idl(1, B) ≅ ord(B^{op}, Ω)

4.3. In [C&S] the authors studied the notion of Cauchy completeness of objects of ord. In the terminology of Section 3, (−)_{∗}: ord [figure]mapidl has a strong right KZ-adjoint (Cauchy completion) that sends an ordered set B to QB = {↓b | b ∈ B}, the set of principal downsets of B. This amounts to the antisymmetrization of B. In [C&S] it is shown that z_{B}: B [figure]QB is an equivalence, for each B, if and only if supports split in S.

4.4. An idempotent in the bicategory rel of relations consists of a set X together with a relation < : X [figure]X equal to its composite with itself. One containment providing the equality makes < transitive; the other makes it interpolative, meaning that if x < y then there exists z in X with x < z < y. Any order ≤ : X [figure]X provides an example of an idempotent in rel since interpolation can be realized trivially via reflexivity. It is convenient to read x < y as “x is below y”. If (X, <) and (Y, <) are idempotents then a function f : X [figure]Y is said to be below-preserving if x < x′ implies fx < fx′. Idempotents and below-preserving functions form a category that we denote idm_{0}. The category idm_{0} becomes an ord-category that we call idm as follows. For f, g: X [figure]Y in idm_{0} we define f ⪯ g to mean (∀x, x′ in X)(x < x′ ⟹ fx < gx′).

4.5. Another ord-category whose objects are the idempotents (X, <) is the idempotent splitting completion of rel. We call it krl (a contraction of “the Karoubian envelope of the category of relations”). From the standard description of idempotent splitting completions, an arrow R: (X, <) [figure](Y, <) in krl is a relation R: X [figure]Y such that

[figure: X; Y; R; X; X; <; X; Y; R; Y; Y; <; X; Y; R]

commutes. It follows that, for all y ∈ Y and x ∈ X we have

(∃y′)(y < y′Rx) iff yRx iff (∃x′)(yRx′ < x)

There is a 2-cell from R : X [figure]Y to S : X [figure]Y in krl if and only if the relation R is contained in S.

4.6. As explained in more detail in [RW4], for f : X [figure]Y in idm, we define f_{#} : X [figure]Y in krl by yf_{#}x if and only if (∃x′)(y < fx′ and x′ < x). We have also f^{#} : Y [figure]X with xf^{#}y if and only if (∃x′)(x < x′ and fx′ < y). It is easy to verify that both f_{#} and f^{#} are arrows in krl and that (−)_{#} : idm [figure]krl is a (strict) pseudofunctor. Moreover, if X and Y are idempotents in rel in virtue of being ordered sets then any such f is in ord, any arrow of krl is in idl and f_{#} = f_{∗} in idl. The following was stated in [RW4] after Proposition 1 but in that paper f ⪯ g: X [figure]Y was defined to mean that f_{#} ⊆ g_{#}.

4.7. Proposition. The pseudofunctor (−)_{#} : idm [figure]krl is proarrow equipment.

Proof. Proposition 1 of [RW4] showed that f_{#} ⊣ f^{#} in krl. We have only to show here that f ⪯ g if and only if f_{#} ⊆ g_{#} using our current definition of f ⪯ g. So assume f ⪯ g and for y ∈ Y, x ∈ X, assume that (∃x′)(y < fx′ and x′ < x). Interpolate x′ < x to get x′ < x′′ < x. Since f ⪯ g we have fx′ < gx′′ and hence (∃x′′)(y < gx′′ and x′′ < x). Conversely, assume f_{#} ⊆ g_{#} and x < x′. Interpolate x < x′ to get x < x′′ < x′ giving fx < fx′′ and x′′ < x′. Since f_{#} ⊆ g_{#} we have (∃x̄)(fx < gx̄ and x̄ < x′) from which follows fx < gx′.

4.8. It should not be supposed that (−)_{#} : idm [figure]krl is an ad hoc proarrow equipment. It is precisely the proarrow equipment of example ii) of subsection 2.2 for the case of V = Ω. In general, there is a 2-functor i: V-cat [figure]V-tax which interprets a V-category as a V-taxon. We have nothing further to say here about V-taxons and the like for general V. Rather, we will shortly exhibit a right KZ-adjoint to (−)_{#} : idm [figure]krl and a strong right KZ-adjoint (Cauchy completion) to (−)_{#} : idm [figure]mapkrl but we think that these are best understood as generalizations to their counterparts for ordered sets.

4.9. Consider the following diagram of ordinary categories and functors.

[figure: _{ord_{0}}; _{idm_{0}}; a; _{ord_{0}}; _{idm_{0}}; i; _{ord_{0}}; _{idm_{0}}; c; ⊥; ⊥]

Here i is the literal inclusion of orders as idempotents. For an idempotent X = (X, <), aX = (X, <∪ 1_{X}), where 1_{X} is the identity relation on X, and cX = ({x ∈ X|x < x}, <|), where < | is the restricted idempotent. It is clear that we have ordinary adjunctions a ⊣ i ⊣ c. It is also clear that i is an ord-functor, for if f ≤ g: X [figure]A in ord then if ⪯ ig in idm. Similarly, if f ⪯ g: X [figure]A in idm then cf ≤ cg in ord and it follows that we can regard i ⊣ c as an ord-adjunction.

[figure: ord; idm; i; ord; idm; c; ⊥]

But a: idm_{0} [figure]ord_{0} does not admit enrichment to an ord-functor. For example, consider the two distinct sum injections f, g : 1 [figure]2 in S. These give rise to distinct arrows f, g: (1, ∅) [figure](2, ∅) in idm, where each idempotent in question has no instances of <. We have f ⪯ g (and g ⪯ f) but we do not have af ≤ ag.

4.10. We have also the commuting diagram of forgetful functors

[figure: ^{ord^{0}}; S; |−|; ^{ord^{0}}; ^{idm^{0}}; i; ^{idm^{0}}; S; |−|]

and note that ord_{0}(1, −) = | − | : ord_{0} [figure]S, where 1 is the one-point ordered set — the terminal object of ord and the identity object for the cartesian monoidal structure. Clearly i1 is terminal in idm and we have idm(1, −) ≅ c : idm [figure]ord. By contrast, idm_{0}(N, −) = |−|: idm_{0} [figure]S, where N = (1, ∅) is ‘the naked one’. Since a: idm_{0} [figure]ord_{0} commutes with the forgetful functors, it follows that the chaotic order construction k : S [figure]ord_{0}, right adjoint to | − | : ord_{0} [figure]S, yields ik : S [figure]idm right adjoint to | − | : idm_{0} [figure]S. Penultimately, in regard to this diagram, observe that the discrete order construction d: S [figure]ord_{0} is left adjoint to | − |: ord_{0} [figure]S while n: S [figure]idm_{0}, the left adjoint to |−|: idm_{0} [figure]S is given by nS = (S, ∅). Finally, we have π_{0} ⊣ d: S [figure]ord_{0}, with π_{0}A the set of connected components of A, but there is no left adjoint for n: S [figure]idm_{0} because n does not preserve the terminal object.

4.11. In [RW4] and [MRW] the ord-functor D = krl(1, −) : krl [figure]ord was studied in detail. For X an idempotent, DX = D(X, <) is the set of downsets of (X, <) ordered by inclusion. Recall that a downset S of (X, <) is a subset S of X with the property that x ∈ S if and only if (∃y)(x < y ∈ S). Of course as with any subset, such an S has a characteristic function that takes values in Ω. Note that the inclusion ordering of subsets is that given by the pointwise-order for Ω-valued functions. For (X, <) an idempotent, the set idm_{0}(X^{op}, iΩ) can be identified with the set of those subsets T of X with the property that x < y ∈ T implies x ∈ T. Call such a T a weak downset of (X, <). (X^{op} for idempotents is just as for orders, that is X^{op} = (X, <)^{op} = (X, <^{op}), where x <^{op} y if and only if y < x.) For the record, observe that, for any idempotent X and any order A, the set idm_{0}(X, iA) admits the order f ≤ g defined by (∀x)(fx ≤ gx) but this is in general distinct from the order ⪯ of idm(X, iA). In general, f ≤ g implies f ⪯ g but not conversely. For example, for any parallel pair of the form f, g : (X, ∅) [figure](A, ≤) we have f ⪯ g, but not necessarily f ≤ g. Identifying subsets with their characteristic functions we see that idm(X^{op}, iΩ) is the set of weak downsets of X with T ⪯ U if and only x < y ∈ T implies x ∈ U.

4.12. Proposition. For any idempotent (X, <), the inclusion iDX [figure]idm(X^{op}, iΩ) is an equivalence of ordered sets.

Proof. Since a downset is a weak downset and, by our generalities about orders, R ⊆ S implies R ⪯ S; it follows that inclusion provides a functor iDX [figure]idm(X^{op}, iΩ). For T a weak downset, define T^{∘} = {x|(∃t)(x < t ∈ T)}. Then T^{∘} is certainly a downset. If T ⪯ U and x ∈ T^{∘} then x < t ∈ T implies (∃y)(x < y < t ∈ T) which implies (∃y)(x < y ∈ U) (by T ⪯ U) and hence x ∈ U^{∘}. Thus T^{∘} ⊆ U^{∘} and (−)^{∘} : idm(X^{op}, iΩ) [figure]iDX is a functor, right adjoint to the inclusion iDX [figure]idm(X^{op}, iΩ), since T^{∘} ⊆ T and hence T^{∘} ⪯ T provides a counit. For T a downset we have also T ⊆ T^{∘} so that (−)^{∘} : idm(X^{op}, iΩ) [figure]iDX is split by the inclusion. To show that we have an equivalence it suffices to show that T^{∘} ⪯ T is invertible, meaning here that T ⪯ T^{∘}, for every weak downset T. But if x < y ∈ T then, by definition, x ∈ T^{∘} which shows T ⪯ T^{∘}.

4.13. Remark. Of course we do not have T^{∘} = T for every weak downset so that the inclusion iDX [figure]idm(X^{op}, iΩ) is not an order isomorphism. Also, for A an order, weak downsets are downsets (and the order relation on idm(iA^{op}, iΩ) is containment, modulo identification of subsets with their characteristic functions). Thus our use of D for both ord(1, −) and krl(1, −) is unambiguous. We also generalize ↓ to objects of idm so that ↓_{X}: X [figure]iDX in idm is the arrow that sends x to ↓x = {x′ ∈ X | x′ < x}.

5. Power Objects and Cauchy Completions for (−)_{#} : idm→krl

5.1. We first show that the proarrow equipment (−)_{#} : idm [figure]krl has a right KZadjoint. We recall that for general f : X [figure]Y in idm, we have f^{#} : Y [figure]X in krl given by xf^{#}y if and only if (∃x′)(x < x′ and fx′ < y). It is easy to see that y ↓_{Y}^{#}S (if and only if (∃y′)(y < y′ and ↓_{Y} y′ ⊆ S)) simplifies to y ∈ S. For all M : X [figure]Y in krl, define m = m(M) : X [figure]iDY by m(x) = {y | yMx}. Since y ∈ m(x) if and only if yMx it is at once clear that each m(x) is a downset and that m: X [figure]iDY is in idm.

5.2. Lemma. For all M : X [figure]Y in krl,

[figure: iDY; Y; ↓^{#}; X; iDY; m(M)_{#}; X; Y; M]

commutes.

Proof. We have y(↓^{#}m_{#})x if and only if (∃S)(y ∈ S and Sm_{#}x) if and only if (∃S, x′)(y ∈ S ⊆ m(x′) and x′ < x) which holds if and only if yMx.

5.3. Lemma. The diagram in Lemma 5.2 exhibits m(M)_{#} as a right lifting in krl of M through ↓^{#} : iDY [figure]Y.

Proof. We recall from [RW4] that krl has all right liftings and, for any L: A [figure]Y [figure] X: M, the right lifting of M through L is given by the relational composite <_{A} .(L ⇒ M).<_{X}, where L ⇒ M is the right lifting in the bicategory rel of all relations. When A is an order it is easy to see that the description simplifies to (L ⇒ M). <_{X}. Now S((↓^{#} ⇒ M). <)x holds if and only if (∃x′)((∀y)(y ∈ S implies yMx′) and x′ < x) which is the case if and only if (∃x′)(S ⊆ m(x′) and x′ < x) which means precisely Sm_{#}x.

5.4. Proposition. The proarrow equipment (−)_{#} : krl [figure]idm has power objects, given by iD as in 4.11 with unit ↓.

Proof. As we have seen in Section 2, it suffices to show that

idm(X, iDY) [figure: ↓^{#}.(−)_{#}] krl(X, Y)

provides an equivalence of categories. Since ↓^{#}.(−)_{#} is surjective by Lemma 5.2 it suffices to show that ↓^{#}.(−)_{#} is fully faithful. So assume that we have f, g : X [figure]iDY in idm with ↓^{#}.f_{#} ⊆↓^{#}.g_{#}. We must show that f ⪯ g. For this we must show that if x′ < x then fx′ ⊆ gx. So along with x′ < x assume that we have y ∈ fx′ Since y ↓^{#}.f_{#}x translates to (∃x′)(y ∈ fx′ and x′ < x) and we are assuming ↓^{#}.f_{#} ⊆↓^{#}.g_{#} we have (∃x′′)(y ∈ gx′′ and x′′ < x) and hence y ∈ gx.

5.5. Remark. We know from our general study of power objects for proarrow equipments in Section 2, that from fully faithfulness of ↓^{#}.(−)_{#} we have the universal property for m(M) given in Lemma 2.6. For (−)_{#} ⊣ iD : krl [figure]idm we have the stronger right lifting property given by Lemma 5.3.

5.6. As shown in [RW4], there is an important idempotent relation, denoted⊂⊂ , on the set of downsets of an idempotent (Y, <), with S ⊂⊂T if and only if (∃t)(S ⊆↓t and t ∈ T). We write 𝔻Y = (|DY |,⊂⊂) for the set of downsets of (Y, <) together with⊂⊂. Since S ⊂⊂T implies S ⊆ T, the identity function provides a functor k: 𝔻Y [figure]iDY in idm. We showed in [RW4] that ↓_{Y} factors through k. We will let ↓ = ↓_{Y} serve double duty and write also ↓ = ↓_{Y} : Y [figure]𝔻Y. Observe that for this interpretation of ↓ we still have y ↓^{#}S if and only if y ∈ S. The idempotent relation ⊂⊂ on |DY | gives rise to a new idempotent relation on idm_{0}(X^{op}, iΩ). For weak downsets U and V we define U ≺≺ V to mean U^{∘} ⊂⊂ V^{∘} where (−)^{∘}: (idm_{0}(X^{op}, iΩ),≺≺) [figure]𝔻Y is as in Proposition 4.12. Note that U^{∘} ⊂⊂ V^{∘} is equivalent to saying (∃y, v)((x < u ∈ U implies x < y) and (y < v ∈ V)).

5.7. Proposition. The inclusion 𝔻Y [figure](idm_{0}(Y^{op}, iΩ),≺≺) provides an equivalence of objects in idm with inverse given by (−)^{∘} : (idm_{0}(Y^{op}, iΩ),≺≺) [figure]𝔻Y as defined in Proposition 4.12.

Proof. Assume that S ⊂⊂T in 𝔻Y. Since the inclusion of downsets in weak downsets is split by (−)^{∘} we have S^{∘} ⊂⊂T^{∘} which means S ≺≺T in weak downsets. This shows that the inclusion provides an arrow 𝔻Y [figure](idm_{0}(Y^{op}, iΩ),≺≺) in idm. If, for weak downsets U and V, U ≺≺ V then U^{∘} ⊂⊂ V^{∘} by definition so that (−)^{∘} : (idm_{0}(Y^{op}, iΩ),≺≺) [figure]𝔻Y is an arrow in idm, split by the inclusion, call it j. To show that j and (−)^{∘} constitute inverse equivalences in idm it suffices to show the inequalities

1_{(idm_{0}(Y^{op},iΩ),≺≺)} ⪯ j(−)^{∘} and j(−)^{∘} ⪯ 1_{(idm_{0}(Y^{op},iΩ),≺≺)}

For the first, assume U ≺≺V. We must show U ≺≺V^{∘}. But this just means showing that U^{∘} ⊂⊂ V^{∘} implies U^{∘} ⊂⊂ V^{∘∘}, which is trivial since (−)^{∘} is idempotent. For the second, we must show that U ≺≺V implies U^{∘} ≺≺V, which is as trivial as the first.

5.8. It follows that we can replace 𝔻Y by (idm_{0}(Y^{op}, iΩ),≺≺) in the next results. For M : X [figure]Y in krl we again use m = m(M) : X [figure]iDX in idm, with m(x) = {y | yMx}, as we did in 5.1. Recall that M ⊣ R in krl if and only if 1_{X} ⊆ RM and MR ⊆ 1_{Y}. The first of these, the unit condition, is equivalent to x < x′ in X implies (∃y)(xRyMx′) and the second, the counit condition, is equivalent to yMxRy′ implies y < y′.

5.9. Lemma. For any map M : X [figure]Y in krl, m = m(M) : X [figure]iDY factors through k: 𝔻Y [figure]iDY and

[figure: 𝔻Y; Y; ↓^{#}; X; 𝔻Y; m_{#}; X; Y; M]

commutes.

Proof. Let M ⊣ R. We have seen in Lemma 5.2 that each m(x) is a downset of X. Under the assumption that M is a map we want to show that m factors through k: 𝔻X [figure]iDX in idm. Assume that x < x′ in X. To show m(x)⊂⊂m(x′) is to show

(∃y′)(m(x) ⊆ ↓y′ and y′ ∈ m(x′))

which is to show

(∃y′)((yMx implies y < y′) and y′Mx′)

From the unit condition for M ⊣ R we have (∃y′)(xRy′Mx′). So if yMx then xRy′ gives y < y′, using the counit condition for M ⊣ R, and this together with y′Mx′ shows that y′ witnesses m(x) ⊂⊂ m(x′). Now y(↓^{#}m_{#})x if and only if (∃S)(y ↓^{#}Sm_{#}x) which is equivalent to

(∃S)(y ∈ S and (∃x′)(S ⊂⊂m(x′) and x′ < x))

which holds if and only if

(∃S)(y ∈ S and (∃x′)((∃y′)(S ⊆ ↓y′ and y′ ∈ m(x′)) and x′ < x))

which holds if and only if

(∃y′, x′)(y < y′ and y′Mx′ and x′ < x)

which is yMx.

5.10. Lemma. For any map M : X [figure]Y in krl, the diagram in Lemma 5.9 exhibits m_{#} as a right lifting in krl of M though ↓^{#} : 𝔻Y [figure]Y.

Proof. Here S(⊂⊂ .(↓^{#} ⇒ M). <_{X})x holds if and only if (∃T, x′)(S ⊂⊂ T and (∀y)(y ∈ T implies yMx′) and x′ < x) if and only if (∃T, x′)(S ⊂⊂ T ⊆ m(x′)) and x′ < x) if and only if (∃x′)(S ⊂⊂m(x′) and x′ < x) which here means Sm_{#}x.

5.11. Proposition. The proarrow equipment (−)_{#} : krl [figure]idm has Cauchy completions, given by 𝔻 as in 5.6 with unit ↓: 1_{idm} [figure]𝔻(−)_{∗}.

Proof. It suffices to show that

idm(X, 𝔻Y) [figure: ↓^{#}.(−)_{#}] mapkrl(X, Y)

provides an equivalence of categories and that the counit

[figure: Y; 𝔻Y; ↓_{#}; 𝔻Y; Y; ↓^{#}; 𝔻Y; 𝔻Y; 1; ⊆]

is an isomorphism in krl. It is convenient to deal first with the latter, by noting that it is part of Proposition 11 in [RW4] — which says that ↓_{#} and ↓^{#} are inverse isomorphisms in krl. In particular, ↓^{#} is also a map in krl. For the first requirement, since ↓^{#}.(−)_{#} is surjective by Lemma 5.9, it suffices to show that ↓^{#}.(−)_{#} is fully faithful. So assume that we have f, g: X [figure]𝔻Y in idm with ↓^{#}.f_{#} ⊆↓^{#}.g_{#}. We must show that f ⪯ g. Since ↓^{#} is a map, ↓^{#}.g_{#} is a map whose right lifting through ↓^{#} is easily seen to be g_{#}. It follows that f_{#} ⊆ g_{#} and hence f ⪯ g since (−)_{#} is locally fully faithful.

5.12. Remark. From Corollary 3.7 it follows that any object of the form iDY is Cauchy complete. Note too that, for B an order, we have DiB = DB where the second D is the power object construction for ord.

5.13. We will also need to know that Cauchy completeness is preserved by application of (−)^{op}. While this topic can also be treated for general proarrow equipments that admit a duality, we content ourselves here with the specific case of (−)_{#} : krl [figure]idm. For Y = (Y, <) in idm we define UY = krl(Y, 1)^{op}. It is easy to see that UY = D(Y^{op})^{op} (where we recall (Y, <)^{op} = (Y, < ^{op})) and that for T ∈ UY we have

t ∈ T iff (∃t′)(T ∋ t′ < t)

We refer to the elements of UY as upsets of Y. We also write ↑ = ↑_{Y} = (↓_{Y} ^{op})^{op}, so that ↑y = {y′ | y < y′}. We define 𝕌Y = (𝔻Y^{op})^{op} and write ⊃⊃ for the dual of ⊂⊂ for DY^{op}. Thus 𝕌Y = (|UY |,⊃⊃) where T′ ⊃⊃T if and only if (∃t′)(T′ ∋ t′ and ↑t′ ⊇ T). We define (−)_{Y}^{+} : DY [figure]UY by

S^{+} = {u | (∃v)(S ⊆ ↓v and v < u} = {u | S ⊂⊂↓u}

and (−)_{Y}^{−}: UY [figure]DY by

T^{−} = {l | ↑l ⊃⊃T }

5.14. Lemma. In idm

[figure: Y; iUY; ↑_{Y}; iDY; Y; ↓_{Y}; iDY; iUY; i(−)_{Y}^{+}; iUY; iDY; i(−)^{−}; ⊣; ≅]

meaning that both triangles commute to within isomorphism and we have the displayed adjunction (in idm).

Proof. The proof is routine but some care needs to be exercised in applying the definitions pertaining to idm. Thus, for example, to show i(−)_{Y}^{+}. ↓_{Y} ≅ ↑_{Y} we must show that if y_{1} < y_{2} then both (↓y_{1})^{+} ⊇ ↑y_{2} and ↑y_{1} ⊇ (↓y_{2})^{+}. The details are left to the reader.

5.15. Lemma. The functions (−)_{Y}^{+} and (−)_{Y}^{−} also provide arrows (−)_{Y}^{+} : 𝔻Y [figure]𝕌Y and (−)_{Y}^{−}: 𝕌Y [figure]𝔻Y in idm which are inverse equivalences and in

[figure: Y; 𝕌Y; ↑; 𝔻Y; Y; ↓; 𝔻Y; 𝕌Y; (−)^{+}; 𝕌Y; 𝔻Y; (−)^{−}; ≃; ≅]

both triangles commute to within isomorphism.

Proof. To see that (−)^{+} defines an arrow (−)^{+} : 𝔻Y [figure]𝕌Y, suppose that, for downsets S and S′, we have S ⊂⊂S′. We can assume this to be witnessed by S ⊂⊂↓s′ with s′ ∈ S′ (for the asumption that S ⊆ ↓s′′ with s′′ ∈ S′ immediately gives us s′′ < s′ ∈ S′). It follows that we have S^{+} ⊃⊃ S^{′+} witnessed by S^{+} ∋ s′ and ↑s′ ⊇ S^{′+}. The first conjunct is clear and for the second, if we have u ∈ S^{′+} then we have s′ ∈ S′ ⊂⊂↓u giving s′ < u, which can be read as ↑s′ ∋ u. The case of (−)^{−} is similar.

To show that (−)_{Y}^{+} : 𝔻Y [figure]𝕌Y and (−)_{Y}^{−}: 𝕌Y [figure]𝔻Y are inverse equivalences consider first the task of showing that 1_{𝔻Y} ≅ (−)^{+−}. We assume that R ⊂⊂ S in 𝔻X and show that both R ⊂⊂ S^{+−} and R^{+−} ⊂⊂ S. If we have R ⊂⊂↓s with s ∈ S then R ⊂⊂ S^{+−} is also witnessed by s since we have S ⊆ S^{+−} (the unit of the adjunction in Lemma 5.14). To show that R^{+−} ⊂⊂ S it suffices to show that R^{+−} ⊆ ↓s. If l ∈ R^{+−} then we have ↑l ⊃⊃ {u | R ⊂⊂↓u} ∋ s which gives ↑l ∋ s and hence l < s. The calculation to show 1_{𝕌Y} ≅ (−)^{−+} is dual.

Finally, we show (−)^{+}. ↓ ≅ ↑ in idm and leave (−)^{−}. ↑ ≅ ↓ for the reader. Assume y_{1} < y_{2} in Y. We will show (↓y_{1})^{+} ⊃⊃ ↑y_{2} and ↑y_{1} ⊃⊃ (↓y_{2})^{+}. From y_{1} < y_{2} there exists y such that y_{1} < y < y_{2} from which we have ↓y_{1} ⊂⊂↓y and also ↑y ⊇ ↑y_{2}. From these we see that y witnesses (↓y_{1})^{+} ⊃⊃↑y_{2}. The same y also witnesses ↑y_{1} ⊃⊃ (↓y_{2})^{+}.

5.16. Proposition. If Y = (Y, <) is Cauchy complete then Y^{op} is Cauchy complete.

Proof. Since ↓_{Y} : Y [figure]𝔻Y has a pseudo section and (−)_{Y}^{+} : 𝔻Y [figure]𝕌Y is an equivalence by Lemma 5.15, (−)_{Y}^{+}. ↓_{Y} : Y [figure]𝕌Y has a pseudo section. Thus its isomorph ↑_{Y} : Y [figure]𝕌Y, also using Lemma 5.15, has a pseudo section so that (↑_{Y})^{op} : Y^{op} [figure](𝕌Y)^{op} has a pseudo section. But this last is ↓_{Y^{op}} : Y^{op} [figure]𝔻Y^{op} showing that Y^{op} is Cauchy complete.

5.17. Remark. We remark that the display in Lemma 5.14 shows that we have what is called the “Isbell conjugation” adjunction in the context of enriched category theory. In [K&S] it is shown, for enriched categories, that the Isbell conjugation adjunction restricted from power objects to Cauchy completions gives an equivalence and hence the self dual property for Cauchy completeness.

6. The Main Results

6.1. Proposition. The ord-functors

[figure: ord; ^{idm^{op}}; iord(−,Ω); ord; ^{idm^{op}}; idm(−,iΩ); ⊣]

are biadjoint in the sense indicated and give rise to an ord-monad idm(iord(−, Ω), iΩ) on ord whose ord-category of algebras is ccd, the ord category of CCD lattices and functors having both right and left adjoints.

Proof. To establish the biadjunction we must show that, for all X in idm and A in ord, we have a pseudonatural equivalence of categories (here ordered sets)

idm(X, iord(A, Ω)) ≃ ord(A, idm(X, iΩ))

For (X, <) an idempotent, there is an equivalence idm(X, iΩ) ≃^{(vii)} DX^{op} by Proposi-

tion 4.12 and, for (A, ≤) an order, the isomorphism ord(A, Ω) ≅^{(i)} DA^{op} is standard, as reviewed in 4.2. In Remark 5.12 we disambiguated the use of D in both ord and idm power object contexts with the equation DiB =^{(ii)} DB. In the string of pseudonatural equivalences below, we have also explicitly used Proposition 5.4 that iD is right biadjoint to (−)_{#} in (iii) and in (v), while (iv) arises from the fact that (−)^{op} : krl^{op} [figure]krl is an involutory isomorphism. Finally, we have (vi) because i: ord [figure]idm is fully faithful. (In anticipation of possible future developments we note that pseudo fully faithfulness of i would have sufficed.)

idm(X, iord(A, Ω)) ≅^{(i)} idm(X, iDA^{op})
=^{(ii)} idm(X, iDiA^{op})
≃^{(iii)} krl(X, iA^{op})
≅^{(iv)} krl(iA, X^{op})
≃^{(v)} idm(iA, iDX^{op})
≅^{(vi)} ord(A, DX^{op})
≃^{(vii)} ord(A, idm(X, iΩ))

The involutory isomorphism (−)^{op} mentioned above for krl leads to an involutory isomorphism (−)^{op} : idm^{co} [figure]idm (just as taking opposites has variance ‘co’ for categories and functors). If the now established biadjunction of the statement is composed with

idm^{coop} [figure: (−)^{op}; (−)^{op}] idm^{op}

seen as a trivial biadjunction, then the composite monad is unchaged (because (−)^{op} is involutory) but in this form it is immediately recognizable as the composite monad DU : ord [figure]ord arising from the distributive law UD [figure]DU of the upset monad over the downset monad (both on ord) studied in [MRW]. The 2-category of algebras for DU was shown in [MRW] to be ccd.

6.2. Theorem. The ord-functors

[figure: ord; ^{idm^{cc}^{op}}; iord(−,Ω); ord; ^{idm^{cc}^{op}}; idm_{cc}(−,iΩ); ⊣]

are biadjoint in the sense indicated, idm_{cc}(−, iΩ) : idm^{op} [figure]ord is bimonadic and the ord-category of algebras is ccd.

Proof. To establish this biadjunction we refer to that of Proposition 6.1 and first note that the left biadjoint applied to an order A produces an isomorph of iDA^{op} and we have seen in 5.12 that idempotents of the form iDB are Cauchy complete so that it factors through idm_{cc}^{op}. On the other hand, Ω = D1 so that 5.12 also shows that iΩ is Cauchy complete. It follows that the restriction of the right biadjoint of Proposition 6.1 to idm_{cc}^{op} is idm_{cc}(−, iΩ). Now with X an arbitrary Cauchy complete idempotent we have the following string of pseudonatural equivalences adapted from those in the proof of Proposition 6.1

idm_{cc}(X, iord(A, Ω)) ≅^{(a)} idm_{cc}(X, iDA^{op})
=^{(b)} idm_{cc}(X, iDiA^{op})
≃^{(c)} krl(X, iA^{op})
≅ krl(iA, X^{op})
≃ idm(iA, iDX^{op})
≅ ord(A, DX^{op})
≃^{(d)} ord(A, idm_{cc}(X, iΩ))

Their justifications are as before except that at (a), (b), (c), and (d) we need also to note that idm_{cc} is the full sub-ord-category of idm determined by the Cauchy complete objects. There is the trivial biadjunction

idm_{cc}^{coop} [figure: (−)^{op}; (−)^{op}] idm_{cc}^{op}

because we have seen in Proposition 5.16 that the dual of a Cauchy complete idempotent is Cauchy complete. If this biadjunction is composed with that in the statement it is clear that the biadjunction of the statement gives rise to the ord-monad DU on ord whose ord-category of algebras was shown in [MRW] to be ccd. The comparison ord-functor idm_{cc}^{op} [figure]ccd is evidently equivalent to D(−)^{op} : idm_{cc}^{op} [figure]ccd by Proposition 4.12. The latter can seen as the composite

idm_{cc}^{op} [figure: (−)^{op}] idm_{cc}^{coop} [figure] mapkrl^{coop} [figure: mapD^{coop}] mapccd_{sup}^{coop} = ccd

where ccd_{sup} is the ord-category of CCD lattices and functors having a right adjoint. The first displayed arrow is an isomorphism. The second is an instance of the formal biequivalence given in subsection 3.8 since (−)_{#} : idm [figure]krl has Cauchy completions. The third is obtained from the biequivalence D : krl [figure]ccd_{sup} of Theorem 17 in [RW4] by application of map(−)^{coop}. It follows that idm_{cc}^{op} [figure]ccd is a biequivalence so that idm_{cc}(−, iΩ) : idm_{cc}^{op} [figure]ord is bimonadic.

22  FRANCISCO MARMOLEJO, ROBERT ROSEBRUGH, AND R.J. WOOD

References

[C&S] A. Carboni and R. Street. Order ideals in categories. Pacific J. Math., 124 (1986), No.

2, 275–288.

[CMW] G. S. H. Cruttwell, F. Marmolejo and R.J. Wood. CCD lattices in presheaf categories. Theory Appl. Categ. 18 (2007), No. 6, 157–171.

[F&W] B. Fawcett and R.J. Wood. Constructive complete distributivity I. Math. Proc. Cam-

bridge Philos. Soc. 107 (1990), No. 1, 81–89.

[K&S] G.M. Kelly and V. Schmitt. Notes on enriched categories with colimits of some class.

Theory Appl. Categ. 14 (2005), No.17, 399–423.

[KOS] J. Koslowski. Monads and interpolads in bicategories. Theory Appl. Categ. 3 (1997), No. 8, 182–212.

[LAW] F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Rend. Sem. Mat. Fis. Milano 43 (1973), 135–166.

[S&W] I. Lopez-Franco, R. Street and R.J. Wood Duals Invert. to appear, 2009.

[MAC] S. Mac Lane. Categories for the working mathematician. Second edition. Graduate Texts in Mathematics 5. Springer-Verlag, New York, 1998.

[M&W] F. Marmolejo and R.J. Wood KZ-Adjunctions. Unpublished Notes, 2004.

[MAR] F. Marmolejo. Doctrines whose structure forms a fully faithful adjoint string. Theory Appl. Categ. 3 (1997), No. 2, 24–44.

[MRW] F. Marmolejo, R. Rosebrugh, and R.J. Wood. A basic distributive law. J. Pure Appl. Algebra 168 (2002), No. 2-3, 209–226.

[PAR] R. Paré. Colimits in topoi. Bull. Amer. Math. Soc. 80 (1974), 556–561.. [P&W] M.C. Pedicchio and R.J. Wood. Groupoidal completely distributive lattices. Special

volume on the occasion of the 60th birthday of Professor Michael Barr (Montreal, QC, 1997). J. Pure Appl. Algebra 143 (1999), No. 1-3, 339–350.

[RW2] R. Rosebrugh and R.J. Wood. Constructive complete distributivity II. Math. Proc. Cambridge Philos. Soc. 110 (1991), No. 2, 245–249.

[RW3] R. Rosebrugh and R.J. Wood. Constructive complete distributivity III. Canad. Math. Bull. 35 (1992), No. 4, 537–547.

[RW4] R. Rosebrugh and R.J. Wood. Constructive complete distributivity IV. Appl. Categ. Structures 2 (1994), No. 2, 119–144.

[RWb] R. Rosebrugh and R.J. Wood. Boundedness and complete distributivity. Appl. Categ. Structures 9 (2001), No. 5, 437–456.

[RWp] R. Rosebrugh and R.J. Wood. Proarrows and cofibrations. J. Pure Appl. Algebra 53 (1988), No. 3, 271–296.

[RWc] R. Rosebrugh and R.J. Wood. Cofibrations II. Left exact right actions and composition of gamuts. J. Pure Appl. Algebra 39 (1986), No. 3, 283–300.

[Wd1] R.J. Wood. Abstract proarrows I. Cahiers Topologie Géom. Différentielle 23 (1982), No. 3, 279–290.

[Wd2] R.J. Wood. Proarrows II. Cahiers Topologie Géom. Différentielle Catég. 26 (1985), No. 2, 135–168.

Instituto de Matemáticas Area de la Investigación Científica Circuito Exterior Ciudad Universitaria México D.F. 04510 México Department of Mathematics Mount Allison University Sackville, NB, E0A 3C0, Canada Department of Mathematics and Statistics Dalhousie University Halifax, NS, B3H 3J5, Canada

Email: quico@matem.unam.mx
      rrosebrugh@mta.ca
      rjwood@dal.ca

This article may be accessed at http://www.tac.mta.ca/tac/ or by anonymous ftp at

ftp://ftp.tac.mta.ca/pub/tac/html/volumes/22/1/22-01.{dvi,ps,pdf}

THEORY AND APPLICATIONS OF CATEGORIES (ISSN 1201-561X) will disseminate articles that significantly advance the study of categorical algebra or methods, or that make significant new contributions to mathematical science using categorical methods. The scope of the journal includes: all areas of pure category theory, including higher dimensional categories; applications of category theory to algebra, geometry and topology and other areas of mathematics; applications of category theory to computer science, physics and other mathematical sciences; contributions to scientific knowledge that make use of categorical methods. Articles appearing in the journal have been carefully and critically refereed under the responsibility of members of the Editorial Board. Only papers judged to be both significant and excellent are accepted for publication. Full text of the journal is freely available in .dvi, Postscript and PDF from the journal’s server at http://www.tac.mta.ca/tac/ and by ftp. It is archived electronically and in printed paper format.

Subscription information. Individual subscribers receive abstracts of articles by e-mail as they are published. To subscribe, send e-mail to tac@mta.ca including a full name and postal address. For institutional subscription, send enquiries to the Managing Editor, Robert Rosebrugh, rrosebrugh@mta.ca.

Information for authors. The typesetting language of the journal is TEX, and L^{A}TEX2e strongly encouraged. Articles should be submitted by e-mail directly to a Transmitting Editor. Please obtain detailed information on submission format and style files at http://www.tac.mta.ca/tac/.

Managing editor. Robert Rosebrugh, Mount Allison University: rrosebrugh@mta.ca

TEXnical editor. Michael Barr, McGill University: barr@math.mcgill.ca

Assistant TEX editor. Gavin Seal, McGill University: gavin seal@fastmail.fm

Transmitting editors.

Richard Blute, Université d’ Ottawa: rblute@uottawa.ca Lawrence Breen, Université de Paris 13: breen@math.univ-paris13.fr Ronald Brown, University of North Wales: ronnie.profbrown (at) btinternet.com Aurelio Carboni, Università dell Insubria: aurelio.carboni@uninsubria.it Valeria de Paiva, Cuill Inc.: valeria@cuill.com Ezra Getzler, Northwestern University: getzler(at)northwestern(dot)edu Martin Hyland, University of Cambridge: M.Hyland@dpmms.cam.ac.uk P. T. Johnstone, University of Cambridge: ptj@dpmms.cam.ac.uk Anders Kock, University of Aarhus: kock@imf.au.dk Stephen Lack, University of Western Sydney: s.lack@uws.edu.au F. William Lawvere, State University of New York at Buffalo: wlawvere@acsu.buffalo.edu Jean-Louis Loday, Université de Strasbourg: loday@math.u-strasbg.fr Ieke Moerdijk, University of Utrecht: moerdijk@math.uu.nl Susan Niefield, Union College: niefiels@union.edu Robert Paré, Dalhousie University: pare@mathstat.dal.ca Jiri Rosicky, Masaryk University: rosicky@math.muni.cz Brooke Shipley, University of Illinois at Chicago: bshipley@math.uic.edu James Stasheff, University of North Carolina: jds@math.unc.edu Ross Street, Macquarie University: street@math.mq.edu.au Walter Tholen, York University: tholen@mathstat.yorku.ca Myles Tierney, Rutgers University: tierney@math.rutgers.edu Robert F. C. Walters, University of Insubria: robert.walters@uninsubria.it R. J. Wood, Dalhousie University: rjwood@mathstat.dal.ca