依赖排序代数理论的幺半范畴 I：语法|上下文|代数理论|广义|张量|等式|语法

A monoidal category of dependently sorted algebraic theories I: syntax

依赖排序代数理论的幺半范畴 I：语法

https://arxiv.org/abs/2511.13547

摘要

这是成对论文中的第一篇，我们在其中构建并研究广义代数理论范畴（按卡特梅尔的意义）上的闭合幺半结构。

在本文中，作为起点，我们定义了两个广义代数理论 A 和 B 之间的张量积 A ⊗ B。这是通过一个算法以语法方式完成的，该算法递归地使用 A 和 B 的公理来生成 A ⊗ B 的公理。我们提供了由我们的构造所恢复的已知结构的例子，例如劳威尔理论的张量积、“细胞”积（依赖类型签名的积），以及图和展示结构的理论。将在第二卷中验证，正如这些特殊情况所提示的，对于某些上下文范畴 Mod(A) 和 Mod(B)（其底层范畴分别等价于 Mod(A, Fam) 和 Mod(B, Fam)），族值模型范畴 Mod(A ⊗ B, Fam) 同构于 Mod(A, Mod(B)) 和 Mod(B, Mod(A))。此外，张量积的细胞结构是通过结合两个理论的推出积操作获得的。

我们还构造了一个函子 ⊗{A,B} : C(A) × C(B) → C(A ⊗ B)，用于比较相关的上下文范畴，并描述形如 (A ⊗ B) ⊗ C ≅ A ⊗ (B ⊗ C) 和 A ⊗ B ≅ B ⊗ A 的同构。在后续论文中，我们将描述 ⊗{A,B} 的一种泛性质，这将诱导张量积的函子性，从而允许我们验证幺半范畴条件。

1 引言

数学中使用的许多种代数结构，例如群、环以及给定域上的向量空间，都可以被描述为等式理论的模型：它们可以通过一组运算符号和一组由运算符号与变量递归构建的表达式对之间的方程来指定。对这类结构的研究是经典泛代数的主要主题，该领域由 A. N. Whitehead、G. Birkhoff 等人从 19 世纪末至 20 世纪上半叶发展而来。1963 年，在他的博士论文（重印版见 [Law04]）中，W. Lawvere 通过展示等式理论及其语义如何能通过某一特定类别的范畴进行编码，重新阐述了该主题的基础；这些理论最初被称为“代数理论”（algebraic theories），后来也被称为“Lawvere 理论”。