Constructive Complete Distributivity II^{∗}

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

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

Abstract

A complete lattice, L, is constructively completely distributive, (CCD)(L), if the sup map defined on down closed subobjects has a left adjoint. It was known that in boolean toposes (CCD)(L) is equivalent to (CCD)(L^{op}). We show here that the latter property for all L (sufficiently, for Ω) characterizes boolean toposes.

∗Research partially supported by grants from NSERC Canada. Diagrams typeset using catmac.

Introduction

The notion of constructive complete distributivity for a complete ordered set L, (CCD)(L), was defined in [1] to mean the existence of a left adjoint to ⋁ : DL ⟶ L, where DL is the set of down-closed subsets of L ordered by inclusion. Terminology springs from (i) the fact that (CCD)(L) is equivalent to

(∀S ⊆ DL) (⋀ {⋁ S | S ∈ S} = ⋁ {⋀ {T (S) | S ∈ S} | T ∈ ΠS})

(which becomes the condition for complete distributivity of L, (CD)(L), if D is replaced by P,the power set functor) and (ii) the following:

Theorem 1 (ac) ⟺ ((CD) ⇔ (CCD)), where (ac) denotes the axiom of choice.

Somewhat less cryptically, the (CCD) condition is the restriction of the more familiar (CD) to down-closed subsets; it implies the stronger condition in the presence of the axiom of choice which in turn is implied by identifying the two notions of distributivity.

Thus, in classsical lattice theory, with the axiom of choice freely assumed, it would appear that (CCD) is simply an easier condition to verify than (CD). However, a considerable body of literature has explained the value of doing Mathematics in a topos and in this more general context the very definition above and Theorem 1 suggest that (CCD) is the relevant notion. Indeed, in any topos, PX is (CCD) for all X while the statement “PX is (CD) for all X” is equivalent to choice.

The power objects, PX, in a topos are not, in general, boolean algebras and it transpires that booleaness of the topos of “sets” does make a substantial difference to the theory of constructive complete distributivity. For a topos E, we write (boo)(E) to indicate that PX is boolean for all X in E. We write (CCD^{op})(L) for (CCD)(L^{op}). With this notation, Theorem 18 of [1] becomes:

(boo) ⟹ ((CCD) ⇔ (CCD^{op})).

Somewhat contrary to intuition, the hypothesis is necessary. In this note we prove:

Theorem 11 (boo) ⟺ ((CCD) ⇔ (CCD^{op})).

Even in a general topos, ( )^{op} is an involution, so

((CCD) ⇒ (CCD)^{op}) ⟹ ((CCD)^{op} ⇒ (CCD)).

To prove Theorem 11 we will show that (CCD) ⇒ (CCD)^{op} reduces to (CCD)^{op}(Ω), where Ω ≅ P1 ≅ D1 is the subobject classifier of the topos. This reduction involves showing that

(CCD)(L) ⟹ (∀X in ord(E))((CCD)(ord(E)(X, L)))

where ord(E) is the 2-category of ordered objects in E. (As in [1], an order is assumed to be reflexive and transitive, but not necessarily antisymmetric.) This follows from the observation that powers of (CCD) objects are (CCD) which in turn follows from the fact that arbitrary products of (CCD) objects are (CCD) .

1 The Main Result

For any topos, E, the subobject classifier, Ω_{E}, is a locale (complete heyting algebra) in E. On the other hand, given any locale, L, in set the subobject classifier for Γ : sh(L) ⟶ set enjoys Γ(Ω_{sh(L)}) ≅ L. However, the logic of E when viewed from E itself is more classical. The fact that Ω_{E} is always (CCD) shows this. In fact, more is true:

Theorem 2 In any topos we have

[figure: Ω; DΩ; ↓_{Ω}; ⊥; ⊥; ⊥; ⊥]

More generally, for any ordered object X, ↓_{DDX} has such a string of adjoints.

Proof. It suffices to observe that Ω ≅ D1 ≅ DD0 and argue as in [1, Theorem 3].

(The adjoint string exhibiting set as a total category in [5] arises in a similar way, starting with the empty category; the common thread is what is called a yoneda structure in [4].)

The situation for Ω^{op} is quite different unless E is boolean. Indeed, the proof of Theorem 10 towards the end of this section shows that if Ω^{op} is merely a locale then Ω (and hence E) is boolean. That this is somewhat contrary to intuition, as claimed in the Introduction, is seen by considering

Ω = ([figure: {; ϕ; <; ξ; <; τ; }; {; ϕ; <; τ; }] )

in set^{2}. The distributive law for binary meets over binary joins intuitionistically implies its dual. Since both the domain and codomain of the above example are finite and the lattice structure is “pointwise” it appears at first glance that all distributivities are consequences of the binary ones. However, even in this simple example the infinitary operations ⋁ : DΩ ⟶ Ω and ⋀^{op} : DΩ^{op} ⟶ Ω^{op} cannot be obtained by considering all iterates of their binary counterparts. Conceptually: Ω is not cardinal finite. Technically: the functions witnessing {ϕ < ξ < τ} and {ϕ < τ} as (CCD^{op}) objects of set do not give an arrow of set^{2}.

Another illustration of this sort of phenomenon is encountered when one considers the infinite demorgan law. We digress slightly.

For H a (not necessarily complete) heyting algebra, (HEY)(H), we write : H^{op} ⟶ H for its negation and observe that we always have ^{op} ⊣ .

In spite of the fact that is a right adjoint, we always have 1 ≅ 0 which is usefully construed as a fragment of left exactness of ^{op}. Indeed, demorgan’s law, (DML)(H), (a ∧ b) ≤ a ∨ b, holds if and only if ^{op} is left exact, in which case is “geometric” modulo (HEY^{op})(H) and completeness of H. We say that H satisfies the infinite demorgan law, (IDM)(H) if and only if

op preserves all infs, which occurs precisely if has a right adjoint. It is easy to see that H is boolean, (BOO)(H), if and only if ⊣ ^{op}. Clearly, the following implications hold for heyting algebras in any topos:

(BOO) ⟹ (IDM) ⟹ (DM)
(BOO) ⟹ (HEY^{op})

In general, they are all strict. To see that (BOO) ⟹ (IDM) is strict it suffices to consider a finite heyting algebra in set, H, for which we have (DM)(H) but not (BOO)(H). From finiteness we have (DM)(H) ⟹ (IDM)(H). Clearly, 3 = {ϕ < ξ < τ} will do. However, Ω in set^{2} illustrates that (IDM) ⟹ (DM) is strict. Once again, (DM)(Ω) follows immediately from pointwise considerations, but (IDM)(Ω) fails via the same obstructions as (CCD^{op})(Ω).

But Ω is not a mere locale in its own topos. In showing the equivalence of (CCD^{op})(Ω) and (BOO)(Ω) it is convenient also to establish their equivalence with (IDM)(Ω) and (HEY^{op})(Ω). The next two lemmas are crucial. (In neither case is α assumed to be order-preserving.)

Lemma 3 (Higgs) (α : Ω[figure] Ω) ⟹ (α^{2} = 1_{Ω}).

Proof. Consult Johnstone [2], exercise 3, p.44.

Lemma 4 (Bénabou) (α ≤ 1_{Ω} : Ω ⟶ Ω) ⟹ (α(π) = π ∧ α(τ)).

Proof. Let μ : U[figure] Ω be (a representative of) the subobject classified by α : Ω[figure] Ω, so that

[figure: Ω; Ω; α; U; 1; !_{U}; μ; τ]

is a pullback and

[figure: U; 1; !_{U}; Ω; μ; τ; =]

the latter since τ is classified by 1_{Ω} and α ≤ 1_{Ω}. We must show that

α = ([figure: Ω; Ω × Ω; (1_{Ω}, α · τ·!_{Ω}); Ω; ∧]) .

The subobject classified by ∧ is (τ, τ) : 1[figure] Ω × Ω so the result follows if and only if

[figure: Ω; Ω × Ω; (1_{Ω}, α · τ·!_{Ω}); U; 1; !_{U}; μ; (τ, τ)]

is a pullback; this follows easily from the information now assembled.

Corollary 5 (α ≤ 1_{Ω} and α(τ) = τ) ⟹ (α = 1_{Ω}).

Theorem 6 (IDM)(Ω) ⟹ (BOO)(Ω)

Proof. Assume that : Ω^{op} ⟶ Ω has a right adjoint, ρ : Ω ⟶ Ω^{op}. The counit for the adjunction gives ρ ≤ 1_{Ω}. We have ρ(τ) = ϕ, since ρ is a right adjoint, and thus ρ(τ) = ϕ = τ. It follows from Corollary 5 that ρ = 1_{Ω} so that ρ is a (split) monomorphism. By Lemma 3 we have ρ^{op}ρ = 1_{Ω}, hence ρ = 1_{Ω^{op}}ρ = ^{op}ρ^{op}ρ = ^{op}1_{Ω} = ^{op}, and hence Ω is boolean.

Lemma 7 For L a (CCD) object of ord(S) and I in S, L^{I} is a (CCD) object of ord(S).

Proof. A product of (CCD) objects is (CCD) [3], or observe that (CCD) is equivalent to saying that, for any family S of down-closed subsets of L, we have

⋀ {⋁ S | S ∈ S} = ⋁ (∩S)

and this identity is constructively inherited by powers.

Lemma 8 For L a (CCD) object of ord(S) and X an object in ord(S), we have ord(S)(X, L) is a (CCD) object of ord(S).

Proof. The arrow D|X| ⟶ X in ord(S) gives rise to ord(S)(X, L) ⟶ ord(S)(D|X|, L) ≅ L^{|X|}, the inclusion of order preserving arrows in all arrows from X to L. Since L is complete the latter has both left and right adjoints, given by Kan extensions. Since L^{|X|} is (CCD) the adjoint string exhibits ord(S)(X, L) as a (CCD) object. See [1, Proposition 10].

Theorem 9 ((CCD) ⇔ (CCD^{op})) ⟺ (CCD^{op})(Ω)

Proof. We always have (CCD)(Ω). See [1, Corollary 4]. So the equivalence of (CCD) and (CCD^{op}) trivially implies (CCD^{op})(Ω). For the converse, assume (CCD^{op})(Ω), that is (CCD)(Ω^{op}), and (CCD)(L). We need to show (CCD)(L^{op}). From

[figure: L; DL; ⋁; ⇓; ↓_{L}; ⊥; ⊥]

application of ( )^{op} : ord^{co}(S) ⟶ ord(S) gives

[figure: L^{op}; (DL)^{op}; ^{⋁ op}; ↓_{L}^{op}; ⇓ ^{op}; ⊥; ⊥; ≅ (ord(S)(L^{op}, Ω))^{op} ≅ ord(S)(L, Ω^{op}).]

By Lemma 8, we have (CCD)(ord(S)(L, Ω^{op})). and so by [1, Proposition 11], we have (CCD)(L^{op}).

Theorem 10 (CCD^{op})(Ω) ⟹ (BOO)(Ω).

Proof. As noted in [1], a complete object L is a locale, (LOC)(L), if and only if ⋁ : DL ⟶ L is left exact; hence (CCD) implies (LOC). In particular, our hypothesis makes Ω^{op} a heyting algebra, the negation for which, à priori distinct from ^{op}, we write as −( ) : Ω ⟶ Ω^{op}. Necessarily, −^{op} − ( ) ≤ 1_{Ω} and −^{op} − (τ) = τ, giving, by an application of Corollary 5, −^{op} − ( ) = 1_{Ω}. Thus Ω^{op}, and hence Ω, is boolean.

(The implications of Theorems 6 and 10 are trivially reversible.) Combining Theorem 10 with Theorem 9 and Theorem 18 of [1] we have:

Theorem 11 (boo) ⟺ ((CCD) ⇔ (CCD^{op})).

References

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

[2] Peter T. Johnstone. Topos Theory. Academic Press, 1977.

[3] Robert Rosebrugh and R. J. Wood. Constructive complete distributivity 3. to appear, 1991.

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

[5] R. J. Wood. Some remarks on total categories. Journal of Algebra, 75:538–545, 1982.