Classical multi-sorted equational theories and their free algebras have been fundamental in mathematics and computer science. In this paper, we present a generalization of multi-sorted equational theories from the classical ($Set$-enriched) context to the context of enrichment in a symmetric monoidal category $V$ that is topological over $Set$. Prominent examples of such categories include: various categories of topological and measurable spaces; the categories of models of relational Horn theories without equality, including the categories of preordered sets and (extended) pseudo-metric spaces; and the categories of quasispaces (a.k.a. concrete sheaves) on concrete sites, which have recently attracted interest in the study of programming language semantics. Given such a category $V$, we define a notion of $V$-enriched multi-sorted equational theory. We show that every $V$-enriched multi-sorted equational theory $T$ has an underlying classical multi-sorted equational theory $|T|$, and that free $T$-algebras may be obtained as suitable liftings of free $|T|$-algebras. We establish explicit and concrete descriptions of free $T$-algebras, which have a convenient inductive character when $V$ is cartesian closed. We provide several examples of $V$-enriched multi-sorted equational theories, and we also discuss the close connection between these theories and the presentations of $V$-enriched algebraic theories and monads studied in recent papers by the author and Lucyshyn-Wright.
翻译:经典的多类等式理论及其自由代数在数学和计算机科学中具有基础性地位。本文从经典($Set$丰富)语境出发,将多类等式理论推广到在$Set$上拓扑的对称幺半范畴$V$的丰富语境中。此类范畴的典型例子包括:拓扑空间与可测空间的各种范畴;关系型Horn理论(无等式)的模型范畴,包括预序集范畴与(扩展)伪度量空间范畴;以及具体站点上的拟空间(也称具体层)范畴——后者近期在编程语言语义学研究中备受关注。针对此类范畴$V$,我们定义了$V$-丰富多类等式理论的概念。我们证明每个$V$-丰富多类等式理论$T$均存在一个底层的经典多类等式理论$|T|$,且自由$T$-代数可通过恰当提升自由$|T|$-代数而获得。我们建立了自由$T$-代数的显式具体描述,当$V$为笛卡尔闭范畴时该描述具有便捷的归纳特征。文中给出了若干$V$-丰富多类等式理论的实例,并讨论了这些理论与作者及Lucyshyn-Wright近期论文中研究的$V$-丰富代数理论与单子呈现之间的紧密联系。