Injective spaces via the filter monad

Martín Hötzel Escardó

Laboratory for the Foundations of Computer Science Edinburgh University, King’s Buildings, Mayfield Road Edinburgh EH9 3JZ, Scotland

  M.Escardo@ed.ac.uk   http://www.dcs.ed.ac.uk/home/mhe

Abstract

An injective space is a topological space with a strong extension property for continuous maps with values on it. A certain filter space construction embeds every T_{0} topological space into an injective space. The construction gives rise to a monad. We show that the monad is of the Kock-Zöberlein type and apply this to obtain a simple proof of the fact that the algebras are the continuous lattices (Alan Day, 1975, Oswald Wyler, 1976). In previous work we established an injectivity theorem for monads of this type, which characterizes the injective objects over a certain class of embeddings as the algebras. For the filter monad, the class turns out to consist precisely of the subspace embeddings. We thus obtain as a corollary that the injective spaces over subspace embeddings are the continuous lattices endowed with the Scott topology (Dana Scott, 1972). Similar results are obtained for continuous Scott domains, which are characterized as the injective spaces over dense subspace embeddings.

Key-words: Extension of maps, injective space, continuous lattice, continuous Scott domain, domain theory, Kock-Zöberlein monad.

AMS classification: 54C20, 06B35, 18C20.

1 Introduction

An injective space is a topological space D with a strong extension property for continuous functions with values on D, to the extent that every continuous map f : X → D extends to a continuous map f̄ : Y → D, for every space Y containing X as a subspace. For example, the extended real line endowed with the topology of lower semicontinuity is an injective space [5].

A certain filter space construction embeds every T_{0} topological space into an injective space. In addition to containing the given space embedded as a subspace, the filter space appears as a quotient of its own filter space. Technically and more precisely, the filter space construction is a monad—see [7] for the definition. We show that the monad is of the Kock-Zöberlein type [6] and apply this to obtain a simple proof of Alan Day’s result that its algebras are the continuous lattices [2].

In [3] we proved that, given a category with the structure of a Kock-Zöberlein monad, the objects that are injective over a certain class of embeddings specified in terms of the monad structure coincide with the algebras of the monad. It turns out that for the filter monad the embeddings are exactly the subspace embeddings. The fact that the injective spaces over subspace embeddings are precisely the continuous lattices endowed with the Scott topology, established by Dana Scott [8], thus appears as a corollary of the characterization of the algebras.

The continuous Scott domains are the algebras of the proper filter monad [11]. For this monad, the associated embeddings are precisely the dense subspace embeddings, and hence the injective spaces over dense embeddings are characterized as the continuous Scott domains. This characterization is folklore for the experts. It was first formulated and proved by Scott, but only published as Exercise II.3.19 of the Compendium [5], whose emphasis is on continuous lattices (personal communication).

More examples of the above situation, including the lower and upper space monads, are investigated in the paper [3], which also has a long introduction explaining the fundamental role of injectivity in Scott’s mathematical theory of computation and its connections with function spaces. Even more examples have been recently discovered by Bob Flagg and the author [4].

For background on continuous lattices the reader is referred to [5]. For more about domain theory and topology see [1, 9].

2 The filter space construction

The filter monad is defined on the category of T_{0} topological spaces and continuous maps. Recall that a space is T_{0} if no two distinct points share the same system of neighborhoods. Given a space X, one denotes its lattice of opens sets by ΩX and constructs the filter space FX as follows. The points are the filters of ΩX. The open sets are generated by the sets

□U = {ϕ ∈ FX | U ∈ ϕ}, U ∈ ΩX,

which form a base as □U ∩ □U′ = □(U ∩ U′).

Given a continuous map f : X → Y, one defines a function Ff : FX → FY by

Ff(ϕ) = {V ∈ ΩY | f^{−1}(V) ∈ ϕ}.

Then F is a functor and one has natural transformations η_{X} : X → FX and μ_{X} : FFX → FX defined by

η_{X}(x) = {U ∈ ΩX|x ∈ U}, μ_{X}(Φ) = ⋃{⋂ U | U ∈ Φ},

which make F into a monad F = (F, η, μ).

Continuity of the functions defined above follows from the fact that

(Ff)^{−1}(□V) = □f^{−1}(V),  η_{X}^{−1}(□U) = U,  μ_{X}^{−1}(□U) = □□U.

The first two equations are routinely verified and the last follows from §2.1 below. Since η_{X} is one-to-one (precisely because X is T_{0}), the second equation shows that η_{X} embeds X as a subspace of FX. The unit laws μ_{X} ∘ η_{FX} = μ_{X} ∘ Fη_{X} = id_{FX} show that μ_{X} is a retraction map (in two ways) and hence FX is a quotient of FFX, because retractions are quotient maps.

2.1 μ_{X}(Φ) = {U ∈ ΩX|□U ∈ Φ}.

Let U ∈ μ_{X}(Φ). Then there is U ∈ Φ with U ∈ ⋂ U, and hence with U ∈ ϕ for all ϕ ∈ U. From this we see that U ⊆ □U. Hence □U ∈ Φ because filters are upper closed. Therefore μ_{X}(Φ) ⊆ {U ∈ ΩX|□U ∈ Φ}. In order to establish the inclusion in the other direction, let U ∈ ΩX with □U ∈ Φ. We have to show that there is U ∈ Φ with U ∈ ⋂ U. We can take U = □U, because ⋂ □U = ↑U, the principal filter generated by U, and the proof is concluded.

Note It follows from this that the filter monad is formally analogous to the so-called continuation monad. In fact, an open set can be regarded as a continuous map into Sierpinski space and a filter can be regarded as a finite-meet-preserving map into the two-point lattice, so that set-abstraction can be translated to lambda-abstraction as in

Ff(ϕ) = λV · ϕ(λx · V (f(x))),
η_{X}(x) = λU · U(x),
μ_{X}(Φ) = λU · Φ(λϕ · ϕ(U)),

which is syntactically equivalent to the definition of the continuation monad.

3 Kock-Zöberlein monads

A monad T = (T, η, μ) defined on a poset-enriched category X, with T : X → X a locally monotone functor, is said to be of the Kock-Zöberlein type if the condition

η_{T X} ≤ T η_{X}

holds for all X. Notice that our definition is dual (at the level of hom-posets) to that of [6].

Since X is poset-enriched, one can consider adjunctions of arrows. Given arrows l : X → Y and r : Y → X one defines

l ⊣ r iff l ∘ r ≤ id_{Y} and id_{X} ≤ r ∘ l,

and one says that l is left adjoint to r and that r is right adjoint to l. In this case each adjunct l and r is uniquely determined by the other. The adjunction is said to be reflective if l ∘ r = id_{Y}, and coreflective if id_{X} = r ∘ l. In these cases one writes l ⊣_{r} r and l ⊣_{c} r respectively.

By specializing Anders Kock’s results [6] from 2-categories to poset-enriched categories, we learn that

3.1 If T = (T, η, μ) is a Kock-Zöberlein monad then

1. An arrow α : T X → X is the structure map of a T -algebra iff η_{X} ⊣_{c} α.

2. η_{T X} ⊣ μ_{X}.

3. μ_{X} ⊣ T η_{X}.

(We showed in [3] that each of these properties is in fact equivalent to the Kock-Zöberlein property.)

By §3.1(1), every object can be the underlying object of at most one algebra, and every structure map of an algebra is uniquely determined by the underlying object of the algebra (as the right adjoint of the unit of the object). Due to this reason, we can identify the algebras of a Kock-Zöberlein monad with their underlying objects.

4 Injective objects which are the algebras of Kock-Zöberlein monads

In what follows we work with a Kock-Zöberlein monad T = (T, η, μ) defined on a poset-enriched category X. The arrows singled out in the following definition are particular cases of the semiupper maps of [10], for which the reflectivity condition is not required:

4.1 By a T -embedding we mean an arrow j : X → Y such that the map T j : T X → T Y has a reflective left adjoint, denoted by T^{∗}j : T Y → T X.

For example, η_{X} : X → T X is a T -embedding with T^{∗}η_{X} = μ_{X}, because the adjunction 3.1(3) is reflective by virtue of the unit law μ_{X} ∘ T η_{X} = id_{X}.

Note The following conditions are equivalent:

1. T -embeddings are order-monic.

2. Each component of η is order-monic.

3. T is order-faithful.

(1) ⟹ (2): Immediate. (2) ⟹ (3): If T f ≤ T g then we have that T f ∘ η_{X} ≤ T g ∘ η_{X} by composition with η_{X}, that η_{Y} ∘ f ≤ η_{Y} ∘ g by naturality, and that f ≤ g by the assumption. (3) ⟹ (1): Let j : X → Y be a T -embedding and f, g : Z → X be arrows with j ∘ f ≤ j ∘ g. Then T j ∘ T f ≤ T j ∘ T g by local monotonicity of T. Hence T f ≤ T g because T j is split-mono. Therefore f ≤ g by the assumption, and the proof is concluded.

4.2 An object D is said to be injective over an arrow j : X → Y if every map f : X → D has an extension f̄: Y → D along j : X → Y, in the sense that the following diagram commutes:

X  \overline{j  ^{}}Y
[figure: f; .......; f̄]
D

One normally assumes that j : X → Y is a monomorphism, so that the word extension is applied in the usual sense, but this is unimportant here. Notice that the extension f̄ need not be unique. But since X is poset-enriched, a definition with canonical choice is possible. We first recall a concept.

A right Kan extension of a map f : X → D along an arrow j : X → Y is a (necessarily unique) map f/j : Y → D such that

1. f/j ∘ j ≤ f and

2. f̄∘ j ≤ f implies f̄ ≤ f/j.

In other words, f/j is the largest solution in f̄ to the inequality f̄ ∘ j ≤ f. In the case that we have equality in (1), we say that f/j is a right extension of f along j.

4.3 We say that an object D is right injective over an arrow j : X → Y if every map f : X → D has a right extension f/j : Y → D along j : X → Y.

4.4 The following statements are equivalent for any object D:

1. D is injective over T -embeddings.

2. D is right injective over T -embeddings.

3. D is a T -algebra.

In this case, if f : X → D is any arrow and j : X → Y is a T - embedding then f/j = m_{D} ∘ T f ∘ T^{∗}j ∘ η_{Y} .

Here m_{D} : T D → D is the unique structure map of the algebra D. The construction of f/j is illustrated in the following diagrams:

[figure: X; j; Y; T X; T^{∗}j; T Y; η_{Y}; Y]
[figure: f; .......; f/j; T f; ....................; f/j]
D  T D
[figure: m_{D}]
D

This was established in [3].

Note It is a basic property of monads that T X endowed with the structure map μ_{X} : T T X → T X is a free T -algebra with insertion of generators η_{X} : X → T X. More precisely, the following universal property holds. Given any T -algebra A with structure map α : T A → A, every arrow f : X → A extends uniquely to a T -algebra homomorphism f̄: T X → A, which is constructed as f̄ = α ∘ T f:

X  \overline{η_{X}  ^{}}T X
[figure: f; .......; f̄]
A

See [7, Theorem VI.2.1]. In general, there can be many arrows f̄ extending f along η_{X}. By 4.4, there is a greatest one, which coincides with the unique T - algebra homomorphism extending f. In fact, one has that

f/η_{X} = α ∘ T f ∘ T^{∗}η_{X} ∘ η_{T X} = α ∘ T f ∘ μ_{X} ∘ η_{T X} = α ∘ T f = f̄,

because α = m_{A}. By taking A = T Y and f = η_{Y} ∘ g for g : X → Y arbitrary, recalling that T g : T X → T Y is always an algebra homomorphism, one sees that the functor part of a Kock-Zöberlein monad is uniquely determined by the unit of the monad, by its object part and by the extension property as T g = (η_{Y} ∘g)/η_{X}. In particular, by taking g = id_{X} we conclude that η_{X}/η_{X} = id_{T X}.

4.5 An object is a T -algebra iff it is a retract of a free T -algebra.

This fact, which is a useful tool for obtaining concrete characterizations of the algebras, was first proved by Anders Kock [6]. It is also a corollary of 4.4, using the facts that η_{A} is a T -embedding and that an injective object over T -embeddings is a retract of every object into which it is T -embedded [3].

5 The filter monad is of the Kock-Zöberlein type

T_{0} topological spaces and continuous maps form a poset-enriched category under the pointwise specialization order. By a simple unfolding of definitions, one sees that the pointwise specialization order is characterized by, for all f, g : X → Y,

f ≤ g iff f^{−1}(V) ⊆ g^{−1}(V) for every V ∈ ΩY.

5.1 F is locally monotone.

Let f, g : X → Y with f ≤ g. In order to prove that Ff ≤ Fg, let ϕ ∈ FX and V ∈ Ff(ϕ). This means that f^{−1}(V) ∈ ϕ. Since f^{−1}(V) ⊆ g^{−1}(V) and ϕ is upper closed, we have that g^{−1}(V) ∈ ϕ. But this means that V ∈ Fg(ϕ). Therefore Ff(ϕ) ⊆ Fg(ϕ).

5.2 F is of the Kock-Zöberlein type.

By specializing the definitions to the appropriate types, we obtain

η_{FX}(ϕ) = {U ∈ ΩFX|ϕ ∈ U}, Fη_{X}(ϕ) = {U ∈ ΩFX|η_{X}^{−1}(U) ∈ ϕ}.

Let U ∈ η_{FX}(ϕ). This means that ϕ ∈ U. By openness of U, there is U ∈ ϕ with □U ⊆ U. Since U = η_{X}^{−1}(□U), we see that □U ∈ Fη_{X}(ϕ). And since filters are upper sets, we conclude that U ∈ Fη_{X}(ϕ), which establishes η_{FX}(ϕ) ⊆ Fη_{X}(ϕ).

5.3 The F-embeddings are precisely the subspace embeddings.

Given a continuous map f : X → Y, its frame map f^{−1} : ΩY → ΩX preserves all joins and hence has a right adjoint f_{∗} : ΩX → ΩY, which sends an open set U ∈ ΩX to the largest open set V ∈ ΩY such that f^{−1}(V) ⊆ U. We can thus define a map F^{∗}f : FY → FX by

F^{∗}f(γ) = {U ∈ ΩX | f_{∗}(U) ∈ γ}.

The set F^{∗}f(γ) is a filter because f_{∗} preserves meets. The function F^{∗}f is continuous because one easily computes

(F^{∗}f)^{−1}(□U) = □f_{∗}(U).

That this produces a left adjoint to Ff is verified as follows:

Ff(F^{∗}f(γ)) = {V ∈ ΩY | f^{−1}(V) ∈ F^{∗}f(γ)}
= {V ∈ ΩY | f_{∗}(f^{−1}(V)) ∈ γ)} ⊇ γ,

because if V ∈ γ then f_{∗}(f^{−1}(V)) ∈ γ as V ⊆ f_{∗}(f^{−1}(V)). Similarly, one concludes that F^{∗}f(Ff(ϕ)) ⊆ ϕ. Reflectiveness means that F^{∗}f ∘Ff(ϕ) = ϕ. So we have to check that the equation f^{−1}(f_{∗}(U)) = U holds iff f is an embedding. But this equation is equivalent to saying that f^{−1} is surjective, which is in turn equivalent to saying that f is a subspace embedding, because our spaces are assumed to be T_{0}.

Note The components of the unit are order-monic.

Assume that η_{X}(x) ≤ η_{X}(y) and let U be an open neighborhood of x. Then U ∈ η_{X}(x) and hence U ∈ η_{X}(y) by the assumption, which means that y ∈ U. Therefore x ≤ y.

Corollary F is order-faithful and subspace embeddings are order-monic.

By virtue of Note 4.1.

6 Injective spaces

We take the characterization [8, Proposition 2.4] as our definition: A complete lattice D is continuous if every d ∈ D is the “lim inf” of its filter of Scott open neighborhoods, in the sense that d = ⋁{⋀ U | d ∈ U}, where U ranges over Scott open sets. Recall that the continuous lattices appear as the (Scott continuous) retracts of the continuous lattices.

6.1 FX is an algebraic lattice endowed with the Scott topology.

It is immediate that the specialization order of FX is inclusion of filters. Since the lattice of filters is algebraic with the principal filters as the compact elements, and since □U is the set of filters containing the principal filter ↑U, we see that □U is a basic Scott open set, which establishes the claim.

6.2 The algebras of the filter monad are the continuous lattices endowed with the Scott topology.

Moreover, the structure map m_{D} : FD → D of an algebra with underlying space D is given by

m_{D}(ϕ) = ⋁ {⋀ U | U ∈ ϕ} .

We know by 6.1 that the free algebra FX is an algebraic lattice endowed with the Scott topology, and by 4.5 that every algebra is a retract of a free algebra. Therefore the algebras are continuous lattices. Conversely, let D be a continuous lattice endowed with the Scott topology. It is clear that m_{D} : FD → D is monotone. We know that FD is an algebraic lattice with a basis consisting of principal filters and that every filter is the directed join of the principal filters generated by its members. Thus, in order to establish continuity of m_{D}, it is enough to show that m_{D}(ϕ) = ⋁{m_{D}(↑U)|U ∈ ϕ}. But this is immediate because m_{D}(↑U) = ⋀ U. By §3.1, one has that m_{D} is a structure map iff η_{D} ∘ m_{D} ≤ id_{FD} and m_{D} ∘ η_{D} = id_{D}. The equation holds precisely because D is continuous. In order to establish the inequality, first notice that η_{D} ∘ m_{D}(ϕ) = {U ∈ ΩD | ⋁{⋀ U′ | U′ ∈ ϕ} ∈ U}. Let U ∈ η_{D} ∘ m_{D}(ϕ). Then ⋀ U′ ∈ U for some U′ ∈ ϕ because {⋀ U′ | U′ ∈ ϕ} is directed and U is Scott open. Hence U ∈ ϕ because U′ ⊆ U. Therefore η_{D} ∘ m_{D}(ϕ) ⊆ ϕ.

Note Alan Day also proved that if D and E are algebras then a continuous function f : D → E is an algebra homomorphism iff it preserves all meets.

6.3 The injective spaces over subspace embeddings are the continuous lattices endowed with the Scott topology.

Moreover, if f : X → D is a continuous map into a continuous lattice and j : X → Y is a subspace embedding, then f has a greatest extension along j, given by

f/j(y) = ⋁ {⋀ U | y ∈ j_{∗}(f^{−1}(U))} .

The F-embeddings are the subspace embeddings by 5.3. Therefore the result follows from 4.4, which says that the injective objects over the T -embeddings of a Kock-Zöberlein monad T are the T -algebras. The above formula is a special case of the general formula f/j = m_{A} ∘ T f ∘ T^{∗}j ∘ η_{Y} of 4.4.

Note Scott’s extension formula produces the map

y ↦ ⋁ {⋀ f(j^{−1}(V)) | y ∈ V } ,

which is equivalent to f/j as defined above.

7 Densely injective spaces

The definition of the filter monad still makes sense if the improper filter (the principal filter generated by the empty set—a top element) is ruled out. The resulting monad is referred to as the proper filter monad and is denoted by F^{+}. The previous results remain true with the following amendments.

By a continuous Scott domain we mean a poset with directed joins and non-empty meets (or, equivalently, bounded joins), subject to the approximation axiom of the definition of a continuous lattice. In the algebraic case one uses the terminology Scott domain.

7.1 F^{+}X is a Scott domain endowed with the Scott topology.

7.2 The F^{+}-embeddings are precisely the dense subspace embeddings.

Because a continuous map f : X → Y is dense iff f_{∗}(∅) = ∅, and this is the condition for F^{∗}f(ϕ) as defined in 5.3 being different from ↑∅ for all ϕ and hence F^{∗}f being well-defined.

7.3 The algebras of the proper filter monad are the continuous Scott domains endowed with the Scott topology. The homomorphisms are the meet-preserving continuous maps.

7.4 The injective spaces over dense subspace embeddings are the continuous Scott domains endowed with the Scott topology.

Acknowledgements I benefited from conversations with Thomas Streicher and Philipp Sünderhauf. I am grateful to Reinhold Heckmann, Anders Kock and Thomas Streicher for (independently) pointing out that a claim made in a previous version of this paper was incorrect (a correct formulation is given by Note 4.1). The diagrams were drawn with Paul Taylor’s package.

References

[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D.M. Gabbay, and T.S.E Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, Oxford, 1994.

[2] A. Day. Filter monads, continuous lattices and closure systems. Canadian Journal of Mathematics, XXVII(1):50–59, 1975.

[3] M.H. Escardó. Properly injective spaces and function spaces. Topology and Its Applications, 89(1–2):75–120, November 1998.

[4] M.H. Escardó and R. Flagg. Injective spaces which are the algebras of Kock-Zöberlein monads. In preparation, 1997.

[5] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, 1980.

[6] A. Kock. Monads for which structures are adjoint to units (version 3). Journal of Pure and Applied Algebra, 104:41–59, 1995.

[7] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[8] D. S. Scott. Continuous lattices. In F.W. Lawvere, editor, Toposes, Algebraic Geometry and Logic, volume 274 of Lectures Notes in Mathematics, pages 97–136. Springer-Verlag, 1972.

[9] M.B. Smyth. Topology. In S. Abramsky, D. M. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 1, pages 641–761. Clarendon Press, Oxford, 1992.

[10] S. Vickers. Locales are not pointless. In C. Hankin, I. Mackie, and R. Nagarajan, editors, Theory and Formal Methods 1994: Proceedings of the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, Mller Centre, Cambridge, 11–14 September 1994. IC Press. 1995.

[11] O. Wyler. Algebraic theories for continuous semilattices. Archive for Rational Mechanics and Analysis, 90(2):99–113, 1985.