BRICS RS-95-20 A. Kock: The Constructive Lift Monad

BRICS

Basic Research in Computer Science

The Constructive Lift Monad

Anders Kock

BRICS Report Series RS-95-20 ISSN 0909-0878 March 1995 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1995, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent publications in the BRICS Report Series. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK - 8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@daimi.aau.dk

BRICS publications are in general accessible through WWW and anonymous FTP:

http://www.brics.aau.dk/BRICS/
ftp ftp.brics.aau.dk (cd pub/BRICS)

The Constructive Lift Monad

Anders Kock

March 28, 1995

The lift monad is the construction which to a poset freely adjoins a bottom element to it, or equivalently (from the classical viewpoint), the construction which freely adjoins suprema for subsets with at most one element. In constructive mathematics (i.e. inside a topos), these two constructions are no longer equivalent, since the equivalence is based on the boolean reasoning that a set with at most one element either is a singleton {x}, or is empty.

Likewise based on boolean reasoning is the proof of two important properties of the lift monad T:

1) If a poset C has filtered suprema, then so does T C.

2) Every poset with a bottom element ⊥ is ”free”, i.e. comes about by applying T to some poset (namely the original poset less the bottom).

Both these properties fail to hold constructively, if the lift monad is interpreted as ”adding a bottom”; see Remark below. If, on the other hand, we interpret the lift monad as the one which freely provides supremum for each subset with at most one element (which is what we shall do), then the first property holds; and we give a necessary and sufficient condition that the second does. Finally, we shall investigate the lift monad in the context of (constructive) locale theory.

I would like to thank Bart Jacobs for guiding me to the litterature on Z-systems; to Gonzalo Reyes for calling my attention to Barr’s work on totally connected spaces; to Steve Vickers for some pertinent correspondence. I would like to thank the Netherlands Science Organization (NWO) for supporting my visit to Utrecht, where a part of the present research was carried out, and for various travel support from BRICS^{1}

1Basic Research in Computer Science, Centre of the Danish National Research Foundation.

The first Section of the present article subsumes my 1992 [15].

1 The lift monad on posets

We shall consistently talk about the arbitrary topos in which we work as if it were the category of sets.

There are several ways to describe the free cocompletion T (C) of a poset C with respect to suprema over subterminal sets (i.e. over sets with at most one element). We shall give two descriptions (equivalent in all toposes). The first is simpler, and the second makes the monad structure, universal properties etc. clearer, and in particular, puts the lift monad into the general context of cocompletion monads.

In the first description, T (C) is given as the set of partial elements of C, meaning the set of maps U → C with U a subterminal set, i.e. a subset of the one-point set 1. The set of these partial elements inherits a partial order from that of C in combination with the partial order on the set of subsets of 1; we shall describe this partial order in a more general context, replacing the set 1 by an arbitrary set X; not so much for the added generality, but for psychological reasons: it is easier to think of the lattice of subsets of an unspecified set X, rather than on the lattice of subsets of 1 (=the lattice Ω of truth values).

For any poset C and any set X, we may form a new poset T_{X}(C), fibered over Ω(X) (= the set of subsets of X) as follows. Its elements are partial maps from X to C, i.e. maps of form c : U → C, where U ⊆ X is a subset. The order relation on these partial maps is the obvious one:

(c : U → C) ≤ (d : V → C)

if U ⊆ V and c ≤ d | U (= the restriction of d to U). (Thus T_{X}(C) is the total space of the fibration over Ω(X) obtained by the Grothendieck construction for the functor Ω(X)^{op} → Posets sending U to Hom(U, C).)

Proposition 1 If C has filtered suprema, then so does T_{X}(C).

Proof. Let I be a filtered poset, and (c_{i})_{i∈I} a family of elements of T_{X}(C) with c_{i} ≤ c_{j} if i ≤ j. Let U_{i} denote the domain of c_{i}, so also U_{i} ⊆ U_{j} for i ≤ j. For each fixed i ∈ I, we have a family of elements in Hom(U_{i}, C) indexed by ↑ i (= the set of elements in I above i), namely

c_{j} | U_{i} for j ≥ i.  (1)

This evidently is a filtered family, and since Hom(U_{i}, C) inherits from C the property of having filtered suprema, the family ( 1) has a supremum, which we call d_{i}.

We claim that

d_{i} = d_{k} | U_{i} for i ≤ k.  (2)

For the inequality ≤, let c_{j} | U_{i} be one of the elements participating in the supremum defining d_{i}. Pick an index l dominating both j and k (using that I is filtering). Then c_{j} ≤ c_{l} | U_{j}, so

c_{j} | U_{i} ≤ c_{l} | U_{i} = (c_{l} | U_{k}) | U_{i} ≤ d_{k} | U_{i},

the last inequality because c_{l} | U_{k} paticipates in the supremum that defines d_{k}. So d_{i} ≤ d_{k} | U_{i}. For the other inequality: since the restriction map Hom(U_{k}, C) → Hom(U_{i}, C) preserves filtered suprema (in fact all kind of algebraic structure which C has), it follows that d_{k} | U_{i} is the supremum of the family of elements c_{l} | U_{i} for l ≥ k, thus is ≤ the supremum of the larger famly of elements c_{l} | U_{i} for l ≥ i, so is ≤ d_{i}. This proves the claim.

It now follows that the d_{i} : U_{i} → C form a compatible family of elements, i.e. there exists a unique d : ⋃ U_{i} → C with d | U_{i} = d_{i} for all i. This d is readily seen to be the supremum in T_{X}(C) of the c_{i}’s. First, c_{i} ≤ d_{i} = d | U_{i} ≤ d for all i, so it is an upper bound. If, on the other hand, c_{i} ≤ e in T_{X}(C) for all i, e is defined on a subset W of X containing ⋃ U_{i}, and we have c_{i} ≤ c_{j} | U_{i} ≤ e | U_{i} for all j ≥ i, and since d_{i} was defined as sup of such c_{j} | U_{i}, d_{i} ≤ e | U_{i}. This holds for all i, from which follows that d ≤ (e | ⋃ U_{i}) in Hom(⋃ U_{i}, C), so d ≤ e in T_{X}(C). So d is the least upper bound, as required.

In a similar vein, we have the follwing, easier, Proposition. In the formulation we give, ”sup-lattice” means that all suprema exist; ”inf-lattice” may be taken to mean either that all infima, or all finite infima only, exist.

Proposition 2 If C is a a sup lattice, resp. an inf lattice, resp. a frame, then so is T_{X}(C).

Proof. This is easier than the previous Proposition; the reason (which also allows one to prove an array of related results) is that C now has all suprema, implying in particular that left Kan extensions with values in it exist, in particular, if i : U → V is an inclusion, and a : U → C a map, there is a smallest \overline{a} : V → C with \overline{a} ∘ i = a. To get suprema in T_{X}(C) of a family a_{i} : U_{i} → C with U_{i} ⊆ X, one forms ⋁ \overline{a_{i}} in the frame Hom(⋃ U_{i}, C), where \overline{a_{i}} denotes the Kan extension of a_{i} to ⋃ U_{i}. Similarly the meet of a : U → C and b : V → C is just (a | U ∩V)∧(b | U ∩V). We leave the proof of the frame distributivity law a ∩ ⋁ b_{i} = ⋁(a ∩ b_{i}) to the reader: for this, one uses both the frame distributivity law in the individual hom-sets Hom(U, C), as well as the frame distributivity law for the lattice Ω(X). (So if C is a coframe, i.e. C^{op} is a frame, it does not, similarly, follow that T_{X}(C) is a coframe. In fact, it won’t be, in general; see the comparison in Section 2 below between the op-lift and scone monads.)

We leave to the reader to prove the following results in the same spirit.

Proposition 3 If C has and F : C → D preserves filtered suprema, then T_{X}(F) : T_{X}(C) → T_{X}(D) preserves filtered suprema.

Proposition 4 If C has and F : C → D preserves (finite) infima, then T_{X}(F) : T_{X}(C) → T_{X}(D) preserves (finite) infima.

Remark. For the simple monad 1 + − on P OS, (”freely adding a bottom element”), the conclusions of Propositions 1 and 2 fail, unless the topos is a deMorgan one (in the sense of [6]). For the 1-point poset 1 is a frame, and (hence) also has filtered sup, but 1+1 cannot be a frame, nor have filtered sup unless the topos is deMorgan. The first statement is clear from [6], and the second can be reduced to it: for, if U ⊆ 1 is subterminal, 1 + U is filtered (filtered, of course, means: inhabited, and ...). (I am indebted to Steve Vickers for this argument). Therefore the inclusion 1 + U ⊆ 1 + 1 has a supremum. Thinking of U as a truth value ∈ Ω, this provides a retraction of Ω onto 1 + 1 ⊆ Ω, and this again implies deMorgan’s law, cf. loc.cit.

The T_{X}, as described, is an endofunctor on the category P OS of posets; we write T for the special case where X = 1. This T is (the functor part of) the lift monad, in the first description. To describe its monad structure and further special properties, we give a second description, namely: T (C) is the set of quasi-principal subsets of C, in the sense of Definition 2 below. This second description will also put T into the context of order completion monads in general, in the sense extensively studied in the literature, cf. e.g. [1], [11], [17], [21], [23], and in partiular put it into the context of KZ-monads, [14].

Recall that the full cocompletion monad J on the category P OS of posets is the construction which to a poset C associates the set J(C) of all lower subsets of C, i.e. subsets D ⊆ C such that if b ≤ a ∈ D then b ∈ D. The order on J(C) is just the inclusion ordering of subsets. Every a ∈ C gives rise to a ”principal” lower set ↓ (a) = {b ∈ C | b ≤ a}, and the map ↓: C → J(C) thus defined is an order-preserving inclusion map.We also denote it ↓_{C}. To say that C is cocomplete (or union-complete, or supremumcomplete) is to say that ↓_{C} has a left adjoint ξ : J(C) → C; then ξ is necessarily supremum formation, ξ(D) = sup D for any lower subset D of C. All the order completion constructions Z of [1], [23] are in fact submonads of this monad, cf. [17], and they share with J the property that left adjoints for ↓ are exactly supremum formation for the relevant kind of lower sets; (in fact these left adjoints are also the structure maps in the monad theoretic sense, since the abstract theory of KZ-monads [14] can be seen to seen to apply).

The most well known of these submonads Z is the monad Idl, where Idl(C) is the set of filtering lower subsets of C (ideals, in the terminology of [7]). This special case led Thatcher, Wagner, Wright, Venugopalan and others to generalize a family of notions and terminology from continuous lattice theory to general Z: Z-continuous and Z-algebraic posets, and the Zway-below relation. Recall from [16] or [7] that a poset C is called continuous if ↓: C → Idl(C) not only has a left adjoint (=supremum formation for filtered lower subset) but this left adjoint in turn has a left adjoint. We shall study the relationship between these notions for the case of the lift monad; our main result being that in this case, the notions of continuous and algebraic agree.

To describe the lift monad we first make the following

Definition 5 A subset D ⊆ C of a poset C is quasi-principal if

(∃a ∈ D) ⇒ (∃b ∈ C : D =↓ (b)).

(Thus, to the extent D is inhabited, it is principal. In classical logic, any set is either inhabited or empty, so besides the principal subsets ↓ (b), the only other quasi-principal subset is the empty one.)

The lift monad T is now defined by letting T (C) consist of the quasiprincipal subsets of C. To argue that T (C) ⊆ J(C) is to argue that quasiprincipal subsets are lower sets. This argument goes: if a′ ≤ a ∈ D, where D is quasi-principal, then D is inhabited, as witnessed by a, so D =↓ (b) for some b. Since a′ ≤ a ≤ b, a′ ∈↓ (b) = D. Slightly more involved is

Proposition 6 T is a submonad of J.

Proof. First, it is a subfunctor. Recall that J becomes a functor by the recipe that if f : C → B is an order preserving map between posets, then J(f) takes the lower set D ⊆ C to ↓ f(D), where generally

↓ X = {y ∈ B | ∃x ∈ X with y ≤ x},

for any subset X of any poset B. Now it is clear that if D is quasi-principal in C, then J(f)(D) is quasi-principal in B. The unit for J is the formation ↓ of principal lower sets, and it clearly factors through T. It remains to be seen that the ”multiplication” of J (which is union formation) restricts to one for T. So we should prove that if F ⊆ J(C) is a quasi-principal family (in the ordering ⊆) of quasi-principal subsets of C, then ⋃ F is a quasi-principal subset of C. So assume that ⋃ F is inhabited. Then there is some a ∈ ⋃ F, hence there is some D with a ∈ D ∈ F. Then D witnesses F to be inhabited, hence principal, so there exists some quasi-principal set W ⊆ C such that

F = {V ∈ T (C) | V ⊆ W }.

In particular D ⊆ W. Since a ∈ D ⊆ W, W is inhabited, hence principal, W =↓ w. We claim that ↓ w = ⋃ F, proving the desired principality of the latter. One inclusion is clear: ifv ≤ w, then v ∈↓ w ∈ F, so v ∈ ⋃ F. Conversely, if v ∈ ⋃ F, we have v ∈ V ∈ F for suitable V, but since F is ↓ W, v ∈ V ⊆ W =↓ w, so v ≤ w, or v ∈↓ w. This proves the Proposition.

(One may alternatively see T as a case of the F am monad (cf e.g. [9]), namely ”families with at most one member” - which, unlike most F ammonads does restrict to a monad on Posets.)

Let C be a poset. If X ⊆ C is a subset with at most one element (so X is subterminal, in the terminology of [13]), then the set ↓ X is clearly quasi-principal. Conversely, if D ⊆ C is quasi-principal, the set

D_{0} = {b ∈ C | D =↓ b}

is subterminal; and ↓ (D_{0}) = D, (↓ X)_{0} = X. So there is hereby established a bijective correspondence

T (C) ≅ C̃,

between the set T (C) of quasi-principal subsets of C and the set C̃ of subterminal subsets of the (underlying set of) C. (The inclusion ordering on the right is generally weaker than the inclusion ordering on the left, though.) The bijection has clearly the property that it preserves supremum formation: the supremum of a subterminal subset X exists iff the supremum of the quasi-principal ↓ X does, and then these suprema are equal. This proves the equivalence of the first two assertions in

Proposition/Definition 7 Let C be a poset. Then the following conditions are equivalent

(1) Every subterminal subset X of C has a supremum

(2) Every quasi-principal subset D of C has a supremum

(3) The order-preserving map ↓: C → T (C) has a left adjoint (which then is supremum formation for quasi-principal subsets)

(4) C can be equipped with structure of algebra for the monad T.

If either of these conditions hold, C is called weakly cocomplete.

Proof. The equivalence of (2) and (3) is standard: analyzing the universal property of supremum formation in adjointness terms. The equivalence of (3) and (4) follows because the monad T is a KZ-monad in the sense of [14].

We now follow [23] and [21] in generalizing the way-below notion, and related concepts from continuous lattice theory into general order completion theory, here for the weak cocompletion (which is a ”union-complete subset system”, in the terminology of [23]).

Let C be a weakly cocomplete poset, and a,b ∈ C. We say that b is T - way-below a, written b ≪_{T} a, if for every quasi-principal D with a ≤ sup D, we have b ∈ D. We say that a is T -compact, or positive if a ≪_{T} a. We say that C is T -continuous if the supremum formation sup : T (C) → C has a left adjoint ⇓, (which is then necessarily given by ⇓ (a) = the set of elements T -way-below a), and we say that C is T -algebraic if it is of the form T (B) for some poset B (which is then necessarily (isomorphic to) the poset of positive elements of C).

We shall henceforth often omit the subscript T when referring to these notions.

(Note that in the boolean situation, an element is positive iff it is not the bottom element; the present positive way of expressing this property is related to a notion of ”positive elements in locales” considered in [8] and [18]. In fact, for any poset with a top element, an element a is T -compact iff every cover of a is inhabited.)

For general reasons, we have that b′ ≤ b ≪ a ≤ a′ implies b′ ≪ a′, and that ≪ satisfies an interpolation property; we shall not recall the latter, since we in our special case have the much stronger

Proposition 8 Let b ≪ a. Then a ≪ a. (”An element way-above anything is necessarily positive.”)

Proof. Let D be quasi-principal with a ≤ sup D. By the assumption that b ≪ a, b ∈ D, so D is inhabited, hence principal, D =↓ (c), say. So a ≤ sup D =↓ (c), thus a ≤ c, and therefore a ∈↓ (c) = D.

Corollary 9 If b ≤ a and b is positive, then a is positive.

Proof. We have b ≪ b ≤ a whence b ≪ a, so a is positive, by the Proposition.

Let now C be a (T -) continuous poset, and let P os(C) be the set of positive elements in C, with ordering induced from C.

Proposition 10 For any a ∈ C, the set P os(C)∩ ↓ (a) is quasi-principal in P os(C); and ↓ (P os(C)∩ ↓ (a)) is quasi-principal in C.

Proof. Assume that the set P os(C)∩ ↓ (a) is inhabited, witnessed by b, say. Then b ≤ a, and b is positive, so by the Corollary, a is positive, whence the set in question is the principal lower set of the poset P os(C) generated by a. The second assertion is a formal consequence of the first.

In the generality of Z-continuous posets, it is quite generally the case that Z-algebraic implies Z-continuous. (It can in fact be proved in the generality of KZ monads, cf. [14], Theorem 3.2). But for the special T at hand here, we have, conversely

Theorem 11 Every T -continuous poset is T -algebraic.

Proof. The crux in the proof is the implication ⇒ in the following

Lemma 12 A poset C is T -continuous iff every element is supremum of the positive elements below it.

Proof. Assume T -continuity. Let a ∈ C. By the assumption of T -continuity of C, we have

a ≤ sup{b ∈ C | b ≪ a}.

(Actually, we have equality.) By Proposition 8, the subset over which we are forming supremum is contained in {b ∈ C | (b ≤ a) ∧ a ≪ a}. If we replace each b which occurs in this supremum formation with a (which is ≥ each such b) the supremum will be at least as big. So we have

a ≤ sup D,

where D is the (subterminal) subset which consists of a alone, but only to the extent that a ≪ a, i.e. to the extent that a is positive. Since the other inequality is clear, a = sup D, and now the Lemma is proved by the fact that D contains only positive elements. (The reader may philosophize over the plural form used here, since there is at most one element in D; but the English language deems, apparently, that plural versus singular is not a quantitative distinction, but a qualitative one: plural is the indefinite number, say 0 or 1,..., whereas singular is the definite one.)

Conversely, assume that every element is sup of the positive elements below it. The adjointness is proved by proving, for each a ∈ C, two inequalities. First we prove a ≤ sup ⇓ (a). Write a = ⋁ b_{i} with the b_{i}’s positive, using the assumption. So it suffices to prove b_{i} ≤ sup ⇓ a, for each of the b_{i}’s. But they are positive, so b_{i} ≪ b_{i} ≤ a, so belong to ⇓ a and thus participate in the sup-formation. The other inequality to be proved is ⇓ sup(U) ⊆ U for any quasi-principal U. Let a belong to the left hand side, so a ≪ sup(U). Proposition 8 now implies that sup(U) is positive, and since it is covered by U, U therefore is inhabited, hence principal, say U =↓ b. So a ≪ sup(U) = b, so a ≤ b, so a ∈↓ b = U. This proves the Lemma.

From here on, the argumentation is quite standard. Define f : C → T (P os(C)) by

f(a) := P os(C)∩ ↓ (a),

which is indeed in T (P os(C), by Proposition 10; and f is clearly order preserving; and define g : T (P os(C)) → C by

g(D) := sup(D);

we have to argue that this supremum exists (and then, g will clearly be order preserving). But it is easy to see that ↓ (D) is quasi-principal in C if D is quasi-principal in P os(C). So then the supremum of ↓ (D) exists in C, hence so does the supremum of D.

We finally see that f and g are mutually inverse to another. First, by the Lemma, we get that g(f(a)) = a for any a ∈ C. Also, for D ∈ T (P os(C)),

f(g(D)) = f(sup D) = P os(C)∩ ↓ sup(D),

which evidently contains D as a subset. But conversely, if b ∈ f(g(D)), then b is positive, and b ≤ sup(D) = sup ↓ D. Since ↓ D is quasi-principal in C and b is positive, this implies that b ∈ D. This proves the Theorem.

Remark 1. If C is a discrete poset, then T (C) consists of the subterminal subsets of C, so that T (C) = C̃, where the tilde denotes the partial-map classifier monad in the sense of topos theory, and justifies the use of the same letter T for the lift monad studied in the present note, and the partialmap classifier monad studied in [13]. One can, in fact, characterize those T -continuous posets which are of the form T (C) for C discrete as those which are shallow in the sense of [13]. For, assume T (C) shallow, and a ≤ b in C, hence a ≤ b in T (C). By shallowness, a = sup({a} ∩ {b}). But by the proof of Theorem 7, the elements of C ⊆ T (C) are exactly the positive elements of T (C). Since a thus is positive in T (C) and a = sup{a} ∩ {b}, a ∈↓ ({a} ∩ {b}) which implies that {a} ∩ {b} is inhabited, hence a = b.

In [13], it is shown that if a set X carries an algebra structure ξ : T X → X for the partial-map-classifier monad, this structure gives rise to a (shallow) partial order ≤ on X, with ξ supremum formation; but ξis not adjoint to the unit X → T X, since the latter is not order-preserving. So the partialmap-classifier monad, i.e. the lift monad, on sets, cannot be construed as a KZ-monad. But in a certain other world of sets, namely the one described in Synthetic Domain Theory (cf. e.g. [3] and the references therein), every set acquires a canonical preorder, and in this context, the partial map classifier is in fact a KZ-monad, as proved in loc. cit.

Remark 2. Let us remark that T is a commutative monad in the sense of the author, cf. e.g. [12] and the references therin; for, it is a submonad of J, which is commutative. Since the category P OS of posets is Cartesian closed, the more specific notions of [12] apply. We claim that the equivalent conditions of loc.cit. Proposition 2.2 hold (so that T is a relevant monad in the sense of Bart Jacobs, [5]). Here it just means that the two canonical maps

T (A × B) ^{\overline{}κ} T (A) × T (B) ^{\overline{}ψ} T (A × B)

compose to the identity map on T (A × B). In fact, let W ⊆ A × B be quasi-principal. By the first map, W goes to (proj_{1}(W), proj_{2}(W)), and this again by the second to proj_{1}(W) × proj_{2}(W). Since the other inclusion is clear, it suffices to prove

proj_{1}(W) × proj_{2}(W) ⊆ W.

But if (a, b) belongs to the left hand side, W must be inhabited, hence principal, say W =↓ (a_{0} × b_{0}), and a ∈ proj_{1}(W) implies a ≤ a_{0}, and similarly b ≤ b_{0}, so (a.b) ∈↓ (a_{0}, b_{0}) = W.

The other composite

T A × T B ^{\overline{}ψ} T (A × B) ^{\overline{}κ} T A × T B

can be shown to be ≤ the identity map on T A × T B, and so κ ⊣ ψ, meaning that T is of the interesting kind of KZ monads studied by Vickers in [22].

Remark 3. Proposition 1 and 3, for X = 1, i.e. for the lift monad T posets, can easily be upgraded to the statement that there is a distributive law of the monad Idl over the lift monad T, so that T lifts to a monad on the category of Idl- algebras (=posets with filtered suprema). One just has to further observe that f C has filtered suprema, the unit C → T C preserves them (as does the multiplication of the monad, being a left adjoint).

I don’t know to what extent the distributive laws between T and the ”nonempty suprema monad” P^{+}, considered in the context of classical boolean logic in [5], carry over to the constructive setting.

2 Lift and scone for locales

According to Proposition 2, T (C) is a frame whenever C is, but the monad T, ↓, ⋃ is not a monad on the category F RM of frames, since the unit map ↓: C → T (C) does not preserve bottom element, so is not a frame map. There is, however, a left adjoint sup : T (C) → C for ↓, since a frame is cocomplete, hence weakly cocomplete. But it is easy to see, using the frame distributivity law for C, that sup : T (C) → C is left exact, i.e. preserves binary inf as well as top element. For binary inf, let D_{1} and D_{2} be quasiprincipal sets. Then their meet D_{1} ∩ D_{2} is quasi-principal; for, if D_{1} ∩ D_{2} is inhabited, then so are D_{1} and D_{2}, say D_{1} =↓ d_{1}, D_{2} =↓ d_{2}, and then D_{1} ∩ D_{2} =↓ (d_{1} ∧ d_{2}), and thus is principal. Thus D_{1} ∩ D_{2} is the meet of D_{1} and D_{2} in the poset T (C) of quasi-principal subsets of C. And applying the frame distributivity law twice, it is easy to see that

⋁ D_{1} ∧ ⋁ D_{2} = ⋁_{d_{1}∈D_{1}} ⋁_{d_{2}∈D_{2}} d_{1} ∧ d_{2} ≤ ⋁ D_{1} ∩ D_{2},

the other inequality being obvious. Preservation of top element by sup = ⋁ is even easier, since the top element of T (C) is not only a quasi-principal subset of C, but actually the principal ↓ 1. Also the map ⋃ : T T C → T C has a left adjoint, namely T (↓_{C}), by a general theorem about KZ-monads,

[14] Theorem 3.2. Furthermore, it is easy to see that this T (↓_{C}) is in fact left exact: First, it preserves top element, since the top element of T (C) is of form ↓_{C} (1_{C}), and since T (↓_{C})∘ ↓_{C}=↓_{T C} ∘ ↓_{C}, and this latter composite is a right adjoint, so preserves top element. Also, T (↓_{C}) preserves binary ∧: we already argued that ∧ in T C is just ∩. So this means that we should prove that

T (↓_{C})(D_{1}) ∩ T (↓_{C} (D_{2}) ⊆ T (↓_{C})(D_{1} ∩ D_{2})  (3)

for D_{1} and D_{2} quasi-principal subsets of C. So assume that F belongs to the left hand side. But then, for i = 1, 2, T (↓_{C})(D_{i}) is inhabited (witness F !), and since T (↓_{C}) is essentially direct image formation (along ↓_{C}), it follows that the D_{i}’s are inhabited, hence principal, D_{i} =↓_{C} (d_{i}). But using again T (↓_{C})∘ ↓_{C}=↓_{T C} ∘ ↓_{C}, it is easy to see that if D_{i} =↓_{C} (d_{i}), the two sides in ( 3) are equal. So F belongs to the right hand side as well.

If we now (like in [7]) take the category of locales LOC to be the category of those order preserving maps f = f_{∗} between frames which have left exact left adjoints f^{∗}, then T, ↓, ⋃ is a monad on the category LOC. If we make LOC into a 2-category, by letting the 2-cells be the inequalities between the f^{∗}’s, the 2-cells we already have between the f_{∗}’s making T, ↓, ⋃ into a KZ monad on P OS, give, by mating, 2-cells in the opposite direction between the f^{∗}’s, so therefore T, ↓, ⋃ is an op-KZ monad when considered on the category LOC, i.e. a monad where structures are right adjoint to units.

Concerning the algebras for this lift monad T on LOC, we have the following result. Recall (Theorem 11 and Lemma 12) that a T -continuous poset is a (weakly cocomplete) poset such that every element in it is a sup of positive elements. (For frames/locales, this in turn can be expressed: C is an open locale, cf. [8].)

Theorem 13 Let C be a locale. Then t.f.a.e:

1) C admits a structure (necessarily unique) for T

2) the positive elements in C are stable under finite intersections; and C is T -continuous.

3) for any locale D, the poset LOC(D, C) has a maximal element, preserved by composition with any locale map D′ → D; and C is T -continuous.

4) (If C corresponds to a sober topological space X) X has a maximal point in the specialization ordering (i.e. X is a totally connected space, in the sense of Barr [2]).

Proof. Assume 1). A T -structure is a right adjoint (locale-) map for the locale map ↓, or equivalently, passing to their left adjoints, a left adjoint (frame-) map for the frame map sup : T (C) → C. Such a left adjoint is then necessarily given by the recipe a ↦⇓ a, the set of elements T -way below a. This map is therefore a frame map, in particular preserves finite infima. Assume that a and b are positive, so a ≪ a and b ≪ b, and hence 0 ≪ a and 0 ≪ b, so 0 ∈⇓ a∩ ⇓ b ⊆⇓ (a ∧ b), the last inclusion because ⇓ preserves binary inf. But by Proposition 8, this implies that a∧b is positive. Similarly, since ⇓ preserves top element, ⇓ 1 =↓ 1, so 1 ≪ 1, so 1 is positive. Finally, the mere existence of such left adjoint on the level of posets already means that it is T -continuous. This proves 2).

Assume 2). To prove 3), it suffices to prove existence of a maximal frame map C → D, (preserved by post-composition with any frame map D → D′); we construct a frame map π : C → Ω, and then post-compose that with the unique frame map δ : Ω → D. This π, we define as follows: for a ∈ C, π(a) is taken to be the truth value of the statement that a is positive. This is a left adjoint (cf. [8]) so preserves sup, and the assumption 2) implies that it preserves finite infs as well, so it is a frame map, as required. To see the maximality of δ ∘ π in F RM(C, D) , let ϵ : C → D be any other frame map, and let a ∈ C. We write a = ⋁{a | a is positive} (using the assumption of T -continuity of C, cf. the proof of Lemma 12). Then

ϵ(a) = ⋁{ϵ(a) | a is positive} ≤ ⋁{1_{D} | a is positive} = δ(π(a)).

The preservation by post-composition is now clear, so 3) holds.

Assume 3). Then in particular there is a ”universally” maximal frame map π : C → Ω (i.e. preserved by post-composition). By the universality, μ ∘ π is a maximal frame map C → C (where μ : Ω → C denotes the unique such frame map), and hence μ ∘ π ≥ identity map of C, which is one of the inequalities for proving π left adjoint to μ; the other inequality is trivially an equality, since Ω is an initial frame. But now this adjointness π ⊣ μ implies that π(a) in fact is the truth value of ”a is positive”, cf. again [8]. To prove 1), we construct a left adjoint frame map ξ : C → T (C) for sup. The candidate we present for this is given by

ξ(a) := {b ∈ C | b ≤ a; and π(a)},

which clearly is quasi-principal (namely inhabited iff π(a) is the truth value true, in which case ξ(a) =↓ (a)). First, ξ is a splitting of sup; for, sup({b ∈ C | b ≤ a; and π(a)}) = a, by the proof of Lemma 12. Secondly, to prove the other adjunction inequality ξ(sup(D)) ⊆ D for any quasi-principal D, let a belong to the left hand side. So a ≤ sup(D) and π(sup(D)); so sup(D) is positive; so if s ≤ sup(D), it follows that s ∈ D, so that D is principal. But this applies in particular to s = sup(D). So sup(D) ∈ D. But then the fact that D is a lower set and a ≤ sup(D) implies a ∈ D. This proves the adjointness required for 1), but we still have to argue that the constructed ξ is a frame map, i.e. that it commutes with finite inf; this is an easy consequence of the fact that π and sup do. So 1) is proved.

Assume finally that the frame C comes from a sober topological space X, C = O(X). Assume 3). Then in particular, the maximal frame map π : O(X) → Ω corresponds, by soberness, to a unique point x_{0} of X, maximal with respect to the specialization ordering. Conversely, if 4) holds, the assumed maximal point witnesses that the space X is inhabited, and for any inhabited space X, O(X) is evidently T -continuous. The maximal point corresponds to a maximal frame map O(X) = C → Ω, and we have to see that it remains maximal by post-composition with any frame map. Let D be any frame, let ϵ : C → D be an arbitrary frame map, and μ : Ω → D the unique such frame map. To prove ϵ(a) ≤ μ(π(a)), it suffices, since O(X) is supgenerated by inhabited subsets, to consider the case when a is an inhabited subset. But then x_{0} ∈ a, being maximal in the specialization ordering, and so π(a) is true ∈ Ω, so μ(π(a)) = 1, so the inequality is trivial. This proves 3), and thus the Theorem.

Classically, i.e. in a boolean topos, the lift monad T on LOC considered here just freely adds a bottom element to (the underlying poset of) the frame C. One may also want, instead, to freely add a top element to it C + 1, as is done in e.g. [4] p. 122, to get a co-lift monad on LOC. This works in a boolean topos; but it does not work in general, for the similar reason as considered before, namely that 1 is a frame, but 1+1 not. And now the formal dual of the lift monad does not work either: it is the functor C ↦ (T (C^{op}))^{op} which to a poset freely adjoins subterminal infima, and reasonably could be called the (constructive) op-lift monad. For, when applied to a frame, the resulting poset will not in general be a frame. To wit, applied to the one-element frame 1, the op-lift monad gives Ω^{op} which is not a frame, in general.

However, a construction that works in general has been considered, (at least for toposes rather than locales), namely the scone construction, cf. loc.cit. p. 190. For locales this construction S may be described as follows. Let C be a frame. Let Ω be the frame of truth values. There is a unique frame map γ^{∗} : Ω → C, with right adjoint (locale map) γ_{∗} : C → Ω. Then S(C) is the subframe of Ω×C consisting of pairs (λ, a) with γ^{∗}(λ) ≤ a or equivalently λ ≤ γ_{∗}(a). (Thus, S(C) arises as the comma construction γ^{∗} ↓ C). Note that the constructive lift monad on locales, considered above, may also be described by a comma category construction, namely T (C) = C ↓ γ^{∗}.

The scone construction on LOC carries a monad structure, it is in fact a KZ monad (structures are left adjoint to units; but recall that the direction of the 2-cells is governed by the inverse image maps (frame maps)).

The following result is basically known (except possibly for the condition 2)), from [10], (cf. also [9], [4]), and is included for completeness, and for comparison with the previous theorem on the lift monad T on LOC

Theorem 14 Let C be a locale. Then t.f.a.e.

1) C admits a structure for the scone-monad S on LOC.

2) The map γ_{∗} : C → Ω is a fibration of posets

3) The topos sh(C) defined by the locale C is local in the sense of [10].

4) For any locale D, there is a minimal element in LOC(D, C), preserved by pre-composition with any locale map D′ → D.

5) (If C corresponds to a sober topological space X) The space has a minimal point in the specialization ordering (i.e. is a focal space, in the sense of [4]).

(The reason for the equivalence of condition 2) and 1) is that the scone construction is really a special case of that ”comma-category” op-KZ-monad on CAT/S whose algebras Street in [20] identified as being the fibrations over S (”Chevalley Criterion”); here, S is taken to be the poset Ω.)

References

[1] B.Banaschewski and E.Nelson, Completions of partially ordered sets, SIAM J.Comp. 11 (1982), 521-528

[2] M.Barr, Fuzzy set theory and topos theory, Canad. Math. Bull. 29 (1986), 501-508

[3] Marcelo Fiore, Lifting as a KZ-doctrine, preprint, Dept. of Computer Science, Edinburgh January 1995

[4] P.Freyd and A.Scedrov, Categories, Allegories, North Holland 1991

[5] B.Jacobs, Semantics of weakening and contraction, Annals Pure Appl. Logic (to appear, 1994)

[6] P.T.Johnstone, Conditions related to de Morgan’s law, in Applications of Sheaves, Proceedings Durham 1977, Springer Lecture Notes in Math. 753 (1979), 479-491 [7] P.T.Johnstone, Stone spaces, Cambridge University Press 1982

[8] P.T.Johnstone, Open locales and exponentiation, in Mathematical Applications of Category Theory, Contemporary Math. 30 (1984), 84-116

[9] P.T. Johnstone, Partial products, bagdomains and hyperlocal toposes, in Applications of Categories in Computer Science, L.M.S. Lecture Notes Series no 177 (Cambridge University Press, 1992), 315-339

[10] P.T.Johnstone and I.Moerdijk, Local maps of toposes, Proc. Lond. Math. Soc. (3) 58 (1989), 281-305

[11] A.Kock, Limit monads in categories, Aarhus Preprint Series 1967/68 No.6

[12] A.Kock, Bilinearity and Cartesian closed monads, Math.Scand.29 (1971), 161-174

[13] A.Kock, Algebras for the partial map classifier monad, in Carboni et al. (ed.) Category Theory, Proceedings, Como 1990 Springer Lecture Notes in Math. 1488

[14] A.Kock, Monads for which structures are adjoint to units, Journ. Pure Appl. Alg (to appear)

[15] A.Kock, Constructive theory of the lift monad on posets, Aarhus Math. Institute Preprint Series 1992 No. 22

[16] G.Markowsky, A motivation and generalization of Scott’s notion of continuous lattices, in Springer Lecture Notes in Mathematics 871 (1982)

[17] J.Meseguer, Order completion monads, Alg. Universalis 16 (1983),63-82

[18] I.Moerdijk, Continuous fibrations and inverse limits of toposes, Compositio Math. 58 (1986), 45-72

[19] D.Novak, Generalization of continuous posets, Trans.A.M.S. 272 (1982), 645-667

[20] R.Street, Fibrations and Yoneda’s Lemma in a 2-category, in Category Seminar, Sydney 1972/73, Springer Lecture Notes in Math. 420 (1974), 104-133 [21] P.Venugopalan, Z-continuous posets, Houston J. Math. 12 (1986), 275-

294

[22] Steve Vickers, Locales are not pointless, Preprint, Imperial College, London Sept 1994

[23] J.B.Wright, E.G.Wagner and J.W.Thatcher, A uniform approach to inductive posets and inductive closure, in Springer Lecture Notes in Computer Science 53 (1977), 192-212

Recent Publications in the BRICS Report Series

RS-95-20 Anders Kock. The Constructive Lift Monad. March 1995. 18 pp.

RS-95-19 Franc�ois Laroussinie and Kim G. Larsen. Compositional Model Checking of Real Time Systems. March 1995. 20 pp.

RS-95-18 Allan Cheng. Complexity Results for Model Checking. February 1995. 18pp.

RS-95-17 Jari Koistinen, Nils Klarlund, and Michael I. Schwartzbach. Design Architectures through Category Constraints. February 1995. 19 pp.

RS-95-16 Dany Breslauer and Ramesh Hariharan. Optimal Parallel Construction of Minimal Suf�x and Factor Automata. February 1995. 9 pp.

RS-95-15 Devdatt P. Dubhashi, Grammati E. Pantziou, Paul G. Spirakis, and Christos D. Zaroliagis. The Fourth Moment in Luby’s Distribution. February 1995. 10 pp. To appear in Theoretical Computer Science.

RS-95-14 Devdatt P. Dubhashi. Inclusion�Exclusion(3) Implies Inclusion�Exclusion(n). February 1995. 6 pp.

RS-95-13 Torben Bra� uner. The Girard Translation Extended with Recursion. 1995. Full version of paper to appear in Proceedings of CSL ’94, LNCS, 1995.

RS-95-12 Gerth St�lting Brodal. Fast Meldable Priority Queues. February 1995. 12 pp.

RS-95-11 Alberto Apostolico and Dany Breslauer. An Optimal O(log log n) Time Parallel Algorithm for Detecting all Squares in a String. February 1995. 18 pp. To appear in SIAM Journal on Computing.

RS-95-10 Dany Breslauer and Devdatt P. Dubhashi. Transforming Comparison Model Lower Bounds to the Parallel-Random-Access-Machine. February 1995. 11 pp.