Properly injective spaces and function spaces - School of
Transcript Of Properly injective spaces and function spaces - School of
Properly injective spaces and function spaces
Mart´ın H¨otzel Escard´o∗
To appear in Topology and Its Applications
Version of Monday 22 nd September 1997
Abstract Given an injective space D (a continuous lattice endowed with the Scott topology) and a subspace embedding j : X → Y , Dana Scott asked whether the higher-order function [X → D] → [Y → D] which takes a continuous map f : X → D to its greatest continuous extension f¯ : Y → D along j is Scott continuous. In this case the extension map is a subspace embedding. We show that the extension map is Scott continuous iff D is the trivial one-point space or j is a proper map in the sense of Hofmann and Lawson. In order to avoid the ambiguous expression “proper subspace embedding”, we refer to proper maps as finitary maps. We show that the finitary sober subspaces of the injective spaces are exactly the stably locally compact spaces. Moreover, the injective spaces over finitary embeddings are the algebras of the upper power space monad on the category of sober spaces. These coincide with the retracts of upper power spaces of sober spaces. In the full subcategory of locally compact sober spaces, these are known to be the continuous meet-semilattices. In the full subcategory of stably locally compact spaces these are again the continuous lattices. The above characterization of the injective spaces over finitary embeddings is an instance of a general result on injective objects in poset-enriched categories with the structure of a KZ-monad established in this paper, which we also apply to various full subcategories closed under the upper power space construction and to the upper and lower power locale monads. The above results also hold for the injective spaces over dense subspace embeddings (continuous Scott domains). Moreover, we show that every sober space has a smallest finitary dense sober subspace (its support). The support always contains the subspace of maximal points, and in the stably locally compact case (which includes densely injective spaces) it is the subspace of maximal points iff that subspace is compact. Keywords and phrases: Injective spaces, function spaces, proper maps, lower and upper power spaces, stably locally compact spaces, subspaces of maximal points, locales, continuous lattices, continuous Scott domains, domain theory, KZ-monads, Kan extensions. Mathematics subject classification: 06B35, 54C20, 54C35, 18C20.
∗Department of Computing, Imperial College, 180 Queen’s Gate, London SW7 2BZ, United Kingdom, e-mail: [email protected], url: http://theory.doc.ic.ac.uk/people/Escardo.
1
1 Introduction
Although the fundamental rˆole of injective spaces in the mathematical theory of computation was emphasized by Dana Scott in his seminal papers [33] and [35], injective spaces have been neglected in the subsequent development of the theory (but see [30, 15]). In this section we recall their rˆole and raise questions related to function spaces and higher-order functions which are answered in the technical development that follows. We also briefly discuss applications, introduce preliminary background and give a summary of the main results of this paper.
1.1 Embedding spaces into domains
In applications of domain theory [2] to denotational semantics [16, 13] and integration [8, 11], one starts by implicitly or explicitly embedding given spaces X, Y , Z, . . . into appropriate domains C, D, E, . . . endowed with the Scott topology. One of the simplest examples is given by the embedding of the discrete space of natural numbers into the so-called flat domain N⊥ of natural numbers [36, 29, 31]. A slightly more elaborate example is given by the embedding of (the one-point compactification of) the discrete space of natural numbers into the so-called domain of lazy natural numbers [16, 2]:
2
nq d
... q ∞
1q dqdqd... q n
0q ddq 2 ddq 1
0
The choice of domains depends, among other things, on the model of computation on the space. For example, the flat and lazy domains of natural numbers respectively capture callby-value and call-by-name evaluation of the successor map [16].
More sophisticated examples of such embeddings include: the Euclidean real line into the domain of compact real intervals ordered by reverse inclusion [34, 13, 10], the same space into the ideal completion of the rational basis of the interval domain, or a similar algebraic domain [14], Cantor space 2ω into the domain 2∞ = 2∗ ∪ 2ω of finite and infinite sequences ordered by prefix [31, 43, 39] (similarly, Baire space Nω into the domain N∞), the space of total functions N → N endowed with the compact-open topology (another version of Baire space) into the domain of partial functions ordered by graph inclusion [36, 31], any second countable T0 space into the domain Pω of subsets of natural numbers ordered by inclusion [35], any second countable T0 space as an isochordal subspace (see below for the definition) of T ω, where T is the flat domain T⊥ of truth values [30], any locally compact Hausdorff space into its upper power space [9], any Polish space onto the subspace of maximal points of a continuous dcpo (directed complete poset) [25, 12].
1.2 Injective spaces
Given embeddings of spaces X and Y into computational models C and D, we model continuous maps X → Y by Scott continuous functions C → D. Therefore it is natural to demand that the continuous functions C → D capture the continuous maps X → Y , in the sense that every continuous map of the latter kind (co)extends to a continuous function of the former kind. Since every continuous map f : X → Y trivially coextends to a continuous
2
map f : X → D, we only need to consider extensions of continuous maps f : X → D to continuous functions f¯ : C → D. This brings us to the subject of injective spaces.
A space D is injective in the ambient category of T0 spaces if every continuous map f : X → D extends to a continuous map f¯ : Y → D, for any space Y containing X as a subspace [33, page 99], as illustrated in the diagram below:
X⊂
j EY
dd
.....¯..
f d © f
D
where j : X → Y is the inclusion. (Notice that in principle there is nothing canonical about f¯.)
A main result in loc. cit. is the characterization of the injective spaces as the continuous lattices endowed with the Scott topology. For example, by the previous discussion, the continuous endomaps of the continuous lattice Pω capture the continuous maps between any two second countable T0 spaces [35, page 527].
If one restricts subspace to dense subspace in the definition, one speaks of densely injective spaces, which are characterized as the continuous Scott domains [15, page 127] (that is, continuous dcpos with least upper bounds of bounded subsets). A continuous Scott domain fails to be a continuous lattice only by lacking a (compact) top element [15, pages 52–53] and the continuous Scott domains coincide with the closed subspaces of the continuous lattices [15, page 109]. The examples of embeddings given above, except for the ones into the ideal completion of the rational intervals, Pω and T ω, and the ones about Polish spaces, are instances of dense embeddings into continuous Scott domains. In fact, these are examples of dense embeddings of Hausdorff spaces onto subspaces of maximal points of continuous Scott domains.
Gordon Plotkin [30, page 233] calls a subspace inclusion X ⊆ Y isochordal if for any two disjoint open sets U, U ⊆ X there are disjoint open sets V, V ⊆ Y with V ∩ X = U and V ∩ X = U . For example, every dense embedding is isochordal.
If one restricts subspace to isochordal subspace in the definition, one speaks of isochordally injective spaces. Plotkin [30, pages 233–234] characterized the second countable isochordally injective spaces as the countably based coherently complete domains (that is, countably based continuous dcpos in which every pairwise bounded subset has a least upper bound). A result by Paul Taylor [40, 2.5.4 and 2.6.4b] implies that the countability hypothesis is not necessary. An example of isochordal embedding into a coherently complete domain which is not a dense embedding is given by the embedding of the real line into the ideal completion of the compact rational intervals ordered by reverse inclusion, defined by x → {[p, q]|p < x < q}.
More generally, if in the definition j ranges over a given class J of embeddings, then one speaks of injective spaces over J [15, page 121].
1.3 Injective spaces and function spaces
By the above discussion, if j : X → C and k : Y → D are subspace embeddings into injective spaces, then the continuous functions C → D capture the continuous maps X → Y in the sense of the (co)extension property. When one considers higher-order maps [X → Y ] → Z, such as the integration and supremum operators discussed in [11], one is led to consider the
3
case in which the function space [C → D] captures the the function space [X → Y ], in the
stronger sense of having it embedded as a subspace, via some continuous (co)extension map
[X → Y ] → [C → D]. By the above remarks, it suffices to consider continuous extension
maps [X → D] → [C → D]. Although in principle there is nothing canonical about the extended map f¯ in the definition
of injective space, this turns out to be the case. In fact, Scott [33, page 116] showed that if D is
injective and j : X → Y is a subspace embedding, then every continuous map f : X → D has
a greatest continuous extension along j, which will be convenient to denote by f /j : Y → D,
given by
f /j(y) = ↑
f j−1(V ) .
y∈V ∈ΩY
Here hom-sets are ordered by the pointwise ordering induced by the specialization order of the target space and ΩY is the frame of open sets of Y .
Having established this result, Scott asked whether the greatest-extension map f → f /j is Scott continuous (very much doubting that this would be the case in general). Here [X → D] and [Y → D] are endowed with the Scott topology, which coincide with the Isbell topology if X and Y are exponentiable [26, page 154] (which further coincide with the compact-open topology if X and Y are locally compact [23, page 61]). Since the greatest-extension map is a right inverse of the restriction map g → g ◦ j, which is always Scott continuous, the greatest-extension map is a subspace embedding iff it is Scott continuous, and in this case [X → D] is a retract of [Y → D].
We show that the greatest-extension map f → f /j is Scott continuous iff D is the trivial one-point space or j is a proper map in the sense of Hofmann and Lawson [18, page 154]. Briefly, a continuous map j : X → Y is proper if the right adjoint ∀j : ΩX → ΩY of its associated frame map Ωj : ΩY → ΩX defined by Ωj(V ) = j−1(V ) is Scott continuous.
The terminology “proper” has been used in several slightly distinct senses in the literature1 – see e.g. [4, pages 97–107] [20, page 104] [41] and the remarks by Johnstone [20, page 121] and Vickers [42, Section 5]. To make things worse, in our case we have the unfortunate ambiguity of the expression “proper subspace embedding”, which can mean either an embedding onto a proper subspace or an embedding which is a proper map in the sense just defined. We have therefore decided to refer to the proper maps in the sense of Hofmann and Lawson as finitary maps and to the subspaces whose inclusion map is finitary as finitary subspaces. The terminology “finitary” is borrowed from Banaschewski [3, page 649], who calls a nucleus on a locale finitary if it is Scott continuous, and it is justified by the fact that a subspace embedding is finitary iff its induced nucleus is finitary.
In view of the above result on injective spaces and finitary embeddings, we are led to investigate the finitary subspaces of injective spaces. More concrete characterizations of the notions of finitary map and finitary subspace are given in the technical development that follows this introduction. For the time being, we remark that the finitary sober subspaces of a (densely) injective space D are the sober subspaces X such that Q ∩ X is compact for every compact saturated set Q ⊆ D. Also, the finitary sober subspaces of the (densely) injective spaces are exactly the stably locally compact spaces. This is a consequence of more general results, including the following.
In the ambient category of sober spaces, the full subcategories of respectively compact, locally compact, spectral and stably locally compact spaces are closed under the formation
1If X and Y are Hausdorff spaces then all definitions are equivalent.
4
of finitary subspaces. Here we don’t assume the Hausdorff separation axiom in the definition of compactness; a space is compact iff it satisfies the Heine-Borel property. Stably locally compact spaces are considered in [20, page 313] [17] [38]. Such spaces are called coherent in [2], but Johnstone [20, page 63] calls coherent the spaces which Vickers [43, page 120] and Smyth [39, page 649] call spectral.
Also, in this ambient category, for every subspace X of a space Y there is a smallest finitary subspace X¯ of Y containing X as a subspace, which we refer to as the finitary hull of X. Moreover, every space has a smallest finitary dense subspace (its support), which is the finitary hull of its subspace of maximal points. In the stably locally compact case, the support is the subspace of maximal points iff that subspace is compact.
The above results hold in the more general category of locales. Moreover, the full subcategory of locales with enough points is closed under the formation of finitary sublocales. Also, the smallest finitary dense sublocale of a locale is the finitary hull of its smallest dense sublocale.
1.4 Injective spaces and upper power spaces
Having established that the “good denominators” are the finitary subspace embeddings, one wonders what the finitarily injective spaces are. We show that they are precisely the algebras of the upper power space monad in the category of sober spaces (considering the empty set as a point of the upper power space construction), which coincide with the retracts of upper power spaces of sober spaces. Moreover, greatest extensions exist and are given by
f /j(y) = f j−1(↑y) .
The full subcategory of locally compact sober spaces is closed under the upper power space construction. The finitarily injective spaces in this subcategory are the continuous meetsemilattices with unit, by virtue of the characterization of the algebras given in [32, pages 135 and 140]. The full subcategory of stably compact spaces is also closed under the upper power space construction. In this subcategory, the finitarily injective spaces are again the continuous lattices.
1.5 Injective spaces and KZ-monads
The above characterization of the finitarily injective spaces is a particular case of a more general result on KZ-monads [24] on poset-enriched categories established in the present paper. Moreover, this result is applied to the lower and upper power locale monads discussed in [32] (see below). If the underlying functor of the monad is Scott continuous on hom-posets (which is the case in our applications), the extension map is also Scott continuous, so that we don’t lose the continuity of the extension map along finitary embeddings when we consider the larger class of finitarily injective spaces.
1.6 Injective spaces and lower power spaces
In applications of domain theory (see e.g. Scott [35, page 528] and Plotkin [31, page 14]), one sometimes wishes to consider least extensions. We show that the least continuous extension along a subspace embedding j : X → Y of an injective-valued map f : X → D exists iff D is trivial or j is semiopen, in the sense that its associated frame map Ωj : ΩY → ΩX has a
5
left adjoint ∃j : ΩX → ΩY . The process of taking least continuous extensions is always Scott continuous, essentially because ∃j, being a left adjoint, preserves all joins.
By an application of the general result on KZ-monads and a result by Steve Vickers [42, Proposition 4.6], we conclude that the injective locales over semiopen embeddings are the algebras of the lower power locale monad. It is plausible the same result holds for the injective spaces over semiopen embeddings, but we don’t pause to check whether this is the case.
1.7 Injective spaces and Kan extensions
By definition, f /j is the greatest continuous map g : Y → D such that g ◦ j = f . Scott [33, page 116] remarked that f /j is in fact the greatest continuous map g such that g ◦ j ≤ f . This shows that f /j is the right Kan extension of f along j. The general definition of a Kan extension of a functor can be found in [7, page 39] and [27, page 232], and its specialization to a monotone map can be found in [1, page 22]. In this paper we consider Kan extensions of arrows of poset-enriched categories.
By virtue of Scott’s remark, D is injective iff for every subspace embedding j : X → Y the restriction map g → g ◦ j : hom(Y, D) → hom(X, D) has an injective right adjoint f → f /j : hom(X, D) → hom(Y, D). We make this characterization into a definition of right injective object in a poset-enriched category. By omitting the injectivity condition on the right adjoint, we obtain a definition of right Kan object; this means that in general we only have (f /j) ◦ j ≤ f . Similarly, we obtain definitions of left Kan and left injective objects.
We show that every injective space over subspace embeddings is a right Kan space over arbitrary continuous maps. Similarly, every right injective space over finitary embeddings is a right Kan space over arbitrary finitary maps, and every left injective locale over semiopen embeddings is a left Kan locale over arbitrary semiopen maps.
1.8 Injective spaces and dense embeddings
The above results on greatest extensions and continuity of the extension map generalize to densely injective spaces. Also, the injective spaces over finitary dense embeddings are characterized via an application of the above result on KZ-monads to the upper power space monad without the empty set as a point of the upper power space construction.
1.9 Injective spaces and isochordal embeddings
Unfortunately, the isochordally injective spaces fail to enjoy both the least- and greatestextension properties, as simple counter-examples which can be safely left to the reader show.
2 Kan objects in poset-enriched categories
2.1 Poset-enriched categories
A poset-enriched category is a category whose hom-sets are posets and whose composition operation is monotone. A poset-functor between poset-enriched categories is a functor which is monotone on hom-posets. A poset-functor F : X → A is poset-faithful if Uf ≤ Ug in A implies f ≤ g in X.
6
The main example of a poset-enriched category is Poset, the category of posets and monotone maps with hom-sets ordered pointwise. If X is any category and U : X → Poset is a faithful functor, then there is a unique way of making X into a poset-enriched category so as to also make U into a poset-faithful functor, given by the definition
f ≤ g in X iff Uf ≤ Ug in Poset,
because one direction of the definition is equivalent to saying that U is a poset-functor and the other is equivalent to saying that U is poset-faithful.
Our main example of such a situation is given by the category Sp0 of T0 topological spaces and continuous maps with U the specialization-order functor. The specialization order [15, page 123] [20, page 45] on the points of a space X is defined by x ≤ y iff every neighborhood of x is a neighborhood of y iff x belongs to the closure of {y}. This definition makes ≤ into a reflexive and transitive relation, which is antisymmetric iff X is T0. Also, it is clear from the definition that any continuous map preserves this preorder. Then the functor in question sends a T0 space to its set of points ordered by the specialization order, and a continuous map to itself. Thus, the induced poset-enrichment in Sp0 is given simply by f ≤ g in hom(X, Y ) iff f (x) ≤ g(x) for all x ∈ X.
Definition 2.1.1 Let X be a poset-enriched category, I be any category, F : I → X be a functor, and P ∈ X be a limit of F with projections {πi : P → Fi}i∈I. Then there is a bijection between the set of cones under X and the set hom(X, P ), which sends the cone {gi : X → Fi}i∈I to the unique g : X → P such that gi = πi ◦ g for all i ∈ I. We say that the given limit is a poset-limit if the above bijection is an order-isomorphism for each X, where cones under X are ordered by {gi : X → Fi}i∈I ≤ {hi : X → Fi}i∈I iff gi ≤ hi for all i ∈ I.
This notion is a particular case of the general notion of V-limit in a V-enriched category, which can be found in e.g. [7, page 7].
All limits in Poset are poset-products, and the same holds for Sp0, poset-enriched as above, because the specialization-order functor U : Sp0 → Poset preserves limits.
2.2 Adjunctions between objects of poset-enriched categories
For a complete account to adjunctions between posets the reader is referred to [15] or [2]. In this subsection we fix terminology and basic facts about adjunctions between objects of poset-enriched categories.
An adjunction between objects X and Y of a poset-enriched category is a pair of arrows l : X → Y and r : Y → X such that l ◦ r ≤ idY and idX ≤ r ◦ l. Such an adjunction is denoted by l r, and l and r are said to be respectively left and right adjoint to each other. In an adjunction l r, each adjunct l and r is uniquely determined by the other.
An adjunction l r is reflective if l ◦ r = idY , and it is coreflective if idX = r ◦ l. A poset-functor F preserves adjunctions in the sense that l r implies Fl Fr; moreover, if F is poset-faithful then it reflects adjunctions in the sense that l r whenever Fl Fr.
Adjunctions compose in the sense that if l : X → Y , l : Y → Z, r : Y → X and r : Z → Y are arrows with l r and l r , then l ◦ l r ◦ r .
7
2.3 Kan extensions of arrows of poset-enriched categories
We first briefly specialize the definition of Kan extension [7, page 39] [27, page 232] from functors to monotone maps (cf. [1, page 22]), and then we consider its (immediate) generalization to arrows of poset-enriched categories.
Let j : X → Y and f : X → D be monotone maps between posets. A right Kan extension of f along j is a monotone map f /j : Y → D such that
(Kan1) (f /j) ◦ j ≤ f
(Kan2) g ◦ j ≤ f for g : Y → D implies g ≤ f /j.
Inequality (Kan1) is illustrated in the following diagram:
X
j EY
dd ≥ f d © f /j
D
Dually, we obtain the definition of left Kan extension by reversing the inequalities. We denote the left Kan extension of f along j by f \j whenever it exists.
By definition, the right Kan extension of f along j, if it exists, is the greatest map g : Y → D such that g ◦ j ≤ f . This is equivalent to saying that for all g : Y → D,
g ◦ j ≤ f iff g ≤ f /j,
which shows that right Kan extensions along a fixed j : X → Y exist for all f : X → D iff the composition map
g → g ◦ j : hom(Y, D) → hom(X, D)
has a right adjoint
f → f /j : hom(X, D) → hom(Y, D).
In [7] and [27], f /j and f \j are denoted by Ranjf and Lanjf respectively. Our notation makes the basic properties of Kan extensions easier to remember, because they resemble the properties of quotients (cf. Theorem 2.3.3 below).
The above definition formally applies to arrows between objects of poset-enriched categories. Before considering this generalization, we consider some basic properties which make sense only for monotone maps between posets. Proposition 2.3.1 and 2.3.2 are obtained by specializing the corresponding results in loc. cit. from functors to monotone maps.
Kan extensions generalize adjunctions, as Proposition 2.3.1, Theorem 2.3.4 and Corollary 2.3.5 below show:
Proposition 2.3.1 A monotone map f : X → D has a right Kan extension along a monotone map j : X → Y if the set f (j−1(↑y)) has a meet in D for each y ∈ Y , and in this case
it is given by f /j(y) = f j−1(↑y) .
An order-embedding [5, page 10] is a monotone map j : X → Y which reflects order in the sense that j(x) ≤ j(x ) implies x ≤ x . The following proposition shows that the right Kan extension f /j is an actual extension if j is an order-embedding:
8
Proposition 2.3.2 If j : X → Y is an order-embedding and f : X → D is a monotone map with a right Kan extension along j, then (f /j) ◦ j = f.
We now prove the facts that generalize to Kan extensions of arrows of poset-enriched categories.
Theorem 2.3.3 Let j : X → Y , k : Y → Z, f : X → D, and r : D → E be arrows of a poset-enriched category. Then the following properties hold whenever the right Kan extensions f /j, (f /j)/k and f /(k ◦ j), f /f and (r ◦ f )/j exist:
1. f /idX = f ,
2. (f /j)/k = f /(k ◦ j),
3. idD ≤ f /f = (f /f ) ◦ (f /f ) (if idD = f /f then f is said to be codense [27, page 242]),
4. r ◦ (f /j) ≤ (r ◦ f )/j, equality holding if r has a left adjoint.
These (in)equations are illustrated in the following diagrams:
X
idX
EX
X
j EY
k EZ
d df d = f d © X
d d≥ fd d
f /j ≥ (f /j)/k = f /(k ◦ j)
c© D
Xf
d df d ≥ d © D
ED f /f ≥ idD
X
j
EY
ed
¡
e df ed
≥ f /j
¡ ¡
e d © ¡
r ◦ fee=e D ≤¡¡(¡r ◦ f )/j
e
¡
e r¡
e¡
e c¡
E
Proof (1): Trivial. (2): By two applications of (Kan1), ((f /j)/k) ◦ k ◦ j ≤ (f /j) ◦ j ≤ f . By (Kan2), (f /j)/k ≤ f /(k ◦ j). In the other direction, (f /(k ◦ j)) ◦ k ◦ j ≤ f by (Kan1). By two applications of (Kan2), f /(k ◦ j) ≤ (f /j)/k.
(3): Since idD ◦ f ≤ f , we conclude that idD ≤ f /f by (Kan2). By monotonicity of composition, f /f ≤ (f /f ) ◦ (f /f ). In the other direction, (f /f ) ◦ (f /f ) ◦ f ≤ (f /f ) ◦ f ≤ f by two applications of (Kan1). Therefore (f /f ) ◦ (f /f ) ≤ f /f by (Kan2).
(4): r ◦ (f /j) ◦ j ≤ r ◦ f by (Kan1). Therefore r ◦ (f /j) ≤ (r ◦ f )/j by (Kan2). In order to establish the inequality in the other direction, assume that r has a left adjoint l. By (Kan1), ((r ◦ f )/j) ◦ j ≤ r ◦ f . By composing with l on the left and using the fact that l ◦ r ≤ idY , l ◦ ((r ◦ f )/j) ◦ j ≤ l ◦ r ◦ f ≤ f . Hence l ◦ ((r ◦ f )/j) ≤ f /j by (Kan2). By composing with r on the left, r ◦ l ◦ ((r ◦ f )/j) ≤ r ◦ (f /j). But idX ≤ r ◦ l. Therefore (r ◦ f )/j ≤ r ◦ (f /j).
9
Item (4) generalizes [33, Lemma 3.9], whose statement amounts to the equation j ◦ (g/e) = (j ◦ g)/e, from greatest extensions to right Kan extensions (and from coreflective adjunctions to adjunctions).
Theorem 2.3.4 Let l : Y → X and r : X → Y be arrows of a poset-enriched category.
1. If l r then every arrow f : X → D has a right Kan extension along r given by f /r = f ◦ l. In particular, l = idX /r.
2. If idX and r have right Kan extensions along r and r ◦ (idX /r) = r/r, then idX /r r. Proof (1): f ◦ l ◦ r ≤ f because l ◦ r ≤ idX by definition of adjunction. This establishes (Kan1). Assume that g ◦ r ≤ f for g : Y → D. Since g ◦ r ◦ l ≤ f ◦ l and since idY ≤ r ◦ l by definition of adjunction, we conclude that g ≤ f ◦ l. This establishes (Kan2). The particular case follows by taking D = X and f = idX .
(2): By (Kan1), (idX /r)◦r ≤ idX . This establishes one half of the adjunction. Since r/r ≥ idY by Theorem 2.3.3(3), we conclude that r ◦ (idX /r) ≥ idY by the hypothesis and transitivity, which establishes the other half. Therefore idX /r r.
Corollary 2.3.5 The arrow r : X → Y has a left adjoint iff idX and r have a right Kan extension along r and the condition r ◦ (idX /r) = r/r holds, and in this case it is idX /r. Proof If l r then r ◦ (idX /r) = r ◦ (idX ◦ l) = r ◦ l = r/r by Theorem 2.3.4(1). The converse is Theorem 2.3.4(2).
2.4 Kan objects in poset-enriched categories
Let X be a poset-enriched category and J be any subcategory of X. Definition 2.4.1 Let D be an object of X.
1. D is a right Kan object over J if for each j : X → Y in J the composition map
◦j : hom(Y, D) → hom(X, D)
has a right adjoint also denoted by RanDj .
/j : hom(X, D) → hom(Y, D),
2. D is a right injective object over J if in addition the right adjoint is an injective function, which means that the right Kan extension f /j is an actual extension, in the sense that (f /j) ◦ j = f .
Left Kan objects and left injective objects are defined dually (at the level of hom-posets), and left-Kan-extension maps are denoted by LanDj .
Let X/J denote the subcategory of X consisting of right Kan objects over J and right adjoints between them. The following is a corollary of Theorem 2.3.3:
Proposition 2.4.2 The equations
Ran(X, D) = hom(X, D) Ran(j : X → Y, r : D → E) = f → r ◦ f /j : hom(X, D) → hom(Y, E)
define a functor Ran : J × X/J → Poset. Notice that RanDj = Ran(j, idD).
10
Mart´ın H¨otzel Escard´o∗
To appear in Topology and Its Applications
Version of Monday 22 nd September 1997
Abstract Given an injective space D (a continuous lattice endowed with the Scott topology) and a subspace embedding j : X → Y , Dana Scott asked whether the higher-order function [X → D] → [Y → D] which takes a continuous map f : X → D to its greatest continuous extension f¯ : Y → D along j is Scott continuous. In this case the extension map is a subspace embedding. We show that the extension map is Scott continuous iff D is the trivial one-point space or j is a proper map in the sense of Hofmann and Lawson. In order to avoid the ambiguous expression “proper subspace embedding”, we refer to proper maps as finitary maps. We show that the finitary sober subspaces of the injective spaces are exactly the stably locally compact spaces. Moreover, the injective spaces over finitary embeddings are the algebras of the upper power space monad on the category of sober spaces. These coincide with the retracts of upper power spaces of sober spaces. In the full subcategory of locally compact sober spaces, these are known to be the continuous meet-semilattices. In the full subcategory of stably locally compact spaces these are again the continuous lattices. The above characterization of the injective spaces over finitary embeddings is an instance of a general result on injective objects in poset-enriched categories with the structure of a KZ-monad established in this paper, which we also apply to various full subcategories closed under the upper power space construction and to the upper and lower power locale monads. The above results also hold for the injective spaces over dense subspace embeddings (continuous Scott domains). Moreover, we show that every sober space has a smallest finitary dense sober subspace (its support). The support always contains the subspace of maximal points, and in the stably locally compact case (which includes densely injective spaces) it is the subspace of maximal points iff that subspace is compact. Keywords and phrases: Injective spaces, function spaces, proper maps, lower and upper power spaces, stably locally compact spaces, subspaces of maximal points, locales, continuous lattices, continuous Scott domains, domain theory, KZ-monads, Kan extensions. Mathematics subject classification: 06B35, 54C20, 54C35, 18C20.
∗Department of Computing, Imperial College, 180 Queen’s Gate, London SW7 2BZ, United Kingdom, e-mail: [email protected], url: http://theory.doc.ic.ac.uk/people/Escardo.
1
1 Introduction
Although the fundamental rˆole of injective spaces in the mathematical theory of computation was emphasized by Dana Scott in his seminal papers [33] and [35], injective spaces have been neglected in the subsequent development of the theory (but see [30, 15]). In this section we recall their rˆole and raise questions related to function spaces and higher-order functions which are answered in the technical development that follows. We also briefly discuss applications, introduce preliminary background and give a summary of the main results of this paper.
1.1 Embedding spaces into domains
In applications of domain theory [2] to denotational semantics [16, 13] and integration [8, 11], one starts by implicitly or explicitly embedding given spaces X, Y , Z, . . . into appropriate domains C, D, E, . . . endowed with the Scott topology. One of the simplest examples is given by the embedding of the discrete space of natural numbers into the so-called flat domain N⊥ of natural numbers [36, 29, 31]. A slightly more elaborate example is given by the embedding of (the one-point compactification of) the discrete space of natural numbers into the so-called domain of lazy natural numbers [16, 2]:
2
nq d
... q ∞
1q dqdqd... q n
0q ddq 2 ddq 1
0
The choice of domains depends, among other things, on the model of computation on the space. For example, the flat and lazy domains of natural numbers respectively capture callby-value and call-by-name evaluation of the successor map [16].
More sophisticated examples of such embeddings include: the Euclidean real line into the domain of compact real intervals ordered by reverse inclusion [34, 13, 10], the same space into the ideal completion of the rational basis of the interval domain, or a similar algebraic domain [14], Cantor space 2ω into the domain 2∞ = 2∗ ∪ 2ω of finite and infinite sequences ordered by prefix [31, 43, 39] (similarly, Baire space Nω into the domain N∞), the space of total functions N → N endowed with the compact-open topology (another version of Baire space) into the domain of partial functions ordered by graph inclusion [36, 31], any second countable T0 space into the domain Pω of subsets of natural numbers ordered by inclusion [35], any second countable T0 space as an isochordal subspace (see below for the definition) of T ω, where T is the flat domain T⊥ of truth values [30], any locally compact Hausdorff space into its upper power space [9], any Polish space onto the subspace of maximal points of a continuous dcpo (directed complete poset) [25, 12].
1.2 Injective spaces
Given embeddings of spaces X and Y into computational models C and D, we model continuous maps X → Y by Scott continuous functions C → D. Therefore it is natural to demand that the continuous functions C → D capture the continuous maps X → Y , in the sense that every continuous map of the latter kind (co)extends to a continuous function of the former kind. Since every continuous map f : X → Y trivially coextends to a continuous
2
map f : X → D, we only need to consider extensions of continuous maps f : X → D to continuous functions f¯ : C → D. This brings us to the subject of injective spaces.
A space D is injective in the ambient category of T0 spaces if every continuous map f : X → D extends to a continuous map f¯ : Y → D, for any space Y containing X as a subspace [33, page 99], as illustrated in the diagram below:
X⊂
j EY
dd
.....¯..
f d © f
D
where j : X → Y is the inclusion. (Notice that in principle there is nothing canonical about f¯.)
A main result in loc. cit. is the characterization of the injective spaces as the continuous lattices endowed with the Scott topology. For example, by the previous discussion, the continuous endomaps of the continuous lattice Pω capture the continuous maps between any two second countable T0 spaces [35, page 527].
If one restricts subspace to dense subspace in the definition, one speaks of densely injective spaces, which are characterized as the continuous Scott domains [15, page 127] (that is, continuous dcpos with least upper bounds of bounded subsets). A continuous Scott domain fails to be a continuous lattice only by lacking a (compact) top element [15, pages 52–53] and the continuous Scott domains coincide with the closed subspaces of the continuous lattices [15, page 109]. The examples of embeddings given above, except for the ones into the ideal completion of the rational intervals, Pω and T ω, and the ones about Polish spaces, are instances of dense embeddings into continuous Scott domains. In fact, these are examples of dense embeddings of Hausdorff spaces onto subspaces of maximal points of continuous Scott domains.
Gordon Plotkin [30, page 233] calls a subspace inclusion X ⊆ Y isochordal if for any two disjoint open sets U, U ⊆ X there are disjoint open sets V, V ⊆ Y with V ∩ X = U and V ∩ X = U . For example, every dense embedding is isochordal.
If one restricts subspace to isochordal subspace in the definition, one speaks of isochordally injective spaces. Plotkin [30, pages 233–234] characterized the second countable isochordally injective spaces as the countably based coherently complete domains (that is, countably based continuous dcpos in which every pairwise bounded subset has a least upper bound). A result by Paul Taylor [40, 2.5.4 and 2.6.4b] implies that the countability hypothesis is not necessary. An example of isochordal embedding into a coherently complete domain which is not a dense embedding is given by the embedding of the real line into the ideal completion of the compact rational intervals ordered by reverse inclusion, defined by x → {[p, q]|p < x < q}.
More generally, if in the definition j ranges over a given class J of embeddings, then one speaks of injective spaces over J [15, page 121].
1.3 Injective spaces and function spaces
By the above discussion, if j : X → C and k : Y → D are subspace embeddings into injective spaces, then the continuous functions C → D capture the continuous maps X → Y in the sense of the (co)extension property. When one considers higher-order maps [X → Y ] → Z, such as the integration and supremum operators discussed in [11], one is led to consider the
3
case in which the function space [C → D] captures the the function space [X → Y ], in the
stronger sense of having it embedded as a subspace, via some continuous (co)extension map
[X → Y ] → [C → D]. By the above remarks, it suffices to consider continuous extension
maps [X → D] → [C → D]. Although in principle there is nothing canonical about the extended map f¯ in the definition
of injective space, this turns out to be the case. In fact, Scott [33, page 116] showed that if D is
injective and j : X → Y is a subspace embedding, then every continuous map f : X → D has
a greatest continuous extension along j, which will be convenient to denote by f /j : Y → D,
given by
f /j(y) = ↑
f j−1(V ) .
y∈V ∈ΩY
Here hom-sets are ordered by the pointwise ordering induced by the specialization order of the target space and ΩY is the frame of open sets of Y .
Having established this result, Scott asked whether the greatest-extension map f → f /j is Scott continuous (very much doubting that this would be the case in general). Here [X → D] and [Y → D] are endowed with the Scott topology, which coincide with the Isbell topology if X and Y are exponentiable [26, page 154] (which further coincide with the compact-open topology if X and Y are locally compact [23, page 61]). Since the greatest-extension map is a right inverse of the restriction map g → g ◦ j, which is always Scott continuous, the greatest-extension map is a subspace embedding iff it is Scott continuous, and in this case [X → D] is a retract of [Y → D].
We show that the greatest-extension map f → f /j is Scott continuous iff D is the trivial one-point space or j is a proper map in the sense of Hofmann and Lawson [18, page 154]. Briefly, a continuous map j : X → Y is proper if the right adjoint ∀j : ΩX → ΩY of its associated frame map Ωj : ΩY → ΩX defined by Ωj(V ) = j−1(V ) is Scott continuous.
The terminology “proper” has been used in several slightly distinct senses in the literature1 – see e.g. [4, pages 97–107] [20, page 104] [41] and the remarks by Johnstone [20, page 121] and Vickers [42, Section 5]. To make things worse, in our case we have the unfortunate ambiguity of the expression “proper subspace embedding”, which can mean either an embedding onto a proper subspace or an embedding which is a proper map in the sense just defined. We have therefore decided to refer to the proper maps in the sense of Hofmann and Lawson as finitary maps and to the subspaces whose inclusion map is finitary as finitary subspaces. The terminology “finitary” is borrowed from Banaschewski [3, page 649], who calls a nucleus on a locale finitary if it is Scott continuous, and it is justified by the fact that a subspace embedding is finitary iff its induced nucleus is finitary.
In view of the above result on injective spaces and finitary embeddings, we are led to investigate the finitary subspaces of injective spaces. More concrete characterizations of the notions of finitary map and finitary subspace are given in the technical development that follows this introduction. For the time being, we remark that the finitary sober subspaces of a (densely) injective space D are the sober subspaces X such that Q ∩ X is compact for every compact saturated set Q ⊆ D. Also, the finitary sober subspaces of the (densely) injective spaces are exactly the stably locally compact spaces. This is a consequence of more general results, including the following.
In the ambient category of sober spaces, the full subcategories of respectively compact, locally compact, spectral and stably locally compact spaces are closed under the formation
1If X and Y are Hausdorff spaces then all definitions are equivalent.
4
of finitary subspaces. Here we don’t assume the Hausdorff separation axiom in the definition of compactness; a space is compact iff it satisfies the Heine-Borel property. Stably locally compact spaces are considered in [20, page 313] [17] [38]. Such spaces are called coherent in [2], but Johnstone [20, page 63] calls coherent the spaces which Vickers [43, page 120] and Smyth [39, page 649] call spectral.
Also, in this ambient category, for every subspace X of a space Y there is a smallest finitary subspace X¯ of Y containing X as a subspace, which we refer to as the finitary hull of X. Moreover, every space has a smallest finitary dense subspace (its support), which is the finitary hull of its subspace of maximal points. In the stably locally compact case, the support is the subspace of maximal points iff that subspace is compact.
The above results hold in the more general category of locales. Moreover, the full subcategory of locales with enough points is closed under the formation of finitary sublocales. Also, the smallest finitary dense sublocale of a locale is the finitary hull of its smallest dense sublocale.
1.4 Injective spaces and upper power spaces
Having established that the “good denominators” are the finitary subspace embeddings, one wonders what the finitarily injective spaces are. We show that they are precisely the algebras of the upper power space monad in the category of sober spaces (considering the empty set as a point of the upper power space construction), which coincide with the retracts of upper power spaces of sober spaces. Moreover, greatest extensions exist and are given by
f /j(y) = f j−1(↑y) .
The full subcategory of locally compact sober spaces is closed under the upper power space construction. The finitarily injective spaces in this subcategory are the continuous meetsemilattices with unit, by virtue of the characterization of the algebras given in [32, pages 135 and 140]. The full subcategory of stably compact spaces is also closed under the upper power space construction. In this subcategory, the finitarily injective spaces are again the continuous lattices.
1.5 Injective spaces and KZ-monads
The above characterization of the finitarily injective spaces is a particular case of a more general result on KZ-monads [24] on poset-enriched categories established in the present paper. Moreover, this result is applied to the lower and upper power locale monads discussed in [32] (see below). If the underlying functor of the monad is Scott continuous on hom-posets (which is the case in our applications), the extension map is also Scott continuous, so that we don’t lose the continuity of the extension map along finitary embeddings when we consider the larger class of finitarily injective spaces.
1.6 Injective spaces and lower power spaces
In applications of domain theory (see e.g. Scott [35, page 528] and Plotkin [31, page 14]), one sometimes wishes to consider least extensions. We show that the least continuous extension along a subspace embedding j : X → Y of an injective-valued map f : X → D exists iff D is trivial or j is semiopen, in the sense that its associated frame map Ωj : ΩY → ΩX has a
5
left adjoint ∃j : ΩX → ΩY . The process of taking least continuous extensions is always Scott continuous, essentially because ∃j, being a left adjoint, preserves all joins.
By an application of the general result on KZ-monads and a result by Steve Vickers [42, Proposition 4.6], we conclude that the injective locales over semiopen embeddings are the algebras of the lower power locale monad. It is plausible the same result holds for the injective spaces over semiopen embeddings, but we don’t pause to check whether this is the case.
1.7 Injective spaces and Kan extensions
By definition, f /j is the greatest continuous map g : Y → D such that g ◦ j = f . Scott [33, page 116] remarked that f /j is in fact the greatest continuous map g such that g ◦ j ≤ f . This shows that f /j is the right Kan extension of f along j. The general definition of a Kan extension of a functor can be found in [7, page 39] and [27, page 232], and its specialization to a monotone map can be found in [1, page 22]. In this paper we consider Kan extensions of arrows of poset-enriched categories.
By virtue of Scott’s remark, D is injective iff for every subspace embedding j : X → Y the restriction map g → g ◦ j : hom(Y, D) → hom(X, D) has an injective right adjoint f → f /j : hom(X, D) → hom(Y, D). We make this characterization into a definition of right injective object in a poset-enriched category. By omitting the injectivity condition on the right adjoint, we obtain a definition of right Kan object; this means that in general we only have (f /j) ◦ j ≤ f . Similarly, we obtain definitions of left Kan and left injective objects.
We show that every injective space over subspace embeddings is a right Kan space over arbitrary continuous maps. Similarly, every right injective space over finitary embeddings is a right Kan space over arbitrary finitary maps, and every left injective locale over semiopen embeddings is a left Kan locale over arbitrary semiopen maps.
1.8 Injective spaces and dense embeddings
The above results on greatest extensions and continuity of the extension map generalize to densely injective spaces. Also, the injective spaces over finitary dense embeddings are characterized via an application of the above result on KZ-monads to the upper power space monad without the empty set as a point of the upper power space construction.
1.9 Injective spaces and isochordal embeddings
Unfortunately, the isochordally injective spaces fail to enjoy both the least- and greatestextension properties, as simple counter-examples which can be safely left to the reader show.
2 Kan objects in poset-enriched categories
2.1 Poset-enriched categories
A poset-enriched category is a category whose hom-sets are posets and whose composition operation is monotone. A poset-functor between poset-enriched categories is a functor which is monotone on hom-posets. A poset-functor F : X → A is poset-faithful if Uf ≤ Ug in A implies f ≤ g in X.
6
The main example of a poset-enriched category is Poset, the category of posets and monotone maps with hom-sets ordered pointwise. If X is any category and U : X → Poset is a faithful functor, then there is a unique way of making X into a poset-enriched category so as to also make U into a poset-faithful functor, given by the definition
f ≤ g in X iff Uf ≤ Ug in Poset,
because one direction of the definition is equivalent to saying that U is a poset-functor and the other is equivalent to saying that U is poset-faithful.
Our main example of such a situation is given by the category Sp0 of T0 topological spaces and continuous maps with U the specialization-order functor. The specialization order [15, page 123] [20, page 45] on the points of a space X is defined by x ≤ y iff every neighborhood of x is a neighborhood of y iff x belongs to the closure of {y}. This definition makes ≤ into a reflexive and transitive relation, which is antisymmetric iff X is T0. Also, it is clear from the definition that any continuous map preserves this preorder. Then the functor in question sends a T0 space to its set of points ordered by the specialization order, and a continuous map to itself. Thus, the induced poset-enrichment in Sp0 is given simply by f ≤ g in hom(X, Y ) iff f (x) ≤ g(x) for all x ∈ X.
Definition 2.1.1 Let X be a poset-enriched category, I be any category, F : I → X be a functor, and P ∈ X be a limit of F with projections {πi : P → Fi}i∈I. Then there is a bijection between the set of cones under X and the set hom(X, P ), which sends the cone {gi : X → Fi}i∈I to the unique g : X → P such that gi = πi ◦ g for all i ∈ I. We say that the given limit is a poset-limit if the above bijection is an order-isomorphism for each X, where cones under X are ordered by {gi : X → Fi}i∈I ≤ {hi : X → Fi}i∈I iff gi ≤ hi for all i ∈ I.
This notion is a particular case of the general notion of V-limit in a V-enriched category, which can be found in e.g. [7, page 7].
All limits in Poset are poset-products, and the same holds for Sp0, poset-enriched as above, because the specialization-order functor U : Sp0 → Poset preserves limits.
2.2 Adjunctions between objects of poset-enriched categories
For a complete account to adjunctions between posets the reader is referred to [15] or [2]. In this subsection we fix terminology and basic facts about adjunctions between objects of poset-enriched categories.
An adjunction between objects X and Y of a poset-enriched category is a pair of arrows l : X → Y and r : Y → X such that l ◦ r ≤ idY and idX ≤ r ◦ l. Such an adjunction is denoted by l r, and l and r are said to be respectively left and right adjoint to each other. In an adjunction l r, each adjunct l and r is uniquely determined by the other.
An adjunction l r is reflective if l ◦ r = idY , and it is coreflective if idX = r ◦ l. A poset-functor F preserves adjunctions in the sense that l r implies Fl Fr; moreover, if F is poset-faithful then it reflects adjunctions in the sense that l r whenever Fl Fr.
Adjunctions compose in the sense that if l : X → Y , l : Y → Z, r : Y → X and r : Z → Y are arrows with l r and l r , then l ◦ l r ◦ r .
7
2.3 Kan extensions of arrows of poset-enriched categories
We first briefly specialize the definition of Kan extension [7, page 39] [27, page 232] from functors to monotone maps (cf. [1, page 22]), and then we consider its (immediate) generalization to arrows of poset-enriched categories.
Let j : X → Y and f : X → D be monotone maps between posets. A right Kan extension of f along j is a monotone map f /j : Y → D such that
(Kan1) (f /j) ◦ j ≤ f
(Kan2) g ◦ j ≤ f for g : Y → D implies g ≤ f /j.
Inequality (Kan1) is illustrated in the following diagram:
X
j EY
dd ≥ f d © f /j
D
Dually, we obtain the definition of left Kan extension by reversing the inequalities. We denote the left Kan extension of f along j by f \j whenever it exists.
By definition, the right Kan extension of f along j, if it exists, is the greatest map g : Y → D such that g ◦ j ≤ f . This is equivalent to saying that for all g : Y → D,
g ◦ j ≤ f iff g ≤ f /j,
which shows that right Kan extensions along a fixed j : X → Y exist for all f : X → D iff the composition map
g → g ◦ j : hom(Y, D) → hom(X, D)
has a right adjoint
f → f /j : hom(X, D) → hom(Y, D).
In [7] and [27], f /j and f \j are denoted by Ranjf and Lanjf respectively. Our notation makes the basic properties of Kan extensions easier to remember, because they resemble the properties of quotients (cf. Theorem 2.3.3 below).
The above definition formally applies to arrows between objects of poset-enriched categories. Before considering this generalization, we consider some basic properties which make sense only for monotone maps between posets. Proposition 2.3.1 and 2.3.2 are obtained by specializing the corresponding results in loc. cit. from functors to monotone maps.
Kan extensions generalize adjunctions, as Proposition 2.3.1, Theorem 2.3.4 and Corollary 2.3.5 below show:
Proposition 2.3.1 A monotone map f : X → D has a right Kan extension along a monotone map j : X → Y if the set f (j−1(↑y)) has a meet in D for each y ∈ Y , and in this case
it is given by f /j(y) = f j−1(↑y) .
An order-embedding [5, page 10] is a monotone map j : X → Y which reflects order in the sense that j(x) ≤ j(x ) implies x ≤ x . The following proposition shows that the right Kan extension f /j is an actual extension if j is an order-embedding:
8
Proposition 2.3.2 If j : X → Y is an order-embedding and f : X → D is a monotone map with a right Kan extension along j, then (f /j) ◦ j = f.
We now prove the facts that generalize to Kan extensions of arrows of poset-enriched categories.
Theorem 2.3.3 Let j : X → Y , k : Y → Z, f : X → D, and r : D → E be arrows of a poset-enriched category. Then the following properties hold whenever the right Kan extensions f /j, (f /j)/k and f /(k ◦ j), f /f and (r ◦ f )/j exist:
1. f /idX = f ,
2. (f /j)/k = f /(k ◦ j),
3. idD ≤ f /f = (f /f ) ◦ (f /f ) (if idD = f /f then f is said to be codense [27, page 242]),
4. r ◦ (f /j) ≤ (r ◦ f )/j, equality holding if r has a left adjoint.
These (in)equations are illustrated in the following diagrams:
X
idX
EX
X
j EY
k EZ
d df d = f d © X
d d≥ fd d
f /j ≥ (f /j)/k = f /(k ◦ j)
c© D
Xf
d df d ≥ d © D
ED f /f ≥ idD
X
j
EY
ed
¡
e df ed
≥ f /j
¡ ¡
e d © ¡
r ◦ fee=e D ≤¡¡(¡r ◦ f )/j
e
¡
e r¡
e¡
e c¡
E
Proof (1): Trivial. (2): By two applications of (Kan1), ((f /j)/k) ◦ k ◦ j ≤ (f /j) ◦ j ≤ f . By (Kan2), (f /j)/k ≤ f /(k ◦ j). In the other direction, (f /(k ◦ j)) ◦ k ◦ j ≤ f by (Kan1). By two applications of (Kan2), f /(k ◦ j) ≤ (f /j)/k.
(3): Since idD ◦ f ≤ f , we conclude that idD ≤ f /f by (Kan2). By monotonicity of composition, f /f ≤ (f /f ) ◦ (f /f ). In the other direction, (f /f ) ◦ (f /f ) ◦ f ≤ (f /f ) ◦ f ≤ f by two applications of (Kan1). Therefore (f /f ) ◦ (f /f ) ≤ f /f by (Kan2).
(4): r ◦ (f /j) ◦ j ≤ r ◦ f by (Kan1). Therefore r ◦ (f /j) ≤ (r ◦ f )/j by (Kan2). In order to establish the inequality in the other direction, assume that r has a left adjoint l. By (Kan1), ((r ◦ f )/j) ◦ j ≤ r ◦ f . By composing with l on the left and using the fact that l ◦ r ≤ idY , l ◦ ((r ◦ f )/j) ◦ j ≤ l ◦ r ◦ f ≤ f . Hence l ◦ ((r ◦ f )/j) ≤ f /j by (Kan2). By composing with r on the left, r ◦ l ◦ ((r ◦ f )/j) ≤ r ◦ (f /j). But idX ≤ r ◦ l. Therefore (r ◦ f )/j ≤ r ◦ (f /j).
9
Item (4) generalizes [33, Lemma 3.9], whose statement amounts to the equation j ◦ (g/e) = (j ◦ g)/e, from greatest extensions to right Kan extensions (and from coreflective adjunctions to adjunctions).
Theorem 2.3.4 Let l : Y → X and r : X → Y be arrows of a poset-enriched category.
1. If l r then every arrow f : X → D has a right Kan extension along r given by f /r = f ◦ l. In particular, l = idX /r.
2. If idX and r have right Kan extensions along r and r ◦ (idX /r) = r/r, then idX /r r. Proof (1): f ◦ l ◦ r ≤ f because l ◦ r ≤ idX by definition of adjunction. This establishes (Kan1). Assume that g ◦ r ≤ f for g : Y → D. Since g ◦ r ◦ l ≤ f ◦ l and since idY ≤ r ◦ l by definition of adjunction, we conclude that g ≤ f ◦ l. This establishes (Kan2). The particular case follows by taking D = X and f = idX .
(2): By (Kan1), (idX /r)◦r ≤ idX . This establishes one half of the adjunction. Since r/r ≥ idY by Theorem 2.3.3(3), we conclude that r ◦ (idX /r) ≥ idY by the hypothesis and transitivity, which establishes the other half. Therefore idX /r r.
Corollary 2.3.5 The arrow r : X → Y has a left adjoint iff idX and r have a right Kan extension along r and the condition r ◦ (idX /r) = r/r holds, and in this case it is idX /r. Proof If l r then r ◦ (idX /r) = r ◦ (idX ◦ l) = r ◦ l = r/r by Theorem 2.3.4(1). The converse is Theorem 2.3.4(2).
2.4 Kan objects in poset-enriched categories
Let X be a poset-enriched category and J be any subcategory of X. Definition 2.4.1 Let D be an object of X.
1. D is a right Kan object over J if for each j : X → Y in J the composition map
◦j : hom(Y, D) → hom(X, D)
has a right adjoint also denoted by RanDj .
/j : hom(X, D) → hom(Y, D),
2. D is a right injective object over J if in addition the right adjoint is an injective function, which means that the right Kan extension f /j is an actual extension, in the sense that (f /j) ◦ j = f .
Left Kan objects and left injective objects are defined dually (at the level of hom-posets), and left-Kan-extension maps are denoted by LanDj .
Let X/J denote the subcategory of X consisting of right Kan objects over J and right adjoints between them. The following is a corollary of Theorem 2.3.3:
Proposition 2.4.2 The equations
Ran(X, D) = hom(X, D) Ran(j : X → Y, r : D → E) = f → r ◦ f /j : hom(X, D) → hom(Y, E)
define a functor Ran : J × X/J → Poset. Notice that RanDj = Ran(j, idD).
10