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$-丰富代数理论和单子呈现之间的密切联系。