Theory and Applications of Categories, Vol. 24, No. 11, 2010, pp. 266–287.

TENSOR PRODUCTS OF SUP-LATTICES AND GENERALIZED SUP-ARROWS

T. KENNEY AND R.J. WOOD

Abstract. An alternative description of the tensor product of sup-lattices is given with yet another description provided for the tensor product in the special case of CCD sup-lattices. In the course of developing the latter, properties of sup-preserving functions and the totally below relation are generalized to not-necessarily-complete ordered sets.

1. Introduction

We write sup for the category of complete lattices and sup-preserving functions and speak of its objects as sup-lattices. When sup is considered as a category over set, the category of sets, by the obvious forgetful functor, bi-sup-preserving functions make sense. Given sup-lattices M, N, and L, a function ϕ: M × N [figure]L is bi-sup-preserving if it preserves suprema in each variable separately. Every sup-preserving ϕ : M × N [figure]L is bi-sup-preserving (unlike the corresponding situation for abelian groups) but the converse is not true. If ϕ : M × N [figure]L is bi-sup-preserving and l : L [figure]L′ is sup-preserving, then the composite lϕ: M×N [figure]L′ is bi-sup-preserving. The tensor product M⊗N for sup-lattices M and N is the codomain for a universal bi-sup-preserving function ι: M × N [figure]M ⊗ N, composition with which provides a natural bijection between sup-preserving functions f : M ⊗ N [figure]L and bi-sup-preserving functions ϕ: M × N [figure]L, as in:

[figure: M × N; M ⊗ N; ι; M × N; L; ϕ; M ⊗ N; L; f]

TENSOR PRODUCTS OF SUP-LATTICES AND GENERALIZED SUP-ARROWS 267

It is now classical that M ⊗ N can be constructed as the quotient of the free sup-lattice on M × N, obtained from the smallest congruence ≡ with (⋁_{i} m_{i}, n) ≡ ⋁_{i}(m_{i}, n) and (m, ⋁_{i} n_{i}) ≡ ⋁_{i}(m, n_{i}). The free functor 𝒫 : set [figure]sup is given by the power set and direct images. For our purposes, the best references for this approach are [J&T] and [PIT], but the story is much older than even the first of those papers.

The first author did part of this work while an AARMS-funded postdoctoral fellow at Dalhousie University, and part of this work while a postdoctoral researcher at Univerzita Mateja Bela. The second author gratefully acknowledges financial support from the Canadian NSERC. Diagrams typeset using M.

Barr’s diagram package, diagxy.tex.

Received by the editors 2010-02-06 and, in revised form, 2010-05-26.

Transmitted by Susan Niefield. Published on 2010-05-31.

2000 Mathematics Subject Classification: 18A25.

Key words and phrases: adjunction, tensor product, totally below, CCD, idempotent.

\begin{matrix}c \\ ◯ \end{matrix} T. Kenney and R.J. Wood, 2010. Permission to copy for private use granted.

The quotient 𝒫(M × N) [figure]M ⊗ N, being an arrow in sup, has a right adjoint in ord, the 2-category of ordered sets, so that in ord, M ⊗ N is a full reflective subobject of 𝒫(M × N). It should be, and is, easier to give an explicit description of M ⊗ N as a full reflective subobject, and this is our purpose in Section 3. We find it convenient to regard sup as a 2-category over ord. The 2-functor sup [figure]ord has a left 2-adjoint, and bi-sup-preserving functions are automatically in ord so that we could simply lift the classical approach to ord. However, the 2-dimensional structure of ord allows us to exploit the calculus of adjoints within ord, and this simplifies the description of the tensor product considerably. We first arrive at our description of the tensor product using some of its known properties, but we also show that our description allows a direct verification of the defining universal property.

In Section 4, we study sup-preserving functions in terms of upper and lower bounds, arriving quickly at a definition of sup-preserving function that makes sense in the absence of suprema (and infima). We study the sup-completion of an ordered set in the category of sup-preserving functions. We build on this work in Section 5, to describe and study the totally below relation for orders with no completeness properties. We isolate a property of ordered sets, which we call STB, that captures the essence of completely distributive (CCD) lattices, in the sense that a sup-lattice is CCD if and only if its underlying ordered set is STB. More remarkably, we show, in Theorem 5.9, that an ordered set is STB if and only if its sup-preserving sup-completion is CCD.

In Section 6 we apply our study of the totally below relation to give a very simple description of the tensor product of sup-lattices in the case that they are CCD sup-lattices. Section 2 sets some notation and recalls a few of the tools that we need.

2. Preliminaries

2.1. It is convenient to take an object (X, ≤) of ord to be a set X together with a reflexive, transitive relation ≤. From our perspective, antisymmetry is an unnecessary and unnatural requirement. If we have x ≤ y and y ≤ x in X, then x and y are isomorphic elements and we could write x ≅ y. But since x ≅ y looks both pedantic and irritating, we will usually write x = y in this case and treat it as an abuse of notation.

The arrows of ord are order-preserving functions, which we freely call functors. Given our interests here, we note that a bi-sup-preserving function ϕ: M × N [figure]L is necessarily a functor. For, if (m, n) ≤ (m′, n′) then

ϕ(m, n) ≤ ϕ(m, n) ∨ ϕ(m, n′) ∨ ϕ(m′, n) ∨ ϕ(m′, n′) = ϕ(m ∨ m′, n ∨ n′) = ϕ(m′, n′)

The 2-cells of ord are (pointwise) inequalities of functors.

2.2. The free sup-lattice on (X, ≤) is D(X, ≤), the set of subsets S of X for which x ≤ y ∈ S implies x ∈ S, ordered by inclusion. We call the elements of DX, downsets of (X, ≤). For a functor f : X [figure]A and a downset S ∈ DX, we have

Df(S) = {a ∈ A | (∃x)(a ≤ fx & x ∈ S)}

For all f, Df has a right adjoint 𝒟f : DA [figure]DX given by inverse image. In turn, 𝒟f has a right adjoint Df : DX [figure]DA given by:

Df(S) = {a ∈ A | (∀x)(fx ≤ a ⟹ x ∈ S)}

Thus for any f : X [figure]A we have Df ⊣ 𝒟f ⊣ Df : DX [figure]DA.

All functors in ord are faithful, so if f is full then Df ⊆ Df follows from general adjunction calculations. However, it is easy to argue directly with the quantifiers. Suppose that a ≤ fx_{0} and x_{0} ∈ S. Then for any x, if fx ≤ a then fx ≤ fx_{0}, which gives x ≤ x_{0} ∈ S by fullness, and x ∈ S because S is a downset.

The inverter of an inequality f ≤ g : X [figure]A in ord is just the full suborder of X determined by the set {x ∈ X | g(x) ≤ f(x)}. In particular:

2.3. Proposition. If f : X [figure]A and Df ⊆ Df then the inverter is

{Y ∈ DX | Df(Y) ⊆ Df(Y)} = {Y ∈ DX | (∀B ∈ DA)(𝒟f(B) ⊆ Y ⟹ B ⊆ Df(Y))}

We remark that the implication in the equation of the proposition can be replaced by “if and only if” because the other implication holds automatically.

2.4. The unit for the 2-adjunction D ⊣ | − | : sup [figure]ord is the full (and faithful) downsegment functor ↓_{X} : X [figure]|DX| in ord, where ↓_{X}(x) = {y ∈ X | y ≤ x}. Writing D also for the resulting 2-monad on ord, we recall that it has the KZ-property which, as characterized in [MAR], means that its multiplication components ⋃_{X} : DDX [figure]DX satisfy D ↓_{X} ⊣ ⋃_{X} ⊣ ↓_{DX}. We can verify this condition using subsection 2.2, for we have

(D ↓_{X})(S) = {T ∈ DX | (∀x)(↓_{X}(x) ⊆ T ⟹ x ∈ S)} = {T ∈ DX | T ⊆ S} = ↓_{DX}(S)

Since suprema for DX are given by union, we have ⋃_{X} ⊣ ↓_{DX}. Thus the equality D ↓_{X} = ↓_{DX} just established (a special case of a key result in [S&W]) shows that ⋃_{X} = 𝒟 ↓_{X} ⊣ D ↓_{X} and hence D ↓_{X} ⊣ ⋃_{X}. It is convenient to record here that

(D ↓_{X})(S) = {T ∈ DX|(∃x)(T ⊆ ↓_{X} x & x ∈ S)} = {T ∈ DX|(∃x)(T ⊆ ↓_{X} x ⊆ S)}

2.5. Because sup is the 2-category of algebras ord^{D} for the KZ-monad, it follows that, for each sup-lattice M, we have a reflexive coinverter diagram in sup.

[figure: DM; DDM; D⋁; DM; DDM; _{⋃_{M}}; DM; M; ⋁]

Reflexivity is provided by D ↓_{M} : DM [figure]DDM, and we note D⋁ ⊣ D ↓_{M} ⊣ ⋃_{M}. Moreover, the coinverter is | − |-contractible with data provided by the right adjoints in the adjunctions ⋁ ⊣ ↓_{M} : M [figure]DM and ⋃_{M} ⊣ ↓_{DM} : DM [figure]DDM.

3. Tensor Products of Sup-Lattices

3.1. We know that the tensor product of sup-lattices has a right adjoint in each variable separately, so that, for general reasons, a tensor product of reflexive coinverters is a reflexive coinverter. Thus for sup-lattices M and N, we have M ⊗ N the coinverter of

[figure: DM ⊗ DN; DDM ⊗ DDN; D⋁⊗D⋁; DM ⊗ DN; DDM ⊗ DDN; ⋃_{M} ⊗⋃_{N}]

However, the tensor product of free lattices simplifies:

3.2. Lemma. For X and Y in ord, DX ⊗ DY [figure: ≃] D(X × Y) in sup where the isomorphism corresponds to the bi-sup-preserving functor γ : DX × DY [figure]D(X × Y), the downset comparison functor for the left exact functor Γ = − × −: set × set [figure]set, as defined and studied in [RW1].

Proof. (Sketch) In general, γ_{X}: ΓDX [figure]DΓX corresponds to the order ideal ΓDX [figure] ΓX obtained by applying Γ to the order ideal ↓_{X}^{+} : DX [figure] X, arising from ↓ : X [figure]DX. In the case at hand, γ(S, T) = S × T. We establish the isomorphism by a Gentzen-Lawvere proof tree. We follow Kelly’s notation (see [KEL]) in using sup_{0}(−, −) for the ord hom for sup and sup(−, −) for the sup-enriched hom. So sup_{0}(L, L′) = |sup(L, L′)|. For L in sup and Y in ord, we write L^{Y} for the cotensor in the sense of enriched category theory and |L|^{Y} for the exponential in ord. Thus |L^{Y} | ≅ |L|^{Y}.

D(X × Y) [figure]L in sup
X × Y [figure]|L| in ord
X [figure]|L|^{Y} in ord
X [figure]|L^{Y} | in ord
DX [figure]L^{Y} in sup
Y [figure]sup_{0}(DX, L) in ord
Y [figure]|sup(DX, L)| in ord
DY [figure](sup(DX, L)) in sup
DX × DY [figure]L bi-sup-preserving

Taking L = D(X × Y) and starting with the identity, we leave the reader the task of showing that the last line results in γ: DX × DY [figure]D(X × Y) : (S, T)| [figure] S × T.

We recall from [RW1] that γ.Γ ↓_{X} = ↓_{ΓX}, so ↓ x × ↓ y = γ(↓ x, ↓ y) = ↓(x, y).

The next, well-known lemma recalls that coinverters in sup are calculated easily via inverters in ord.

3.3. Lemma. For

[figure: X; A; f; X; A; g]

in sup (where we use double-shafted arrows for instances of inequality) with f ⊣ ϕ and g ⊣ γ in ord, and

[figure: X; A; ϕ; X; A; γ; I; X; κ]

an inverter in ord, the full (and faithful) κ has a left adjoint k: X [figure]I which provides a coinverter for g [figure]f. Moreover, if h : X [figure]J in sup coinverts g [figure]f, then the unique l : I [figure]J satisfying ℓk = h is given by ℓ = hκ.

3.4. Note that the inverter of D ↓_{X} ⊆ D ↓_{X} is

{Y ∈ DX|(∃x)(Y = ↓_{X} x)}

which, as shown in [RW2], is the Cauchy completion of X. (It is also the antisymmetrization of X.)

3.5. Theorem. The tensor product of sup-lattices M and N can be calculated as the inverter

[figure: M ⊗ N; D(M × N); κ; D(M × N); D(DM × DN); D(↓_{M} × ↓_{N}); D(M × N); D(DM × DN); D(↓_{M} × ↓_{N})]

Explicitly

M ⊗ N = {W ∈ D(M × N)|(∀(S, T) ∈ DM × DN)(S × T ⊆ W ⟹ (⋁S, ⋁T) ∈ W)}

and this subset of D(M × N) is reflective with the reflector providing the coinverter of the diagram in 3.1.

Proof. The first and last parts of the statement follow from using Lemma 3.3 to calculate the coinverter of the the diagram in 3.1, after rewriting the domain of the 2-cell using Lemma 3.2. Since the domain of the relevant 2-cell in 3.1 is the right adjoint of the right adjoint of the codomain, the codomain of the inverter 2-cell must be the right adjoint of the right adjoint of D(↓_{M} × ↓_{N}), which by subsection 2.2 is D(↓_{M} × ↓_{N}).

For the explicit description: using 2.2 we have

D(↓_{M} × ↓_{N})(U) = {(S, T) ∈ DM × DN | (∃(m, n))((S ⊆ ↓ m & T ⊆ ↓ n) & (m, n) ∈ U)}

and

D(↓_{M} × ↓_{N})(U) = {(S, T) ∈ DM × DN | (∀(m, n))((↓ m ⊆ S & ↓ n ⊆ T) ⟹ (m, n) ∈ U)}

= {(S, T) ∈ DM × DN | S × T ⊆ U}

From these descriptions, we see that M ⊗N, calculated in ord, is the subset of D(M ×N) consisting of those W satisfying

(∀(S, T) ∈ DM × DN)(S × T ⊆ W ⟹ (∃(m, n))(S ⊆ ↓ m & T ⊆ ↓ n & (m, n) ∈ W))

Because M and N are sup-lattices, we can replace S ⊆ ↓ m with ⋁ S ≤ m and T ⊆ ↓ n with ⋁ T ≤ n and the condition above simplifies to

(∀(S, T) ∈ DM × DN)(S × T ⊆ W ⟹ (⋁S, ⋁T) ∈ W)

3.6. We will write (−)^{∨∨} for the left adjoint to the inclusion κ: M ⊗ N [figure]D(M × N). Of course, infima in M ⊗ N are given by intersection, as in D(M × N), while for any 𝒮 in D(M ⊗ N), we have ⋁𝒮 = (⋃ 𝒮)^{∨∨}.

For any W ∈ M ⊗ N, the special rectangles M × ∅ = ∅ and ∅ × N = ∅ are contained in W so that we have (⊤_{M}, ⊥_{N}) ∈ W and (⊥_{M}, ⊤_{N}) ∈ W. Since W is a downset, the axis wedge M × {⊥_{N}} ∪ {⊥_{M}} × N is contained in W. Moreover, at least using Boolean logic, it is clear that M × {⊥_{N}} ∪ {⊥_{M}} × N ∈ M ⊗ N, so that the bottom element of M ⊗ N is ⊥_{M⊗N} = M × {⊥_{N}} ∪ {⊥_{M}} × N.

Any downset is the union of the principal downsegments determined by its elements. Thus for any W in D(M × N), we have W = ⋃{↓(m, n)|(m, n) ∈ W }. For any W in M ⊗ N, we have

W = W^{∨∨} = (⋃{↓(m, n)|(m, n) ∈ W })^{∨∨} = ⋁{(↓(m, n))^{∨∨}|(m, n) ∈ W }  (1)

Define ι: M × N [figure]M ⊗ N by ι(m, n) = (↓(m, n))^{∨∨}. At least using Boolean logic, it is easy to see that

(↓(m, n))^{∨∨} = ⊥_{M⊗N} ∪ ↓(m, n) = M × {⊥_{N}} ∪ ↓(m, n) ∪ {⊥_{M}} × N

It is suggestive to write m ⊗ n for ι(m, n) = (↓(m, n))^{∨∨}, so W = ⋁{m ⊗ n|(m, n) ∈ W }, for any W ∈ M ⊗ N.

From Equation (1) it follows that, for any sup-preserving f, g: M ⊗ N [figure]L, fι = gι implies f = g. In fact, for any sup-preserving f such that fι = ϕ, we must have f(W) = ⋁{ϕ(m, n) | (m, n) ∈ W }. Since (m, n) ∈ W if and only if ι(m, n) ≤ W in M ⊗ N, f is the left Kan extension of ϕ along ι. In particular, the identity is the left Kan extension of ι along ι, so ι is dense.

Using known properties of tensor products of sup-lattices, we have deduced that tensor products can be described as in Theorem 3.5. However, we can sharpen our understanding of the concepts involved, by showing that the universal property of the tensor product follows directly from the description in the theorem.

3.7. Proposition. For sup-lattices M, N, and L, a functor ϕ: M × N [figure]L is bi-sup-preserving if and only if the following equation holds, where γ is the downset comparison functor mentioned in Lemma 3.2:

[figure: M × N; DM × DN; M × N; ⋁×⋁; DM × DN; D(M × N); γ; D(M × N); L; D(M × N); D(M × N); DL; Dϕ; DL; L; ⋁; M × N; L; ϕ]

Proof. Assume that ϕ is bi-sup-preserving. For any (S, T) in DM ×DN, we have (using (−)^{↓ −} to denote the down-closure of a subset):

ϕ(⋁S, ⋁T) = ⋁{ϕ(s, ⋁T) | s ∈ S}
= ⋁{⋁{ϕ(s, t) | t ∈ T } | s ∈ S}
= ⋁{ϕ(s, t) | (s, t) ∈ S × T }
= ⋁{ϕ(s, t) | (s, t) ∈ S × T }^{↓ −}
= ⋁Dϕ(γ(S, T))

Conversely, assume that the equation given by the diagram holds, and consider an arbitrary subset A of M and an element b of N. Now

ϕ(⋁A, b) = ϕ(⋁A^{↓ −}, ⋁ ↓ b)
= ⋁Dϕ(γ(A^{↓ −}, ↓ b))
= ⋁Dϕ(γ(A^{↓ −}, {b}^{↓ −}))
= ⋁Dϕ(A × {b})^{↓ −}
= ⋁{ϕ(a, b)|a ∈ A}^{↓ −}
= ⋁{ϕ(a, b)|a ∈ A}

where the second equation is the assumption. Similarly, for any a ∈ M and B ⊆ N, ϕ(a, ⋁B) = ⋁{ϕ(a, b)|b ∈ B}.

In the introduction, we remarked that if ϕ : M × N [figure]L is bi-sup-preserving and l: L [figure]L′ is sup-preserving, then lϕ is bi-sup-preserving. This follows immediately from the characterization of bi-sup-preservation provided by Proposition 3.7, since “l preserves sups” is expressed by the following equation:

[figure: L; L′; l; DL; L; ⋁; DL; DL′; Dl; DL′; L′; ⋁]

which can be pasted to that of Proposition 3.7 along the edge ⋁ : DL [figure]L. We want to show that ι: M × N [figure]M ⊗ N is bi-sup-preserving. Our next lemma builds on our remarks in 3.6.

3.8. Lemma. The following equation holds:

[figure: M × N; M ⊗ N; ι; DM × DN; M × N; ⋁×⋁; DM × DN; D(M × N); γ; D(M × N); M ⊗ N; (−)^{∨∨}]

Proof. Let (S, T) be an element of DM×DN. We must show (S×T)^{∨∨} = (↓(⋁S, ⋁T))^{∨∨}. From S × T ⊆ (S × T)^{∨∨}, we have (⋁S, ⋁T) ∈ (S × T)^{∨∨}, which is the same as ↓(⋁S, ⋁T) ⊆ (S × T)^{∨∨} and hence (↓(⋁S, ⋁T))^{∨∨} ⊆ (S × T)^{∨∨}. On the other hand,

S × T ⊆ ↓ ⋁S × ↓ ⋁T = ↓(⋁S, ⋁T)

so (S × T)^{∨∨} ⊆ (↓(⋁S, ⋁T))^{∨∨}

3.9. Corollary. The functor ι: M × N [figure]M ⊗ N is bi-sup-preserving.

Proof. Consider the following diagram in the light of the diagrams in Proposition 3.7 and Lemma 3.8:

[figure: M × N; M ⊗ N; ι; DM × DN; M × N; ⋁×⋁; DM × DN; D(M ⊗ N); D(M ⊗ N); M ⊗ N; ⋁; DM × DN; D(M × N); γ; D(M × N); D(M ⊗ N); Dι; D(M × N); M ⊗ N; (−)^{∨∨}]

Commutativity of the outer square expresses the statement of the corollary. It remains to establish the equation given by the triangle. Since all arrows in the triangle preserve suprema, it suffices to show that the composites agree on principal downsets of M × N. In other words we have only to show

(↓(m, n))^{∨∨} = ⋁{(↓(a, b))^{∨∨} | (a, b) ≤ (m, n)}

which is trivial.

3.10. Lemma 3.7 shows that if a functor ϕ preserves suprema then, unlike the situation for abelian groups, ϕ is bi-sup-preserving. To see this, just observe that the triangle in the following diagram commutes:

[figure: M × N; DM × DN; M × N; ⋁×⋁; DM × DN; D(M × N); γ; D(M × N); L; D(M × N); D(M × N); DL; Dϕ; DL; L; ⋁; M × N; L; ϕ; D(M × N); M × N; ⋁]

Also, since γ: DM × DN [figure]D(M × N) has a left adjoint, given in terms of the product projections p and r by ⟨Dp, Dr⟩: D(M × N) [figure]DM × DN, and γ.(↓_{M} × ↓_{N}) = ↓_{M×N}, we have

[figure: DM × DN; D(M × N); ⟨Dp,Dr⟩; DM × DN; M × N; ⋁×⋁; D(M × N); M × N; ⋁]

Thus general suprema for M × N are suprema of rectangles. Of course, this does not say that bi-sup-preserving implies sup-preserving. (Given U in D(M × N), Dp(U) × Dr(U) is the smallest rectangle that contains U.)

Writing bisup(M ×N, L) for the ordered set of bi-sup-preserving functors from M ×N to L, and recalling our remark in 3.6 that a sup-preserving f with fι = ϕ is necessarily the left Kan extension of ϕ along ι, we have

sup(M ⊗ N, L) [figure: −·ι] bisup(M × N, L)

one to one.

3.11. Theorem. The sup-lattice M ⊗ N, as given by Theorem 3.5, classifies functors that are bi-sup-preserving, in the sense that

sup(M ⊗ N, L) [figure: −·ι] bisup(M × N, L)

is a bijection.

Proof. Any ϕ: M × N [figure]L gives rise to a unique sup-functor F : D(M × N) [figure]L for which F ↓_{M×N} = ϕ, namely the left Kan extension of ϕ along ↓_{M×N}, which is given by F = ⋁ · Dϕ. Now consider

[figure: D(M × N); D(DM × DN); D(⋁×⋁); D(M × N); D(DM × DN); D(⋁×⋁); D(M × N); DL; Dϕ; DL; L; ⋁; D(M × N); M ⊗ N; (−)^{∨∨}]

To show that − · ι of the theorem statement is surjective, it suffices to show that if ϕ: M × N [figure]L is bi-sup-preserving then F = ⋁Dϕ coinverts the inequality. For, in that case, we have a sup-preserving f : M ⊗ N [figure]L with f.(−)^{∨∨} = F, and hence

fι = f.(−)^{∨∨}. ↓_{M×N} = F ↓_{M×N} = ϕ

To show that ⋁Dϕ coinverts the inequality is, by Theorem 3.5, to show that its right adjoint takes values in M ⊗ N, which is to show, for all l ∈ L, that ϕ^{−1}(↓ l) ∈ M ⊗ N. So assume that, for (S, T) ∈ DM × DN, we have S × T ⊆ ϕ^{−1}(↓ l), which is equivalent to assuming that Dϕ(S × T) ⊆ ↓ l. We must show that (⋁S, ⋁T) ∈ ϕ^{−1}(↓ l). By Proposition 3.7, ϕ(⋁S, ⋁T) = ⋁Dϕ(S × T), but by applying ⋁ to the assumption, ⋁Dϕ(S × T) ≤ ⋁ ↓ l = l. So we have ϕ(⋁S, ⋁T) ≤ l and hence (⋁S, ⋁T) ∈ ϕ^{−1} ↓(l).

4. Sup-Arrows

4.1. We will soon turn to a description of M ⊗ N, for CCD lattices M and N, in terms of the totally below relation. For a and b in L a complete lattice, we define

a ≪ b iff (∀S ∈ DL)(b ≤ ⋁ S ⟹ a ∈ S)

and read “a is totally below b” for a ≪ b, as in [RW2]. (We caution that other authors use a ≪ b for the way below relation, which requires that the S in our definition be an up-directed downset. The two relations are not the same. Totally below trivially implies way below, but the converse is false. For example, in any power set lattice, to say that S is totally below T is to say that S is a sub-singleton subset of T while S is way below T if and only if S is a finite subset of T.) We will provide an interesting extension of the totally below relation to ordered sets that are not necessarily complete. Before doing so, we define a few other concepts, without completeness, that are familiar for complete lattices.

4.2. From [RW3], for any X in ord, we have (−)^{+} : DX [figure]UX = (D(X^{op}))^{op}, where, for S in DX, we define S^{+} = {u ∈ X | (∀s ∈ S)(s ≤ u)} as the set of upper bounds for S. Similarly, we have (−)^{−}: UX [figure]DX, where T^{−} is the set of lower bounds for T. We always have (−)^{+} ⊣ (−)^{−} and the two equations on the left below. The two equations on the right hold if X is complete (equivalently cocomplete).

[figure: X; UX; ↑; DX; X; ↓; DX; UX; (−)^{+}; UX; DX; (−)^{−}; ⊣; X; UX; ⋀; DX; X; ⋁; DX; UX; (−)^{+}; UX; DX; (−)^{−}; ⊣]

For the monad (−)^{+−} on DX, we will write (DX)^{+−} for the (−)^{+−}-closed subsets of DX. In ord, (DX)^{+−} is a full reflective subobject of DX, so it is also a complete lattice, and ↓ : X [figure]DX factors through (DX)^{+−}. We will write d: X [figure](DX)^{+−} for the first such factor.

4.3. Lemma. For x in X and S in DX, if ⋁ S exists then

x ∈ S^{+−} ⟺ x ≤ ⋁ S

.

Proof. Observe that ⋁S exists if and only if ⋀S^{+} exists, in which case they are equal.

\begin{matrix}x ∈ S^{+−} \\ (∀u ∈ S^{+})(x ≤ u) \end{matrix} ; x ≤ ⋀ S^{+} ; x ≤ ⋁ S

4.4. Corollary. For S in DX, ⋁ S exists if and only if S^{+−} ∩ S^{+} is non-empty.

4.5. Corollary. For S in DX, if ⋁ S exists then S^{+−} = ↓ ⋁ S.

Proof. Trivially, x ≤ ⋁ S if and only if x is in ↓ ⋁ S.

4.6. Corollary. An ordered set X is complete if and only if d: X [figure](DX)^{+−} is an equivalence.

For any f : X [figure]A in ord, we have Df : DX [figure]DA. If S in DX has a supremum in X and Df(S) has a supremum in A, then f preserves ⋁ S if and only if f(⋁ S) ≤ ⋁ Df(S) (the opposite inequality holding automatically). Lemma 4.3 allows us to express sup preservation for an arrow f : X [figure]A in ord without requiring existence of any suprema.

4.7. Definition. An arrow f : X [figure]A in ord will be called a sup-arrow if, for x ∈ X and S ∈ DX,

x ∈ S^{+−} ⟹ f(x) ∈ (Df(S))^{+−}

We write ord_{sup} for the locally full sub-ord-category of ord determined by the sup-arrows.

Note that a sup-arrow preserves any suprema that exist. For, if ⋁ S exists, then from ⋁ S ∈ S^{+−}, we have f(⋁ S) ∈ (Df(S))^{+−}, while it is trivial that f(⋁ S) ∈ (Df(S))^{+}, so by Corollary 4.4, f(⋁ S) = ⋁ Df(S).

Hence, if A is complete, then f is a sup-arrow if and only if

x ∈ S^{+−} ⟹ f(x) ≤ ⋁ Df(S)

Clearly, there is an inclusion functor, I : sup [figure]ord_{sup}. We should also note that (after extending the definition of Df to arbitrary functions between ordered sets) sup-arrows are automatically order preserving.

While ↓ : X [figure]DX preserves only trivial suprema, we have:

4.8. Theorem. For X an ordered set, the arrow d: X [figure](DX)^{+−} is a sup-arrow and provides the unit for an adjunction (D−)^{+−} ⊣ I: sup [figure]ord_{sup}.

Proof. For the first clause, let S be a downset of X, and take x ∈ S^{+−}. We must show d(x) ∈ (Dd(S))^{+−}. First observe that

(Dd(S))^{+} = {T ∈ (DX)^{+−} | (∃s ∈ S)(T ⊆ d(s))}^{+} = {U ∈ (DX)^{+−} | S ⊆ U}

It follows that, to show d(x) ∈ (Dd(S))^{+−} is to show d(x) ⊆ U for all U ∈ (DX)^{+−} which contain S. But this is to show x ∈ U for all U ∈ (DX)^{+−} which contain S. But this says precisely that x ∈ S^{+−}.

For the second clause, observe that any S ∈ (DX)^{+−} satisfies S ≅ ⋁{d(s) | s ∈ S}. It follows that, for any f : X [figure]A in ord_{sup} with A complete, there is at most one arrow f̂: (DX)^{+−} [figure]A in sup (to within isomorphism) satisfying the equation

[figure: X; (DX)^{+−}; d; X; A; f; (DX)^{+−}; A; f̂]

and it is given by f̂(S) = ⋁{f(s) | s ∈ S}. To see that f̂: (DX)^{+−} [figure]A as defined is an arrow in sup, we must show that f̂(⋁ 𝒮) ≤ ⋁ Df̂(𝒮), for any 𝒮 ∈ D((DX)^{+−}). But

f̂(⋁ 𝒮) = f̂((⋃ 𝒮)^{+−})
= ⋁{f(x) | x ∈ (⋃ 𝒮)^{+−}}

and

⋁ Df̂(𝒮) = ⋁{f̂(S) | S ∈ 𝒮 }
= ⋁{⋁{f(s) | s ∈ S} | S ∈ 𝒮 }
= ⋁{f(s) | s ∈ ⋃ 𝒮 }

so it suffices to show that, for x ∈ (⋃ 𝒮)^{+−}, f(x) ≤ ⋁{f(s) | s ∈ ⋃ 𝒮 }. We have this because f is a sup-arrow and ⋃ 𝒮 is a downset.

The theorem tells us that d: X [figure](DX)^{+−} is the completion of X that preserves any existing suprema in X. Indeed, it is the completion by one-sided Dedekind cuts.

5. The Totally Below Relation

5.1. Definition. For y and x in X in ord, we define

y ≪ x iff (∀S ∈ DX)(x ∈ S^{+−} ⟹ y ∈ S)

read y ≪ x as “y is totally below x”, and write ⇓ x = {y | y ≪ x}.

By Lemma 4.3, the definition of the totally below relation for general orders agrees with the previous definition for complete X. The elementary properties of ≪ for complete orders persist: for any (X, ≤), ≪_{X} is an order ideal from X to X (so b ≤ y ≪ x ⟹ b ≪ x and y ≪ x ≤ a ⟹ y ≪ a) and y ≪ x ⟹ y ≤ x. It follows that ≪ is transitive.

5.2. We recall that a completely distributive, CD, lattice is a complete lattice L which satisfies

(∀𝒮 ⊆ 𝒫L)(⋀{⋁S | S ∈ 𝒮 } = ⋁{⋀{T (S) | S ∈ 𝒮 } | T ∈ Π𝒮 }

where we have written Π𝒮 for the set of choice functions T on 𝒮 so that, for each S ∈ 𝒮, T (S) ∈ S. A complete lattice is constructively completely distributive, CCD, if it satisfies the above but with “∀𝒮 ⊆ 𝒫L” replaced by “∀𝒮 ⊆ DL”. Evidently, CD implies CCD, and the converse holds in the presence of the axiom of choice, AC. In fact, we have

(AC) ⟺ ((CD) ⟺ CCD)

which surely motivates the terminology. Many familiar theorems for CD lattices have been proven constructively for CCD lattices, so that they become theorems about CCD lattices in a topos. In particular we have, constructively, the Raney-Büchi theorem that a complete lattice is CCD if and only if it is a complete-homomorphic image of a complete ring of sets.

For our present purposes, we recall from [RW2] that a complete lattice L is CCD if and only if, for all x ∈ L, x ≤ ⋁ ⇓ x. In other words, every element of L is the supremum of all the elements totally below it. Since we have generalized the totally below relation from complete lattices to general ordered sets, the characterization of CCD lattices in this paragraph suggests the following:

5.3. Definition. An ordered set (X, ≤) is said to be STB if, for all x ∈ X, we have x ∈ (⇓ x)^{+−}. We write stb for the full subcategory of ord_{sup} determined by the (X, ≤) with the STB property.

It follows from Lemma 4.3 that a complete lattice is CCD if and only if it is STB as an ordered set. Hence the inclusion functor I : sup [figure]ord_{sup} restricts to an inclusion functor I : ccd_{sup} [figure]stb where ccd_{sup} is the full subcategory of sup determined by the CCD lattices. Clearly, the following diagram is a pullback:

[figure: stb; _{ord_{sup}}; ^{ccd^{sup}}; stb; I; ^{ccd^{sup}}; sup; sup; _{ord_{sup}}; I]

The STB condition allows a simple, useful characterization of (−)^{+−}-closed downsets. In fact, this characterization of (−)^{+−}-closed downsets characterizes STB orders:

5.4. Lemma. For (X, ≤) in ord, (X, ≤) is STB if and only if, for all S ∈ DX, S^{+−} = {x ∈ X | ⇓ x ⊆ S}.

Proof. Assume (X, ≤) is STB. If ⇓ x ⊆ S then x ∈ (⇓ x)^{+−} ⊆ S^{+−} shows x ∈ S^{+−}, while if x ∈ S^{+−} then for any y ≪ x we have y ∈ S, so that ⇓ x ⊆ S.

Conversely, assume the condition and, for any x ∈ X, consider the downset (⇓ x)^{+−} = {y ∈ X | ⇓ y ⊆ ⇓ x}. Since ⇓ x ⊆ ⇓ x, x ∈ (⇓ x)^{+−} and X is STB.

5.5. Lemma. (Interpolation) If (X, ≤) is STB and y ≪ x then (∃z)(y ≪ z ≪ x).

Proof. Let S = {u|(∃z)(u ≪ z ≪ x)} and assume y ≪ x, so that ⇓ y ⊆ S. By STB for X, y ∈ S^{+−} and since y is arbitrary ⇓ x ⊆ S^{+−}. By STB for X again, x ∈ S^{+−+−} = S^{+−}. But now y ≪ x ∈ S^{+−} implies y ∈ S.

Thus if (X, ≤) is STB, ≪ is idempotent as a relation from X to X. (To say that ≪ ∘ ≪=≪ is to say that ≪ ∘ ≪⊆≪, transitivity, and that ≪⊆≪ ∘ ≪, interpolativity in the sense of Lemma 5.5.) Recall the ord-category idm studied in detail in [MRW]. The objects of idm are pairs (X, <) where X is a set and < is an idempotent relation on X. An arrow f : (X, <) [figure](A, <) is a function f : X [figure]A for which x < y in X implies fx < fy in A. If f, g : X [figure]A in idm then f ≤ g if and only if, for all x < y in X, we have fx < gy in A. Notice that ord is a 2-full sub-ord-category of idm. Clearly, if (X, ≤) is STB then (X, ≪) is an object of idm and the identity function provides an arrow (X, ≪) [figure](X, ≤) in idm.

There is an alternative description of the arrows in stb.

5.6. Proposition. For STB objects X and A and f : X [figure]A in ord, f is in ord_{sup} (and hence in stb) if and only if

(∀a ∈ A, x ∈ X)(a ≪ fx ⟹ (∃y ∈ X)(a ≤ fy & y ≪ x))

Proof. Assume f ∈ ord_{sup} and a ≪ fx. Since X is STB, x ∈ (⇓ x)^{+−}, and then since f is a sup-arrow, f(x) ∈ (Df(⇓ x))^{+−}. By definition of ≪, we have a ∈ (Df(⇓ x)) so (∃y)(a ≤ f(y) and y ≪ x).

Conversely, assume the condition and x ∈ S^{+−}. To show f ∈ ord_{sup} we must show f(x) ∈ (Df(S))^{+−}. By Lemma 5.4, it is sufficient to show that, for a ≪ f(x), we have a ∈ Df(S). But by assumption we have y with a ≤ fy and y ≪ x. Since x ∈ S^{+−}, the second conjunct gives us y ∈ S and hence a ∈ Df(S).

We recall from [MRW] that the 2-functor D extends to idm. For any (X, <) in idm, we say that a subset S of X is a downset of the idempotent if

x ∈ S ⟺ (∃y)(x < y ∈ S)

We write D(X, <) for the set of downsets of (X, <), ordered by inclusion. In fact, see [RW2], D(X, <) is a CCD lattice and every CCD lattice arises in this way. The 2-natural transformation ↓ also extends to idm. For any (X, <) in idm we define ↓ : X [figure]D(X, <) by ↓ x = {y | y < x}.

5.7. Lemma. For x, y ∈ (X, ≤) an ordered set, x ≪ y in X if and only if ↓ x ≪ ↓ y in (D(X, ≤))^{+−}.

Proof. Assume x ≪ y and that, for 𝒮 ∈ D((D(X, ≤))^{+−}), we have ↓ y ⊆ ⋁𝒮 in (D(X, ≤))^{+−}. Now ⋃ 𝒮 is certainly a downset of D(X, ≤) and since ⋁𝒮 = (⋃ 𝒮)^{+−}, ↓ y ⊆ (⋃ 𝒮)^{+−}, so y ∈ (⋃ 𝒮)^{+−} and from from x ≪ y, we get x ∈ ⋃ 𝒮. Thus x ∈ S ∈ 𝒮, for some S ∈ 𝒮. Now we have ↓ x ⊆ S ∈ 𝒮 in (D(X, ≤))^{+−} so that ↓ x ∈ 𝒮 since 𝒮 is a downset of elements of (D(X, ≤))^{+−}. This shows that ↓ x ≪ ↓ y.

For the converse, assume ↓ x ≪ ↓ y and y ∈ S^{+−} for some S ∈ D(X, ≤). We know that S = ⋃{↓ s | s ∈ S}, so y ∈ S^{+−} gives y ∈ (⋃{↓ s | s ∈ S})^{+−}, which means that y ∈ ⋁{↓ s | s ∈ S} in (D(X, ≤))^{+−}. So ↓ y ⊆ ⋁{↓ s | s ∈ S} = ⋁{T | T ⊆ ↓ s & s ∈ S} in (D(X, ≤))^{+−} and {T | T ⊆ ↓ s & s ∈ S}, call it 𝒮, is a downset of (D(X, ≤))^{+−}.

Since ↓ x ≪ ↓ y, we have ↓ x ∈ 𝒮. But now ↓ x ⊆ ↓ s, for some s ∈ S. Hence x ≤ s ∈ S, and thus x ∈ S, which shows that x ≪ y.

5.8. Remark. Before stating the next theorem, it is convenient to point out that an STB order (X, ≤) allows us to construct D(X, ≪), for ≪ an idempotent, in addition to the usual D(X, ≤). Every ≪-downset is easily seen to be a ≤-downset and we leave it as an exercise for the reader to show that S^{∘} = {x ∈ X | (∃y)(x ≪ y ∈ S)} describes a right adjoint (−)^{∘}: D(X, ≤) [figure]D(X, ≪) to the inclusion i: D(X, ≪) [figure]D(X, ≤), and S^{∘} = ⇓ ⋁S.

5.9. Theorem. For (X, ≤) an ordered set, the following are equivalent:

(i) (X, ≤) is STB;

(ii) The composites

D(X, ≪) [figure: i; (−)^{∘}] D(X, ≤) [figure: (−)^{+−}; j] (D(X, ≤))^{+−}

are inverse isomorphisms;

(iii) D(X, ≪) ≅ D(X, ≤))^{+−};

(iv) (D(X, ≤))^{+−} is CCD.

Proof. (i) ⟹ (ii) For T ∈ D(X, ≪), we have T ⊆ (T^{+−})^{∘} from the composite of the adjunctions i ⊣ (−)^{∘} and (−)^{+−} ⊣ j. For S ∈ (D(X, ≤))^{+−}, we have (S^{∘})^{+−} ⊆ S, also from the composite adjunction. Using the characterization given in Lemma 5.4, we have (T^{+−})^{∘} = {x | (∃y)(x ≪ y & ⇓ y ⊆ T)} ⊆ T. On the other hand, again by Lemma 5.4, (S^{∘})^{+−} = {y | ⇓ y ⊆ S^{∘}}. Take y ∈ S. Then for any x ≪ y, we have x ∈ S^{∘}. Thus ⇓ y ⊆ S^{∘}, and so y ∈ (S^{∘})^{+−}. So S ⊆ (S^{∘})^{+−}.

(ii) ⟹ (iii) is trivial.

(iii) ⟹ (iv) follows from the fact that all lattices of the form D(A, <) for < an idempotent on a set A are CCD.

(iv) ⟹ (i) Assume (D(X, ≤))^{+−} is CCD, and take x ∈ X. We have

x ∈ ↓ x = ⋁{S ∈ (D(X, ≤))^{+−} | S ≪ ↓ x}
= ⋁{⋁{↓ s | s ∈ S} | S ≪ ↓ x}
= ⋁{↓ s | s ∈ S ≪ ↓ x}
= ⋁{↓ s | ↓ s ≪ ↓ x}
= ⋁{↓ s | s ≪ x}
= (⋃{↓ s | s ≪ x})^{+−}
= {t | t ≪ x}^{+−}
= (⇓ x)^{+−}

where the fifth equality uses Lemma 5.7.

5.10. Remark. In the special case where X of the theorem is taken to be a CCD lattice L, then a minor replacement in (ii), using Corollary 4.5, gives us that the composites

D(L, ≪) [figure: i; (−)^{∘}] D(L, ≤) [figure: ⋁; ↓] L

are inverse isomorphisms. This is Proposition 13 of [RW2].

Since D(X, ≪) is a CCD lattice it follows that (D−)^{+−} : ord_{sup} [figure]sup restricts to give (D−)^{+−} : stb [figure]ccd_{sup} and the following corollary follows immediately from Theorems 4.8 and 5.9.

5.11. Corollary. For X an STB order, the arrow d: X [figure](DX)^{+−} is a sup-arrow and provides the unit for a 2-adjunction (D−)^{+−} ⊣ I: ccd_{sup} [figure]stb.

We deduce further:

5.12. Corollary. The mate with respect to the adjunctions (D−)^{+−} ⊣ I in the pullback diagram preceding Lemma 5.4 is also an equality and the resulting diagram

[figure: stb; _{ord_{sup}}; ^{ccd^{sup}}; stb; (D−)^{+−}; ^{ccd^{sup}}; sup; sup; _{ord_{sup}}; (D−)^{+−}]

is also a pullback.

Observe that the condition of Proposition 5.6 is implied by

(∀a ∈ A, x ∈ X)(a ≪ fx ⟹ (∃y ∈ X)(a ≪ fy & y ≪ x))

simply because a ≪ fy implies a ≤ fy.

5.13. Lemma. If X and A are STB orders and f : X [figure]A is a function that preserves merely ≪, then the condition above is equivalent to the condition of Proposition 5.6.

Proof. Assume the condition of Proposition 5.6, and let a ≪ fx. We have z with a ≤ fz and z ≪ x. From the second conjunct, we have z ≪ y ≪ x, and since f preserves ≪, we have a ≤ fz ≪ fy and hence a ≪ fy (and y ≪ x).

Since the displayed condition above is the condition for an arrow f : (X, ≪) [figure](A, ≪) in idm between STB orders (X, ≤) and (Y, ≤) to be a sup-arrow and it makes no mention of order preservation, we generalize one step further and say:

5.14. Definition. An arrow f : (X, <) [figure](A, <) in idm is a sup-arrow if

(∀a ∈ A, x ∈ X)(a < fx ⟹ (∃y ∈ X)(a < fy & y < x))

We caution however that a sup-arrow in idm does not speak about preserving suprema with respect to the idempotents <, even if the idempotents should happen to be reflexive relations and hence orders. We have not defined suprema for general idempotents here (and have no need to do so) but it can be done using the 2-structure of idm.

5.15. We write idm_{sup} for the locally-full sub-2-category of idm determined by the sup-arrows. We recall from [RW2] that an arrow f : L [figure]A in ccd_{sup} preserves the totally below relation if and only if the right adjoint of f has a right adjoint, so that f is a map in sup, meaning that f has a right adjoint in the 2-category sup. We will write ccd_{mapsup} for the locally full sub-2-category of ccd_{sup} determined by the maps. It follows from Lemma 5.13 that there is a forgetful functor (−, ≪) : ccd_{mapsup} [figure]idm_{sup}, which sends a CCD lattice L to the idempotent (L, ≪) given by its totally below relation, and regards a map f : L [figure]A in sup as an arrow f : (L, ≪) [figure](A, ≪) in idm_{sup}.

5.16. Theorem. For (X, <) an idempotent, the arrow ↓ : X [figure]D(X, <) in idm gives an arrow ↓ : (X, <) [figure](D(X, <), ≪) in idm_{sup}, and provides the unit for a 2-adjunction D ⊣ (−, ≪) : ccd_{mapsup} [figure]idm_{sup}.

Proof. Since D(X, <) is a CCD lattice, (D(X, <), ≪) is also an idempotent. It was shown in [RW2] that if x < y in X then ↓ x ≪ ↓ y in D(X, <). Now assume S ≪ ↓ x. We have S ⊆ ↓ t and t < x. We interpolate to get t < y < x and now S ⊆ ↓ t, t ∈ ↓ y, and y < x provides S ≪ ↓ y and y < x, which shows ↓ : (X, <) [figure](D(X, <), ≪) in idm_{sup}. Next assume that we are given an arbitrary f : (X, <) [figure](A, ≪) in idm_{sup}, with A a CCD lattice. To finish the proof of the theorem, we must show that there is a unique (to within isomorphism) arrow f̂: D(X, <) [figure]A in ccd_{mapsup} for which (f̂, ≪) satisfies the following equation in idm_{sup}.

[figure: (X, <); (D(X, <), ≪); ↓; (X, <); (A, ≪); f; (D(X, <), ≪); (A, ≪); f̂]

For every element S in D(X, <), we have S = ⋁{↓ s | s ∈ S}. Thus any f̂ satisfying our requirements must have

f̂(S) = f̂(⋁{↓ s | s ∈ S}) = ⋁{f̂(↓ s) | s ∈ S} = ⋁{fs | s ∈ S}

Thus it remains to show that f̂(S) = ⋁{fs | s ∈ S} meets all of our requirements. To show that the equation f̂. ↓ = f holds, we have

f̂(↓ s) = ⋁{fx | x < s} = ⋁{a | a ≤ fx & x < s}
= ⋁{a | a ≪ fs} = fs

The last equality holds because A is CCD and the penultimate equality uses the properties of f being in idm_{sup}. Now f̂ preserves all suprema because, taking 𝒮 in D(D(X, <)), we have

f̂(⋁𝒮) = f̂(⋃ 𝒮) = ⋁{fs | s ∈ ⋃ 𝒮 } = ⋁{⋁{fs | s ∈ S} | S ∈ 𝒮 }
= ⋁{f̂(S) | S ∈ 𝒮 }

Because f̂preserves suprema and D(X, <) is complete, it follows that f̂has a right adjoint in ord. This right adjoint has a right adjoint (making f̂ an arrow in ccd_{mapsup}) if and only if f̂ preserves ≪. (See [RW2].) So assume S ≪ T in D(X, <). We have S ⊆ ↓ t for some t ∈ T and hence also t < u for some u ∈ T. Applying f̂ and f we have:

f̂(S) ≤ f̂(↓ t) = ft ≪ fu ≤ f̂(T)

and hence f̂(S) ≪ f̂(T).

6. Tensor Products of CCD Lattices

6.1. The paper [RW2] exhibits a biequivalence between ccd_{sup} and the idempotent splitting completion of the bicategory of relations, kar(rel), which has a tensor product that is given on objects by cartesian product. The paper then shows that the tensor product of CCD lattices as sup-lattices agrees with the tensor product of kar(rel). We conclude now with yet another description of the tensor product of CCD lattices that uses our results about the totally below relation.

6.2. Lemma. For CCD lattices M and N, the reflector (−)^{∨∨}: D(M × N) [figure]M ⊗ N is given by U^{∨∨} = {(m, n) | ⇓ m × ⇓ n ⊆ U}

Proof. Provisionally write \overline{U} = \{(m, n) | ⇓ m × ⇓ n ⊆ U\}. To show that \overline{U} ∈ M ⊗ N, assume we have S × T ⊆ \overline{U} for (S, T) ∈ DM × DN. We need to show (⋁S, ⋁T) ∈ \overline{U}. For this we require ⇓ ⋁S × ⇓ ⋁T ⊆ U. From Remark 5.8 this means precisely that we require S^{∘} × T^{∘} ⊆ U and we recall that S^{∘} = {x | (∃s)(x ≪ s ∈ S)}. So if we have (x, y) ∈ S^{∘} × T^{∘}, we have x ≪ s ∈ S and y ≪ t ∈ T with (s, t) ∈ S × T ⊆ \overline{U}. So (x, y) ∈ ⇓ s×⇓ t ⊆ U. Thus \overline{U} ∈ M ⊗N. It is clear that, for any U ∈ D(M ×N), we have U ⊆ \overline{U}. Assume now that W ∈ M ⊗ N and U ⊆ W. It suffices to show that \overline{U} ⊆ W. But if (m, n) satisfies ⇓ m × ⇓ n ⊆ U then U ⊆ W implies ⇓ m × ⇓ n ⊆ W and hence (m, n) = (⋁ ⇓ m, ⋁ ⇓ n) ∈ W. Since \overline{(−)} is left adjoint to the inclusion κ: M ⊗ N [figure]D(M × N, ≤), \overline{U} = U^{∨∨}.

Generalizing very slightly what we observed in Remark 5.8, we note that every downset of M × N with respect to the idempotent ≪_{M} × ≪_{N} is a downset of M × N with respect to ≤_{M×N}=≤_{M} × ≤_{N} so that we have an inclusion

i: D(M × N, ≪_{M} × ≪_{N}) [figure]D(M × N, ≤)

It has a right adjoint

(−)^{∘}: D(M × N, ≤) [figure]D(M × N, ≪_{M} × ≪_{N})

which, for U ∈ D(M × N, ≤), is given by U^{∘} = {(a, b) | ∃((x, y) ∈ U)(a ≪ x & b ≪ y)} Again, we leave the details to the reader.

6.3. Theorem. For CCD lattices M and N CCD, M ⊗ N ≅ D(M × N, ≪_{M} × ≪_{N}). The composites

D(M × N, ≪_{M} × ≪_{N}) [figure: i; (−)^{∘}] D(M × N, ≤) [figure: (−)^{∨∨}; κ] M ⊗ N

are inverse isomorphisms;

Proof. Write < for the idempotent ≪_{M} × ≪_{N} on M × N. For any V ∈ D(M × N, <), we have V ⊆ V^{∨∨∘} and, for any W ∈ M ⊗ N, we have W^{∘∨∨} ⊆ W, by adjointness. Now take (x, y) ∈ V^{∨∨∘}. This implies (x, y) < (m, n) ∈ V^{∨∨}, which implies

(x, y) ∈ ⇓ m × ⇓ n & (m, n) ∈ V^{∨∨}

which implies (x, y) ∈ V, so that V^{∨∨∘} ⊆ V. Finally, assume (x, y) ∈ W. We want to show that (x, y) ∈ W^{∘∨∨}, which is to show ⇓ x × ⇓ y ⊆ W^{∘}. For any (a, b) ∈ ⇓ x × ⇓ y, its membership in W^{∘} is witnessed by (x, y).

6.4. Remark. The reader may have noticed that the proof of Theorem 6.3 is similar to that which establishes the isomorphism (ii) in Theorem 5.9. Both can be seen to follow from (a dual of) Eilenberg and Moore’s theorem, Proposition 3.3 in [E&M]. This is the theorem which asserts that for t ⊣ g: A [figure]A in the 2-category of categories, with t underlying a monad and g a comonad, the category of algebras A^{t} is isomorphic to the category of coalgebras A_{g}, via a functor that identifies the forgetful functors. Eilenberg and Moore’s theorem is easily seen to hold in any 2-category in which the objects A^{t} and A_{g} exist. In particular, it holds in each of the duals of the 2-category of categories and in the duals of ord. Thus if g ⊣ t then the Kleisli categories, A^{g} and A_{t} are isomorphic via a functor that identifies the free functors. If a monad t is idempotent, then the Eilenberg-Moore object and the Kleisli object coincide and the Kleisli arrow is the left adjoint of the Eilenberg-Moore arrow. In ord all monads and comonads are idempotent.

6.5. Remark. For M and N CCD lattices, the (fully faithful) adjoint string

D(↓ × ↓) ⊣ 𝒟(↓ × ↓) ⊣ D(↓ × ↓)

gives rise to the longer adjoint string

D(⇓ × ⇓) ⊣ D(⋁ × ⋁) ⊣ D(↓ × ↓) ⊣ 𝒟(↓ × ↓) ⊣ D(↓ × ↓)

In the terminology of [RW4], these are distributive adjoint strings and the inverter, λ, of the inequality D(⇓ × ⇓) ≤ D(↓ × ↓) is necessarily the left adjoint of the left adjoint of the inverter, κ, of D(↓ × ↓) ≤ D(↓ × ↓). It follows that, for M and N CCD lattices, M ⊗ N can equally well be calculated as the inverter of D(⇓ × ⇓) ≤ D(↓ × ↓). Of course the inclusions λ and κ are in general different but it is easy to calculate and see that the inverter of D(⇓ × ⇓) ≤ D(↓ × ↓) reveals directly that M ⊗ N is the set of downsets of (M × N, ≤) that are also downsets for the idempotent ≪_{M} × ≪_{N} as already shown in Theorem 6.3. Moreover, the fully faithful adjoint string λ ⊣ (−)^{∨∨} ⊣ κ reveals M ⊗ N to be a complete quotient of D(M × N) and hence CCD by Proposition 11 of [F&W].

[figure: 𝒟(M × N); 𝒟(𝒟M × 𝒟N); D(⇓ × ⇓); ⊥; 𝒟(M × N); 𝒟(𝒟M × 𝒟N); D(⋁ × ⋁); ⊥; 𝒟(M × N); 𝒟(𝒟M × 𝒟N); D(↓ × ↓); ⊥; 𝒟(M × N); 𝒟(𝒟M × 𝒟N); 𝒟(↓ × ↓); ⊥; 𝒟(M × N); 𝒟(𝒟M × 𝒟N); D(↓ × ↓); M ⊗ N; 𝒟(M × N); λ; ⊥; M ⊗ N; 𝒟(M × N); (−)^{∨∨}; ⊥; M ⊗ N; 𝒟(M × N); κ]

References

[E&M] S. Eilenberg and J.C. Moore. Adjoint functors and triples. Illinois J. Math. 9 (1965), 381–398.

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

[J&T] A. Joyal and M. Tierney. An extension of the Galois theory of Grothendieck. Memoirs of the American Mathematical Society, Vol. 51, No. 309, 1984.

[KEL] G. M. Kelly. Basic Concepts of Enriched Category Theory, London Math. Soc. Lecture Notes Series 64, Cambridge University Press, 1982.

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

[MRW] F. Marmolejo, Robert Rosebrugh, and R.J. Wood. Duality for CCD lattices. Theory Appl. Categ. 22 (2009), No. 1, 1–23.

[PIT] A.M. Pitts. Applications of sup-lattice enriched category theory to sheaf theory. Proc. London Math. Soc. 57 (1988), 433–480.

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

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

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

[RW4] Robert Rosebrugh and R.J. Wood. Distributive adjoint strings Theory Appl. Categ. 1 (1995), No.6, 119–145.

[S&W] R. Street and R.F.C Walters. Yoneda structures on 2-categories. J. Algebra 75 (1982), 538–545.

Department of Mathematics and Statistics Dalhousie University Halifax, NS, B3H 3J5 Canada

Email: tkenney@mathstat.dal.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/24/11/24-11.{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, Ecole Polytechnique Fédérale de Lausanne:

gavin seal@fastmail.fm

Transmitting editors.

Clemens Berger, Université de Nice-Sophia Antipolis, cberger@math.unice.fr 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 Tom Leinster, University of Glasgow, T.Leinster@maths.gla.ac.uk 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