1 Introduction

The category of locales provides an example of a category where exponentials do not always exist (not all locales are locally compact) but for which double exponentiation at the Sierpinski locale does always exist; the double exponential is given by the double power locale construction, [VT04]. This example motivates a broader question: what categorical conditions can we think of that establish that a monad is a double exponential monad, in the absence of an assumption of cartesian closedness on the ambient category? The double power locale monad has a strength and the category of locales is enriched over posets and has categorical tensors that are stable under finite product. Further, the proof that the double power locale functor is a double exponential seems, at the very least, to require this level of assumptions on the ambient category C and the structure of the monad. So the question becomes: when are enriched strong monads double exponential monads? This paper provides some categorical conditions that answer the question. We show that for any strong order enriched monad T we have that T is a double exponential monad [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] provided (i) A is a T-algebra, (ii) [A.sup.X] exists weakly and is given by categorical tensor; and, (iii) the contravariant functor C(_, A) is fully faithful.

The structure of the paper is as follows. In the next section we recall some results about categorical tensors, focusing on how when tensors exist they induce a monad on the category V over which our ambient category C is enriched. The following section discusses weak exponentials, and describes a condition for when weak exponentials are given by tensor. The next section proves the main result, showing that the categorical conditions just outlined are sufficient for a strong monad to be double exponential. The second to last section outlines how the result can be applied to prove that the double power locale monad is a double exponential monad. The last section provides a discussion on potential further work.

2 Order enriched categorical definitions and initial lemmas on tensors

Let C be a category enriched over another category V. We assume that V is a category with finite products and has 1 generating; that is, for any two morphisms c, d : D [??] E if ca = da for all a : 1 [right arrow] D then c = d. Any enrichment over V uses finite products in V as the monoidal structure. Consult B2.1 of [J02] for material on enriched categories; in particular we follow the notation [absolute value of C] for the underlying ordinary category of an enriched category C.

The definition of tensor for an object D of V and an object X of C, is an object D [R] X of C together with a map [i.sup.D.sub.X] : D [right arrow] C (X, D [cross product] X) such that for every Y and every morphism l : D [right arrow] C(X,Y) there is a unique map [x.sub.l] : D [cross product] X [right arrow] Y such that l factors as [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Put another way, (_) [cross product] X : V [right arrow] [absolute value of (C)] is left adjoint to C(X, _) : [absolute value of (C)] [right arrow] V. We use the notation e[v.sub.X,Y] for the map [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; i.e. the mate of the identity on C(X,Y). Below we will have a fixed object A as part of our assumptions; [D.sub.X] will be used as notation for C(X, A) and e[v.sub.X] for e[v.sub.X,A] : [D.sub.X] [cross product] X [right arrow] A.

Say C has finite products and tensors. Then for any pair [X.sub.1] and [X.sub.2] of objects of C there is a canonical map [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] given by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] where [l.sub.x] is the map

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Tensors are said to be stable under finite products provided this canonical map is always an isomorphism. Note that the condition is equivalent to the same condition restricted to [X.sub.1] = 1. Notice that the mate of

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is the same as the mate of

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

by definition of [PSI]. It follows that if tensors are stable under product then the diagram

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

commutes. Therefore every arrow X [right arrow] D [cross product] X in the image of [i.sup.D.sub.X] can be expressed as (a, Idx) '? X - D [R] X for some a : 1 [right arrow] D [cross product] 1. This will be exploited when we come to looking at natural transformations between functors of the form C(_ x X,A) : [absolute value of ([C.sup.op])] [right arrow] V.

Notice also that the following diagram commutes, provided tensors are stable under product:

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

This follows by unwinding the definitions of the various isomorphisms involved. By definition of tensor, for each object X of C, a monad [K.sub.X] is induced on V whose functor part is given by D [??] (X, D [cross product] X); this is the monad on V induced by the adjunction (_) [cross product] X [??] C(X, _). The last two diagrams show that provided tensors are stable under product, (_) x Idx induces a monad morphism from K(= [K.sub.1]) to [K.sub.X]. It follows that for any X and Y, C (X, Y) is a K algebra; its structure map is given by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Example 2.1. The category of sets, enriched over itself, is an example: X [cross product] Y is given by X x Y, from which it is clear that the tensor is stable under finite products.

Example 2.2. The category of locales, Loc, is enriched over Pos, the category of posets. It has tensors that are stable under products. For any poset P, monotone maps P [right arrow] Loc(X, Y) are in order preserving bijection with Loc(Idl(P) x X,Y), where Idl(P) is the locale whose frame of opens is the set of upper closed subsets of P. In other words P [cross product] X exists and is given by Idl(P) x X, from which it is clear that the tensor is stable under products. The monad induced on Pos is the ideal completion monad (its functor part sends each poset to its set of ideals; that is, lower closed and directed subsets). The category of algebras is therefore the category dcpo, of directed complete posets.

With these basic facts about tensor recalled and examples given, we can now progress with an initial lemma.

Lemma 2.3. Assume that C, enriched over V, has finite products and tensors that are stable under finite product. Then,

(a) for any objects X, Y and A of C, given any natural transformation [alpha] : C(_ x X, A) [right arrow] C(_ x Y,A),

(i) [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] A is equal to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]; and,

(ii) [[alpha].sub.1] is a K-algebra homomorphism.

(b) For any two natural transformations [alpha], [beta] : C(_ x X, A) [right arrow] C(_ x Y,A), [[alpha].sub.1] = [[beta].sub.1] if and only if [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Part (a)(ii) tells us that natural transformations Loc(_ x X,A) [right arrow] Loc(_ x Y, A) give rise to dcpo homomorphisms. Part (b) will be key to the proof of the main result.

Proof. (a)(i). By definition of tensor, a proof is needed that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is equal to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

Since 1 is generating, and every a : 1 [right arrow] [D.sub.X] factors as [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], the two arrows are equal because a is natural at each [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and, as observed above, [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] factors as [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

(a)(ii). We must check for any [phi] : 1 [right arrow] C(X, A) [cross product] 1, that

[[alpha].sub.1](e[v.sub.X]([phi] x I[d.sub.X])) = e[v.sub.Y](([[alpha].sub.1] [cross product] 1)[phi] x I[d.sub.Y])

The right hand side is equal to e[v.sub.Y] ([[alpha].sub.1] [cross product] I[d.sub.Y])([phi] x I[d.sub.Y]) and by (a)(i) this is equal to [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and so this stage of the proof follows by naturality at [phi].

One way round for (b) follows from (a)(i). For the other way round observe that for any natural transformation 7 : C(_ x X, A) [right arrow] C(_ x Y, A) and for any a : [right arrow] [D.sub.X], it is clear from naturality that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

3 Weak exponentials as tensors

If X and A are two objects of a category C, then a weak exponential [W.sup.[X,A]] is an object of C together with a map we[v.sub.X,A] : [W.sup.[X,A]] x X [right arrow] A such that for every map a : Z x X [right arrow] A there is a map [f.sub.a] : Z [right arrow] [W.sup.[X,A]] such that a factors as we[v.sub.X,A] ([f.sub.a] x I[d.sub.X]). In other words a weak exponential is the same thing as an exponential but without the uniqueness requirement placed on [f.sub.a]. For interest, note that if the definition of weak exponential was weakened to require the existence of [f.sub.a] only in the case Z = 1, then [D.sub.X] [cross product] 1 would always be a weak exponential [W.sup.[X,A]].

Weak exponentials are important in our context because in their presence the natural transformations that are of interest to us are uniquely determined by their actions on the weak evaluation map wev:

Lemma 3.1. If C is a category, with finite products, enriched over V and A an object of C such that [W.sup.[X,A]] exists for every X, then every natural transformation C(_ x X, A) [right arrow] C(_ x Y,A) is uniquely determined by [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

Proof. This is immediate from naturality and the definition of weak exponential (and our assumption that 1 generates V) because every a : Z x X [right arrow] A factors as we[v.sub.X,A]([f.sub.a] x I[d.sub.X]).

If C has tensors that are stable under products then we say that the weak exponential [W.sup.[X,A]], when it exists, is given by the tensor [D.sub.X] [cross product] 1 provided the map [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] A makes [D.sub.X] [cross product] 1 into a weak exponential. The next lemma provides some insight into the relationships between the various categorical statements that we are discussing:

Lemma 3.2. Let C be a category over V with finite products and tensors that are stable under product, and X and A two objects of C. Then C has weak exponentials [W.sup.[X,A]], given by the tensor [D.sub.X] [cross product] 1, if and only if for every object Z there exists a map [r.sub.Z] : [D.sub.z x X] [cross product] Z [right arrow] [D.sub.X] [cross product] 1 such that e[v.sub.X]([r.sub.Z] x I[d.sub.X]) = e[v.sub.Z x X]

Proof. Say [D.sub.X] [cross product] 1 is a weak exponential, then the [r.sub.Z] required exists for any Z, by applying the definition of weak exponential to e[v.sup.Z x X] : ([D.sub.Z x X] [cross product] Z) x X [right arrow] A.

In the other direction, say we are given a : Z x X [right arrow] A, then a must factor as e[v.sub.z x X]([p.sub.a], I[d.sub.Z x X]) for some [p.sub.a] : 1 [right arrow] [D.sub.Z x X] [cross product] 1. But then [r.sub.Z]([p.sub.a], I[d.sub.Z]) is the morphism required to prove that [D.sub.X] [cross product] 1 is a weak exponential.

It is well know that the category of locales has weak exponentials, [W.sup.[X,S]], given by tensor, Idl([D.sub.X]), where we are taking A = S, the Sierpinski locale, for C = Loc (and so for any locale X, [D.sub.X] [congruent to] OX, the opens of X). For example you can exploit the facts that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] and S is injective. The lemma can also be applied; since the opens of Z x X are in order preserving bijection with suplattice homomorphisms OX [right arrow] O[Z.sup.op] there is a forgetful monotone map from [D.sub.ZxX] [right arrow] Loc(Z, Idl([D.sub.X])), which defines a map [r.sub.Z] : Idl([D.sub.Z x X]) x Z [right arrow] Idl([D.sub.X]) for any locale Z.

4 Main result

Before we state and prove our main result, we must be clearer about what is meant by a double exponential monad. For objects X and A in C, [A.sup.X] does not necessarily exist in C as we are not making the assumption that C is cartesian closed. However, the presheaf C(_ x X, A) : [absolute value of ([C.sup.op])] [right arrow] V is the exponential C[(_,A).sup.C(_,X)] in the presheaf category [[absolute value of ([C.sup.op])], V]. So we can define the double exponential [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] to be an object of C with the property that morphisms p : [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] are (naturally in Y) in bijection with natural transformations from C(_ x X, A) to C(_ x Y, A). An enriched monad T = (T, [eta], [mu]) on an enriched category C is a double exponential monad with respect to an object A provided TX is a double exponential AaX, naturally in X, and under the bijections that this establishes the unit t/x is mapped to the identity natural transformation on C(_ x X, A) and the natural transformation C(_, [[mu].sub.X]) is [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], where [[??].sup.X] : C(_ x X,A) [right arrow] C(_ x TX, A) is the mate of the identity on TX.

If T is a double exponential monad, then a strength can be defined on it by defining, for any Z and X of C, [t.sub.Z,X] : Z x TX [right arrow] T(Z x X) to be the map corresponding to the natural transformation [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. C(_ x Z x TX, A). If T is a monad with a strength then it is a double exponential monad provided that also the strength is, up to isomorphism, that determined by the double exponential structure (i.e. determined by [[??].sup.X.sub.(_) x Z]).

Theorem 4.1. Let V be a finite product category with 1 generating and C a category enriched over V with tensors that are stable under product. Denote by K the monad on V induced by the assumption that C has tensors (i.e. its functor part is D [??] (1, D [cross product] 1)).

Let A be an object of C such that for any object X of C the weak exponential W[X,A] exists and is given by tensor. Then for any strong V-monad T on C, we have that T is isomorphic to the double exponential monad induced by A provided

(i) A is a T-algebra; and,

(ii) the functor [U.sub.A] : [absolute value of ([C.sub.T])] [right arrow] [([V.sup.K]).sup.op] given by [U.sub.A](X) = C(X,A) is full and faithful.

For clarity we note that the functor [U.sub.A] is a contravariant functor from the underlying ordinary category of the Kleisli category determined by T to the category of algebras on V induced by the tensor. It is given by

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

where a : TA [right arrow] A is the structure map on A. That this is well defined is clear from earlier lemmas (to see that aT(_)f is a K algebra homomorphism, observe that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII] determines a natural transformation with [[alpha].sub.1] = aT(_)f and apply Lemma 2.3 (a) (ii)).

Proof. We start with a proof that for any objects X and Y of C, morphisms p : Y [right arrow] TX are in bijection with the collection of natural transformations from C(_ x X,A) to C(_ x Y,A).

For every object X of C, consider the functor [F.sub.X] : [absolute value of (C)] [right arrow] [absolute value of ([C.sub.T])] that sends Z to Z x X on objects and sends a morphism [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. Clearly C(_ x X, A) = [U.sub.A][F.sub.X].

Given p : Y [right arrow] TX, define [[alpha].sup.p] : [F.sub.Y] [right arrow] [F.sub.X] by defining [[alpha].sup.p.sub.Z] to be the composite

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII],

where t is the strength on T. By exploiting the fact that the strength [t.sub.Z,X] is natural in Z, it can be checked that [[alpha].sup.p] is a natural transformation and so gives rise to a natural transformation [[beta].sup.p] [equivalent to] [U.sub.A]([[alpha].sup.p]) from C(_ x X, A) to C(_ x Y,A). By exploiting the fact that [t.sub.1,X] is (canonically isomorphic to) the identity on TX (by definition of strength) we see that [[alpha].sup.p.sub.1] = p.

On the other hand given a natural transformation [beta] from C(_ x X, A) to C(_ x Y, A), we know by part (a)(ii) of Lemma 2.3 that [[beta].sub.1] is a K-algebra homomorphism and so by assumption there is some [p.sub.[beta]] : Y [right arrow] TX such that [U.sub.A] ([p.sub.[beta]]) = [[beta].sub.1]. By combining (b) of Lemma 2.3 and Lemma 3.1 we know that f is uniquely determined by f 1 and so as we have assumed that [U.sub.A] is faithful, a bijection is established between morphisms Y [right arrow] TX and natural transformations C(_ x X, A) to C(_ x Y,A). For clarity we note that given p : Y [right arrow] TX, then the corresponding natural transformation, fiP, sends any b : Z x X [right arrow] A to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

It is then clear that the bijection is natural in Y and further that the mate of [[eta].sub.X] : X [right arrow] TX must be the identity natural transformation, this last by exploit ing the fact that [[eta].sub.Z x X] must factor as [t.sub.Z,X](I[d.sub.Z] x [[eta].sub.X]) for any Z, by definition of strength. To see that the bijection is natural in X, say we are given g : [X.sub.1] [right arrow] [X.sub.2], then it must be checked for any p : Y [right arrow] T[X.sub.1] and any b : Z x [X.sub.2] [right arrow] A that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is equal to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

which follows by naturality of [t.sub.Z,X] at X.

We also must have that C(_, [[mu].sub.X]) is [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII], up to the bijections established.

To see this it can be checked that for any p : Y [right arrow] TTX that [MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]. for any b : Z x X [right arrow] A that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is equal to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII].

This can be seen by exploiting the facts that aTa = a[[mu].sub.A], [mu] is natural (at b) and that [[mu].sub.Z x X](T[t.sub.Z,X])[t.sub.Z,TX] = [t.sub.Z,X]([d.sub.Z] x [[mu].sub.X]), by definition of strength.

Finally, the strength t of T must be shown to be that induced by the double exponential structure. Say we are given b : [Z.sub.1] x Z x X [right arrow] A, then it must be checked that

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

is equal to

[MATHEMATICAL EXPRESSION NOT REPRODUCIBLE IN ASCII]

which is clear from the definition of strength.

5 Application

The double power locale monad, P, was initially defined as the composite, in either order, of the lower and the upper power locale monad, [JV91]. It does not matter which order is taken because the upper and lower power locale monads commute with each other. If x is a locale then the frame of opens of the double power locale PX, is given by the free frame on OX, keeping the dcpo structure on OX fixed. Notice then that S [congruent to] P0 because the frame of opens of S is the free frame on the singleton set 1 (and the frame of opens of the zero locale is the singleton set). So S is a P-algebra.

Both the lower and upper power locale monads have strengths; this can be seen by exploiting the fact that locale product can be given by either suplattice or preframe tensor. Therefore the double power locale monad has a strength as it is easy to check that the composition of any two commuting monads, both with a strength, has a strength. It is clear that [U.sub.S] : [Loc.sub.P] [right arrow] [Pos.sup.op] is the functor that sends a morphism Y [right arrow] PX to its corresponding dcpo homomorphism; it is therefore faithful. Equally any dcpo homomorphism OX [right arrow] OY arises in this way and so we have checked all the conditions of our main theorem and can conclude that P is a double exponential monad.

6 Discussion

That the double power locale monad is a double exponential monad was originally shown in [VT04]. The proof offered here, it is hoped, provides some insight into categorical techniques that can be deployed to obtain the result. Trivially the main result can be applied to cartesian closed categories, so the challenge of finding non-trivial applications is finding categories that are not cartesian closed but for which double exponentiation does exist (for some object A). Aside from Loc the author has been unable to think of any; the relationship between the monad induced on the category V and the points of the double power locale monad seems to be quite particular. To take these ideas further one instinct is to tamper with Pos; for example, the points of the lower and upper power locales are natural transformations between functors [Loc.sup.op] [right arrow] SLat, where SLat is the category of semilattices. But this fails then to be double exponentiation because the Yoneda lemma does not embed Loc into [[Loc.sup.op], SLat]. On the other hand if the situation is unique, perhaps it is characterizing Loc? Indeed the category of locales is the opposite of the category of order internal distributive lattices in the category dcpo; is it possible for a category to be the category of internal distributive lattices on the category of algebras of its enrichment (and to have double exponentiation) without this somehow forcing it to be Loc? The challenge in this idea seems to be in proving that the enrichment is necessarily Pos.

Another avenue is to see whether the categorical techniques offered here can be deployed to provide a result about indexed categories, with V the base category. This idea is plausible because the double power locale monad is double exponentiation relative to any topos [epsilon], but a direct application of the result offered here is not possible because 1 is not generating in the category of posets relative to an arbitrary topos [epsilon]. The author hopes to make an indexed version of our main result the topic of a follow up paper.

Received by the editors in April 2015--In revised form in February 2016.

Communicated by E. Colebunders.

2010 Mathematics Subject Classification : 06D22,18D, 18D20.

6.1 Acknowledgement

This paper is dedicated to my daughter, Hannah Townsend.

References

[J02] Johnstone, P.T. Sketches of an elephant: A topos theory compendium. Vols 1, 2, Oxford Logic Guides 43, 44, Oxford Science Publications, 2002.

[JV91] Johnstone, P.T., and Vickers, S.J. "Preframe presentations present", in Carboni, Pedicchio and Rosolini (eds) Category Theory--Proceedings, Como, 1990 (Springer Lecture Notes in Mathematics 1488,1991), 193-212.

[VT04] Vickers, S.J. and Townsend, C.F. A Universal Characterization of the Double Power Locale. Theoretical Computer Science 316 (2004) 297-321.

8, Gordon Villas, Aylesbury Road, Tring, HERTS HP23 4DJ, U.K.

Email: info@christophertownsend.org