Metric Spaces, Generalized Logic, and Closed Categories
Posted by Emily Riehl
Guest post by Tom Avery
Before getting started, I’d like to thank Emily for organizing the seminar, as well as all the other participants. It’s been a lot of fun so far! I’d also like to thank my supervisor Tom Leinster for some very helpful suggestions when writing this post.
In the fourth instalment of the Kan Extension Seminar we’re looking at Lawvere’s paper “Metric spaces, generalized logic, and closed categories”. This is the paper that introduced the surprising description of metric spaces as categories enriched over a certain monoidal category . A lot of people find this very striking when they first see it, and it helps to drive home the point that enriched categories are not just ordinary categories with some extra structure on the hom-sets; in fact the hom-sets don’t have to be sets at all!
Lawvere also intended the paper to serve as an accessible introduction to enriched category theory, so it begins fairly gently with some basic definitions. For the purposes of this post however, I’ll assume the reader has at least seen the definitions of symmetric monoidal closed categories, -categories, and -functors. If not, everything you need can be found on the nlab.
Lawvere begins by describing some of the philosophy behind the paper. He argues that rather than being abstract nonsense that only appears at the highest level of mathematics, category theory can be found even in the most elementary concepts. He mentions the well known examples of posets and groups as categories, and the aim of the paper is to describe another example of an elementary mathematical structure arising from categorical constructions, namely metric spaces.
We’ll also look at posets as enriched categories that are closely related to metric spaces, and this is where the “generalized logic” of the title comes in. The idea is that objects in a monoidal category will be truth values for our generalized logic, morphisms in will be entailments between them, certain functors correspond to logical operations, and adjointness relations between these functors correspond to rules of inference.
We will only consider categories enriched in complete and cocomplete symmetric monoidal closed categories (which I’ll just call “monoidal categories”), and we are particularly interested in two examples. The first is , which has two objects, and , and three morphisms, which we write as entailments: , and . The tensor product is given by conjunction, the unit is and the internal hom is implication.
The hom-tensor adjunction gives a correspondence between judgements and , which is just the deduction theorem from logic. Categories enriched in are simply posets (well, really preorders); we interpret the hom-object as the truth value of the statement , and the composition and identities give us
The category has as objects non-negative reals together with , and has a single morphism precisely when . The tensor product is addition with as the unit, and this forces the internal hom to be truncated subtraction:
but we’ll just write this as . Thus the fact that if and only if can be thought of as somehow generalizing the deduction theorem. The composition and identities in an -category give us
which are familiar as axioms of metric spaces, and this is how we will refer to -categories. This is a weakening of the usual metric space axioms in three ways:
We don’t require that only when . This condition amounts to requiring that isomorphic objects are equal, which is undesirable from a categorical point of view; this is also the reason for dropping antisymmetry of posets. There are naturally occurring examples that don’t satisfy the non-degeneracy condition; perhaps most notably, it makes sense to regard the distance between two measurable functions that are equal almost everywhere as being zero.
We allow . Allowing infinite distances is also quite natural, as it’s easy to imagine spaces where it’s impossible to get from one point to another. For example, this is the most sensible way to think of distances in a discrete space.
We don’t require . Allowing non-symmetry is a more significant shift in what we mean by a metric space, but even so there are natural examples, for example the Hausdorff metric on subsets of a metric space. It’s best to think of the hom-values in a generalized metric space not as representing distances, but representing the least time or effort it takes to get from one point or state to another. When you look at it this way, there’s no reason to assume symmetry (e.g. going up and down a hill are not equally difficult).
There is a monoidal functor sending and , and this induces an inclusion of the category of posets into the category of metric spaces. There is also a monoidal functor , so metric spaces and categories can be seen as generalizing posets in different directions.
Functor categories and Yoneda
A -functor between posets is precisely an order preserving map, and a -functor between metric spaces is a Lipschitz map with Lipschitz constant 1, i.e. a function such that for all and in . For an arbitrary monoidal category and -categories and the functor -category has as objects the -functors , and the hom objects are defined by the end
When , this just gives the ordinary end representation of the set of natural transformations. Since and are both posets, ends reduce to products, which are conjunctions in and suprema in . So for posets, the object of natural transformations between order preserving maps is the truth value of the statement . In other words, order preserving maps are ordered by domination. For metric spaces the hom object is given by . So the space of Lipschitz-1 maps between metric spaces is endowed with the sup metric.
The closed structure of the monoidal category makes itself into a -category. For this gives the obvious interpretation of as a poset. However, the metric on is given by truncated subtraction, rather than the usual . The self-enrichment of means we can define the presheaf -category , and that allows us to define the Yoneda embedding , which sends an object to the representable presheaf . Just as in ordinary category theory, this embedding is full and faithful, which in the case of posets gives:
Proposition. Any poset can be embedded into the poset of downwards closed subsets of (ordered by inclusion), by sending an element to the set of all things .
Here we have used the correspondence between downwards closed subsets and order preserving maps . For metric spaces we have:
Proposition. Any metric space can be isometrically embedded into the space of Lipschitz-1 maps .
Adequacy and density
We say that a -functor is adequate if the composite
of the Yoneda embedding with restriction along is full and faithful. We say that is dense if we have an isomorphism of bimodules . I haven’t yet said what bimodules are, but the important thing is that in the case of metric spaces this becomes the condition that
This terminology is slightly unfortunate, because what Lawvere calls an adequate functor is nowadays called a dense functor, and Lawvere’s notion of density doesn’t have a modern name as far as I’m aware. A functor is dense iff it’s image is dense in the usual metric space sense. Lawvere shows that a dense functor is adequate, at least in the case of metric spaces. A metric space is separable if it admits a dense map from the discrete space on the natural numbers, and this result give us
Proposition. Any separable metric space can be isometrically embedded in the space of sequences of reals endowed with the sup metric.
This space of sequences is not quite as usually defined because of the non-standard metric on .
The comprehension scheme
A(n ordinary) functor is called a discrete opfibration if every morphism is the image under of a unique morphism with domain . There is a correspondence between discrete opfibrations on and functors , and this correspondence is obtained by restricting a certain adjunction to an equivalence. This adjunction can be defined for arbitrary , provided that the unit of is in fact terminal (this gives a way of defining projections from a tensor product to each of the factors, which is not generally possible). I won’t go into the details of how it’s defined, but I’ll describe what it gives for and .
Given an order-preserving map between posets, the left adjoint of this adjunction sends to , defined by setting to be the truth value of the statement . The right adjoint sends to , where is the (upwards closed) subset of on which takes the value , and is the inclusion. If we take to be a discrete poset (i.e. a set) then is just a unary predicate on , and
Lawvere calls the right adjoint of the adjunction the comprehension scheme, and this example shows why.
For metric spaces, the left adjoint sends a Lipschitz-1 map to the function defined by , i.e. the distance from the image of . The right adjoint sends to the inclusion of its vanishing set.
It’s interesting to note that for and , this adjunction restricts to an equivalence between a subcategory of (the discrete opfibrations, and inclusions of upwards closed subsets respectively) and the whole functor category . For however, only those functions that give the distance from a closed subset are invariant under the adjunction, and these correspond to the inclusion of this closed set. Thus purely categorical considerations naturally give rise to the closed sets in as a distinguished class of subsets.
Bimodules and Kan extensions
For -categories and , a bimodule consists of a -functor (the placement of the is not completely agreed upon, but I’ll stick with Lawvere’s convention). We can think of a bimodule as a -category structure on the disjoint union of and , with as the hom object between an object of and an object of , and with all the hom objects in the other direction being the initial object of . The -functoriality of means that we have a “composition” operation , and dually, and that this composition is associative.
There are two special types of bimodule that are particularly important, and they are both induced by -functors. Given a -functor , we define bimodules and by
A morphism between two bimodules is just a -natural transformation between the corresponding -functors . Given bimodules and , we can define the composite bimodule by the coend
and this composition is associative (up to isomorphism). The bimodule given by serves as an identity for this composition, and hence there is bicategory of -categories, bimodules and natural transformations.
Let be the -category with a single object and whose only hom object is the unit object of . Then a bimodule is just an object of , and composition is just the tensor product in . So bimodule composition generalizes the tensor product, and it’s natural to ask whether the internal hom of also generalizes. Since general bimodule composition is not commutative, there are two composition operations (on the left and the right) that could potentially have right adjoints, and in fact they both do, and these are defined by end formulae. If we restrict our attention to modules of the form for a -functor , the operation also has a left adjoint, which is given by , and can also be written explicitly as a coend.
Let be a -functor . Bimodules are just -functors , and the bimodule composite is the bimodule corresponding to the -functor . Thus the left and right adjoint to precomposition with in this case give left and right Kan extensions along , and the formulae for these adjoints reduce to the familiar coend and end formulae for left and right Kan extensions:
When is full and faithful, the Kan extensions really are extensions, in other words if you extend and then restrict, you get back what you started with. So specializing all this to the case gives:
Proposition. Let be a subspace of a metric space , and let be a Lipschitz-1 map from to . Then has both maximal and minimal Lipschitz-1 extensions to the whole of , given by
A particularly interesting example is given when is the space of simple, non-negative functions on a probability space (i.e. positive linear combinations of indicator functions of measurable sets), and is the inclusion into the space of all measurable functions (with the sup metric). If you take to be the integral of the simple function , then the two Kan extensions of give the upper and lower integrals of a measurable function . In particular, is integrable if and only if .
If we think of a map from a poset to as a unary relation or predicate, then the left and right Kan extensions become
If we restrict to the case when and are just sets, so that is an arbitrary function, this gives
and specializing even further to the case when is a product projection we have
So existential and universal quantification are (very) special cases of Kan extensions. This leads Lawvere to use the phrase “Kan quantification” for Kan extensions.
Every -functor gives rise to an adjunction in the bicategory of bimodules, and it’s natural to ask under what conditions does every adjunction arise in this way. Recall that a metric space is (Cauchy) complete if every Cauchy sequence has a limit. A bit of care is needed when making this precise, because the possible non-symmetry of the metric means there are several things it could mean for a sequence to be Cauchy or convergent.
Proposition. A metric space is Cauchy complete if and only if every adjunction of bimodules is induced by a Lipschitz-1 map . In particular, the points of the Cauchy completion of correspond to bimodule adjunctions (where is the one point metric space).
This gives a description of Cauchy complete metric spaces that is purely categorical, so it makes sense to talk about Cauchy complete -categories for arbitrary . It turns out that an ordinary (-enriched) category is Cauchy complete iff all idempotents split, and the Cauchy completion of a ring regarded as a one object category enriched in is the category of finitely generated projective modules.
These days it’s more common to see Cauchy complete categories defined in terms of absolute colimits. I’m not too sure about the history of the concept, but I think the definition Lawvere gives came first, and Street later gave the characterisation in terms of absolute colimits in “Absolute colimits in enriched categories”.
Free -categories
Finally, Lawvere defines a -graph to consist of a set of “vertices” and for every pair of vertices an object of (i.e. like a -category but without composition or identities). A morphism of -graphs is a function and a family of morphisms . There is an evident forgetful functor from to the category of -graphs. This has a left adjoint which sends a -graph to the -category which has the vertices of as objects and hom objects defined by
where the sum runs over all finite sequences of vertices. In the case of metric spaces, this gives the “least-cost” distance:
I’ll finish with a few questions for those more knowledgeable than myself:
I think the only categorical notion in the paper that I hadn’t at least heard of before is Lawvere’s notion of density (i.e. a functor such that ; as noted above this is different from what people usually mean by a dense functor). Does this appear elsewhere in category theory, or is it only interesting for metric spaces?
A lot of the results about metric spaces are very similar to classical results, but are not quite the same because of the non-standard metric on . Is there any way of recovering the classical results without too much work?
The idea of generalized logic is intriguing, but I’m not sure how far you can go with it. Is it possible, for example, to talk about generalized models of a generalized theory?
Re: Metric Spaces, Generalized Logic, and Closed Categories
In the author commentary to the TAC reprint of this article, Lawvere writes:
The converse I certainly believe: see Cauchy complete category. But I’d love to collect explicit examples where category theory influences developments in metric space theory, rather than simply reinterprets known theorems (albeit in a spectacularly elegant way).
Tom, maybe I should specifically direct this question to you? Though I would also be interested in learning about milder influences. For instance, has Lawvere’s suggested relaxation of the axioms for a metric space caught on in any way?