Non-cartesian closedness of Met
Let Met denote the category of metric spaces and nonexpansive maps. It's well known that if we equip the product of two metric spaces with the L_{\infty} metric (the max of the distances in the two coordinates), we get categorical products in Met; alternatively, if we impose the L_1 metric on the product (the sum of the two coordinate distances), we get a monoidal closed structure, at least if we weaken the usual definition of a metric by allowing metrics to take the value \infty. It's intuitively obvious that the cartesian monoidal structure on Met can't be closed. But I've never (until I wrote one down today!) seen a formal proof of this; does anyone know if it exists anywhere in the literature? My proof is not particularly elegant: it amounts to showing that a particular coequalizer in Met is not preserved by a functor of the form (-) x Y. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Hi Peter, If Met is a CCC, then [X,Y] has as elements all morphisms from X to Y (use the adjoint transposes of morphisms from 1 to [X,Y]). And the distance of morphisms f,g is sup_x d(fx,gx) (use the adjoint transposes of morphisms from two-element spaces to [X,Y]). However, addition of real numbers is not nonexpansive from R x R to R, although its curred form from R to [R,R] is. This is a contradiciotn. Best regards, Jiri On Fri, 16 Dec 2022, ptj@maths.cam.ac.uk wrote:
Let Met denote the category of metric spaces and nonexpansive maps. It's well known that if we equip the product of two metric spaces with the L_{\infty} metric (the max of the distances in the two coordinates), we get categorical products in Met; alternatively, if we impose the L_1 metric on the product (the sum of the two coordinate distances), we get a monoidal closed structure, at least if we weaken the usual definition of a metric by allowing metrics to take the value \infty.
It's intuitively obvious that the cartesian monoidal structure on Met can't be closed. But I've never (until I wrote one down today!) seen a formal proof of this; does anyone know if it exists anywhere in the literature? My proof is not particularly elegant: it amounts to showing that a particular coequalizer in Met is not preserved by a functor of the form (-) x Y.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Peter, we don't have such an example in the paper. Our argument used the cartesian closed category of "metric spaces without triangular inequality", and showed that, for a metric space X, all exponential Y^X (Y metric) taken in that category satisfy the triangular inequality if and only if X satisfies that condition. Best regards Dirk On 16 December 2022 at 22:05 GMT+0000, ptj@maths.cam.ac.uk wrote ...
Dear Dirk, dear Maria Manuel,
That's very interesting, and I should have remembered it. But did your argument come up with an explicit example of a colimit in Met not preserved by a functor of the form (-) x Y ?
I suppose I'll have to go and read your paper!
Best regards, Peter
On Dec 16 2022, Dirk Hofmann wrote:
Dear Peter,
in our paper
- Clementino, M. M., & Hofmann, D. (2006). Exponentiation in $V$-categories. Topology and its Applications, 153(16), 3113–3128.
we give a characterisation of exponentiable metric spaces. The result essentially states that a metric space (in the sense of Lawvere) is exponentiable if and only if "there is always a point in the middle", that is, whenever d(x,z)=u+v, then there is a point y with d(x,y)≤u+ε and d(y,z)≤v+ε. A finite metric space with a non-trivial distance cannot be exponentiable.
Best regards Dirk
On 16 December 2022 at 16:41 GMT+0000, <ptj@maths.cam.ac.uk> wrote ...
Let Met denote the category of metric spaces and nonexpansive maps. It's well known that if we equip the product of two metric spaces with the L_{\infty} metric (the max of the distances in the two coordinates), we get categorical products in Met; alternatively, if we impose the L_1 metric on the product (the sum of the two coordinate distances), we get a monoidal closed structure, at least if we weaken the usual definition of a metric by allowing metrics to take the value \infty.
It's intuitively obvious that the cartesian monoidal structure on Met can't be closed. But I've never (until I wrote one down today!) seen a formal proof of this; does anyone know if it exists anywhere in the literature? My proof is not particularly elegant: it amounts to showing that a particular coequalizer in Met is not preserved by a functor of the form (-) x Y.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Jirka, That's an interesting idea, but I'm having difficulty making it work in practice. It seems to me that the most you can get from considering morphisms from 2 is that the metric on [X,Y] must satisfy d(f,g) \geq sup_x d(fx,gx) -- to get the reverse inequality you would need to impose the L_1 metric on the product 2 x X. And that inequality is the wrong way round for showing that the transpose of addition on R is nonexpansive. Best regards, Peter On Dec 16 2022, Jirí Adámek wrote:
Hi Peter,
If Met is a CCC, then [X,Y] has as elements all morphisms from X to Y (use the adjoint transposes of morphisms from 1 to [X,Y]). And the distance of morphisms f,g is sup_x d(fx,gx) (use the adjoint transposes of morphisms from two-element spaces to [X,Y]).
However, addition of real numbers is not nonexpansive from R x R to R, although its curred form from R to [R,R] is. This is a contradiciotn.
Best regards, Jiri
On Fri, 16 Dec 2022, ptj@maths.cam.ac.uk wrote:
Let Met denote the category of metric spaces and nonexpansive maps. It's well known that if we equip the product of two metric spaces with the L_{\infty} metric (the max of the distances in the two coordinates), we get categorical products in Met; alternatively, if we impose the L_1 metric on the product (the sum of the two coordinate distances), we get a monoidal closed structure, at least if we weaken the usual definition of a metric by allowing metrics to take the value \infty.
It's intuitively obvious that the cartesian monoidal structure on Met can't be closed. But I've never (until I wrote one down today!) seen a formal proof of this; does anyone know if it exists anywhere in the literature? My proof is not particularly elegant: it amounts to showing that a particular coequalizer in Met is not preserved by a functor of the form (-) x Y.
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Peter, can you generalize your argument to a necessary and sufficient condition on V such that the usual closed structure on V-Cat is cartesian? This is of interest for its applicability to models of concurrent computation, as follows. My group's 1989 paper "Temporal Structures", http://boole.stanford.edu/pub/man90.pdf presented at CTCS-89 in Manchester and later in journal form as Mathematical Structures in Computer Science, Volume 1:2, 179-213 (July 1991), had the following abstract. "We combine the principles of the Floyd-Warshall-Kleene algorithm, enriched categories, and Birkhoff arithmetic, to yield a useful class of algebras of transitive vertex-labeled spaces. The motivating application is a uniform theory of abstract or parametrized time in which to any given notion of time there corresponds an algebra of concurrent behaviors and their operations, always the same operations but interpreted automatically and appropriately for that notion of time. An interesting side application is a language for succinctly naming a wide range of datatypes." A little later I noticed that the structures treated there were starting to look like those in Girard's recent (1986) work on linear logic, and wrote about that as Section 5 in my CONCUR-92 paper "The Duality of Time and Information", http://boole.stanford.edu/pub/dti.pdf. (I like to think of Ecclesiastes 9:11, "but time and chance happeneth to them all" as an early appearance of that duality via Shannon's statistical view of information, and the bras and kets of quantum mechanics as a later one.) The idea of orthocurrence (the monoid in a closed monoidal category) as interaction, and its adjoining closed structure as observation, is spelled out more explicitly in a talk I gave at an IJCAI'01 workshop on spatial and temporal reasoning in Seattle in 2001 organized by NSF's Frank Anger. Slides (cryptic): http://boole.stanford.edu/pub/ijcaitalk.pdf Paper (detailed): http://boole.stanford.edu/pub/ortho.pdf, unpublished but later incorporated into Paper (far more detailed): http://boole.stanford.edu/pub/seqconc.pdf What got me into all this in the beginning was noticing in the mid-1980s that in the obvious generalization of ordered time (Pos) to real time (Met), the closed monoidal structure ceased to be cartesian and the single operation of orthocurrence now split into two monoids, one closed and the other cartesian. That's when I noticed the similarity to Girard's linear logic, which had made the same split independently and at the same time but for a totally different application, substructural logic. The connection was completed once I'd figured out the duality of time and information as in Ezekiel 9:11. For Vineet Gupta's thesis in 1991 I suggested choosing between that duality and cubical complexes as a geometric model of concurrency. After looking at both for a month Vineet picked the former. At POPL'91 Boris Trakhtenbrot asked me at question time how the two could be connected, which I was unable to do until realizing (too late for Vineet who'd finished his thesis by then) that Chu(Set,3) provided the edges, faces, etc. of the cubical complexes by interpreting 3 as {0, 1/2, 1} with each face's dimension given by the number of 1/2's (transitions) appearing in it. Vaughan Pratt [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
Dear Peter, Thanks for pointing out that my argument has been incomplete. Here is a proof that Met is not a ccc: We use that limits in Met are the limits in Set with the supremum metric (coordinate-wise). Let us denote by Met(X,Y) the hom-sets with the supremum metric d'(f,g) = sup_x d(fx,gx). The addition of real numbers from RxR to R is not non-expanding, but its curried from R to Met(R,R) is; thus all we need to do is to show that if Met were a ccc, one could take [X,Y]=Met(X,Y). The underlying set of [X,Y] can be taken to be the hom-set, using adjoint transposes of morphisms from 1 to [X,Y]. And the universal morphism eval:[X,Y]xX -> Y can be taken to be the evaluation map (precompose it with morphisms fxX for f:1->[X,Y]). The metric d of [X,Y] satisfies d \geq d', using adjoint transposes of morphisms from 2-element spaces to [X,Y]. To prove d \leq d', we first consider a finite space X. Let id: n->X be the identity map from the discrete space on the underlying set of X, a coproduct of n copies of 1. Then [id,Y]: [X,Y]->[n,Y]= Y^n demonstrates that d= d'. For X arbitrary, express it as a directed colimit X=colim X_i of all finite subspaces X_i. Then [X,Y] = lim [X_i,Y] carries the supremum metric. Best regards, Jiri [For admin and other information see: http://www.mta.ca/~cat-dist/ ]
participants (4)
-
Dirk Hofmann -
Jirí Adámek -
ptj＠maths.cam.ac.uk -
Vaughan Pratt