依赖排序代数理论的幺半范畴 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 理论”。

有限极限理论的概念

广义代数理论和上下文范畴

一个正确类型化的变量列表（在某种意义上需要精确说明，例如在每种情况下前面的 ⊢）被称为上下文。通过使用术语序列来给出适当的态射定义，上下文可以像构建与等式理论相关的劳弗理论一样组装成一个范畴。

理论的张量积

本文的贡献

2 广义代数理论的张量积

在阅读本节时，读者被邀请将构造的每一步与 §3 中的例子进行比较，特别是严格双范畴理论 (3.1)，因为它展示了一般定义中存在的许多特征。

2.1 来自判断对的表达式

我们请读者参考附录中我们下面使用的句法结构的定义——排序和项字母表、排序/项表达式、高度函数、项的规范排序等。

2.3 两个理论的张量积（作为预理论）

原文链接：https://www.arxiv.org/pdf/2511.13547