Extending $Set$-functors to Lawvere metric spaces

--- tags: seminar, maths, blute, ottawa, Coalgebras over Lawvere metric spaces --- [Part of a presentation on Coalgebras over Lawvere Metric Spaces](https://hackmd.io/@alexhkurz/HkzAdwlAF) # Extending $Set$-functors to Lawvere metric spaces ## Idea In order to extend a set-functor $T$ to a functor $\overline T$ on metric spaces, the idea is simply to define $\overline T$ in the diagrams below as left Kan extensions: ![](https://hackmd.io/_uploads/rJGGH_OCt.png) On the left, we start from a set-functor $T$, on the right we do the same, but now with a given metric on $TX$. **Example:** We have seen the example of $\Omega=2$ and $T=\mathcal P$. In that case, $\Omega$-cat is the category of preorders and on the left we get the bisimulation-order. On the right, if we order $T$ by inclusion, we get the forward-simulation order and if we order $T$ by reverse inclusion, we get the backward-inclusion order. If we quotient preorders to posets, these functors are known, respecitively, as the convex powerset, the upset functor and the downset functor. Mathematical work goes into the following. - The left Kan extensions exist. - Identify the colimits needed to compute the Kan extension. - Characterise those functors $\overline T$ that arise as Kan extensions. - Compute the $\Omega$-catification in interesting examples. The central issue here is item 2. In terms of [Kelly](http://www.tac.mta.ca/tac/reprints/articles/10/tr10.pdf), Theorem 5.19, we need to find a **density presentation** of $D:Set\to\Omega$-cat. [^dense] The density presentation in the case of $\Omega=2$ is easily described and that is what we turn to now. ## Preorders and Posets: $\Omega=2$ We first treat the special case $\Omega=2$ (see Theorem 4.3 in [Positive Fragments of Coalgebraic Logics](https://arxiv.org/pdf/1402.5922.pdf)). We write $Ord$ to stand for either the category of preorders or the category of posets. **Theorem:** $D:Set \to Ord$ is dense. While the details need some development, the essence of the argument is simple: Every order is a certain enriched (or weighted or indexed) colimit, known as a *coinserter*, of discrete orders (sets). A coinserter is similar to a coequaliser, but, intuitively, quotienting wrt a preorder rather than an equivalence relation. **Definition:** The **coinserter** of $(f,g)$ is an arrow $h$ which is universal wrt $hf\le hg$. **Lemma:** Let $X=(X_0,\le)$ be an order and represent $(X_0,\le)$ as the pair of projections $\pi_1,\pi_2:{\le}\to X_0$ in $Set$. Then $X$ is the coinserter of ($\pi_1,\pi_2$) in $Ord$. The left Kan extension $\overline TX$ is now the coinserter of $(T\pi_1,T\pi_2)$. **Theorem:** The left Kan extension of $T$ is the given by the coinserter of the pair $T\pi_1,T\pi_2: T({\le})\to T(X_0)$. **Example:** The theorem makes it easy to verify that the three powerset functors in the section on [ordered coalgebras](https://hackmd.io/@alexhkurz/ryji9lZRY) are left Kan extensions. **Example:** The posetification $\overline{\mathcal D}$ of the finitely supported probability distribution functor $\mathcal D$ maps a partial order $(X,\leqslant_X)$ to the set of distributions on $X$, ordered by $p\sqsubseteq q$ iff $p[U]\leqslant q[U]$ for all upward closed subsets $U\subseteq X$. *Proof (Sketch):* We have $p\sqsubseteq q$ if there is a distribution $w$ on $\leqslant_X$ such that $\mathcal D\pi_1(w)=p$ and $\mathcal D \pi_2(w) = q$, denoting by $\pi_i$ the projections ${\leqslant_X}\to X$. That this implies $p[U]\leqslant q[U]$ is easily checked. For the converse, we adapt the argument of (De Vink and Rutten, 1999) by setting up a flow network so that the existence of $w$ is equivalent to the existence of a flow of 1. We then use $p[U]\leqslant q[U]$ to show that there is a minimal cut of 1, which in turn implies the existence of a maximal flow of 1 due to the max-flow-min-cut theorem. ## General $\Omega$ The general case combines two ideas we have seen before. - Every order is a coinserter of sets. - Every $\Omega$-cat is a relational presheaf, or multi-order. Our aim is to define a notion of multi-coinserter, or $\Omega$-coinserter, so that we can prove **Lemma:** Every $\Omega$-cat is the $\Omega$-coinserter of a diagram in $Set$. Technically, a coinserter is a weighted colimit consisting of a pair $(f,g):A\to B$ and weights $\phi(B)=\{\ast\}$ and $\phi(A)=2=\{0<1\}$ such that $\phi(f)(\ast)=0$ and $\phi(g)(\ast)=1$. Given an $\Omega$-cat $X$ with underlying set $X_0$ and "multi-orders" $X_r=\{(x',x) \mid r\ge X(x',x)\}$, we build a diagram with pairs $$\delta_0^r,\delta_1^r:X_r\to X_0$$ and weights $\phi(0)=\{\ast\}$ and $\phi(r)=2_r$ and $\phi(\delta_0^r)(\ast)=0$ and $\phi(\delta_1^r)(\ast)=1$. Comparing the weights of a coinserter with the weights of an $\Omega$-coinserter, the only difference is that in $2_r$ the distance from 0 to 1 is not [^e] $e$ but $r$, to quote from the paper: ![](https://hackmd.io/_uploads/HJG56-F0t.png) [^e]: Recall that $e$ is the neutral element of the quantale. While this idea is straightforward, unfortunately the details are tricky and require the patience to unfold the definition of weighted limits which is opaque at first sight (quoting from Kelly, page 38):[^weighted] ![](https://hackmd.io/_uploads/Bk7E1MFRK.png) [^weighted]: $\mathcal V$ is $\Omega$, $F$ is the weight, $G:\mathcal K\to \mathcal B$ is the diagram and $F\star G$ the weighted colimit. ## Examples **Example:** Extending the powerset functor to metric spaces gives the familiar Hausdorff metric: ![](https://hackmd.io/_uploads/rJW6eGYAK.png) which is equivalent to (under suitable conditions on the quantale $\Omega$) ![](https://hackmd.io/_uploads/SJcGZzFRt.png) **Question:** What do we get if we extend the distribution functor to metric spaces? [^dense]: $D:\mathcal A\to \mathcal C$ is dense if the left Kan extension of $D$ along $D$ is the identity (Kelly, Theorem 5.1). This roughly means that every object in $\mathcal C$ is a colimit of a diagram in $\mathcal A$. Examples: - The one-elment set is dense in Set. - The finitely presentable objects are dense in a locally finitely presentable category. - The finitely generated free algebras are dense in a variety (= category of algebras defined by finitary operations and equations). - The Kleisli category is dense in the category of Eilenberg-Moore algebras of a monad. The importance of enriched category theory can partly be explained by the fact that there are more enriched colimits. For example, the ordinary functor $Set\to Pos$ is not dense but the enriched functor $Set\to Pos$ is dense. ## References For the claim on the distribution functor I used - Erik P. de Vink, Jan J. M. M. Rutten: [Bisimulation for Probabilistic Transition Systems: A Coalgebraic Approach](https://www.sciencedirect.com/science/article/pii/S0304397599000353?via%3Dihub). Theor. Comput. Sci. 221(1-2): 271-293 (1999) The main reference for this section are for the special case of $\Omega=2$ - A Balan, A Kurz, J Velebil: **[Positive Fragments of Coalgebraic Logics](https://lmcs.episciences.org/1594)**. Logical Methods in Computer Science, Vol. 11(3:18)2015, pp. 1–51 [(pdf)](https://arxiv.org/pdf/1402.5922.pdf). and for the case of a general quantale - Adriana Balan, Alexander Kurz, Jiri Velebil: [Extending set functors to generalised metric spaces](https://lmcs.episciences.org/5132/pdf). Logical Methods in Computer Science 15(1) (2019). ([pdf](https://lmcs.episciences.org/5132/pdf))