一句话:证明集合自函子可典范扩展为广义度量空间上的自函子,并用左 Kan 扩展计算实例与终余代数。
论文研究如何把集合上的类型构造子(自函子 T)提升到交换 quantale V 丰富的 V-cat,即广义度量空间与非扩张映射范畴。作者证明存在典范扩展 T_V,从而使同一递归域方程 X≅TX 可在集合与度量空间等不同范畴中求解,并通过 change of base 研究其终余代数之间的关系。数学核心是证明离散函子 D:Set→V-cat 是 V-cat-dense 且具有密度表示,由此可沿 D 计算左 Kan 扩展。该证明给出具体实例的显式计算方法,涵盖 Pompeiu-Hausdorff 度量并产生新例子。此为 CALCO 2015 论文扩展版,新增 2.4、3.3 节,共 57 页,被 LMCS 接收。
For a commutative quantale $\mathcal{V}$, the category $\mathcal{V}-cat$ can be perceived as a category of generalised metric spaces and non-expanding maps. We show that any type constructor $T$ (formalised as an endofunctor on sets) can be extended in a canonical way to a type constructor $T_{\mathcal{V}}$ on $\mathcal{V}-cat$. The proof yields methods of explicitly calculating the extension in concrete examples, which cover well-known notions such as the Pompeiu-Hausdorff metric as well as new ones. Conceptually, this allows us to to solve the same recursive domain equation $X\cong TX$ in different categories (such as sets and metric spaces) and we study how their solutions (that is, the final coalgebras) are related via change of base. Mathematically, the heart of the matter is to show that, for any commutative quantale $\mathcal{V}$, the `discrete' functor $D:\mathsf{Set}\to \mathcal{V}-cat$ from sets to categories enriched over $\mathcal{V}$ is $\mathcal{V}-cat$-dense and has a density presentation that allows us to compute left-Kan extensions along $D$.Comment: 57 pages; extended version of the paper presented at CALCO 2015; accepted for publication in LMCS; Sections 2.4 and 3.3 were added
@article{paperbot834,
title = {Extending set functors to generalised metric spaces},
author = {Adriana Balan and Alexander Kurz and Jiří Velebil},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 1},
year = {2019},
doi = {10.23638/lmcs-15(1:5)2019}
}