观念
代数的最初意义是对运算与等式的研究. 一个代数理论就是若干种运算和这些运算之间的若干条等式. 代数理论的模型就是一个集合 (或一般范畴的对象) 上带有指定的运算, 满足指定的等式.
一种更抽象的视角是, 运算和等式不过是一个具有有限乘积 (有限极限) 的范畴的表现. 故代数理论可 “无坐标” 式地定义为这样的一个范畴, 这个范畴就是它的语法范畴. 而该理论的模型则是语法范畴到 $\mathsf{Set}$ (或一般范畴) 的保持结构的函子.
还有另一个方向的抽象. 代数理论 $\mathcal T$ 给出一个记录了所有运算与等式的 “自由代数” 函子 $F\colon \mathsf{Set}\to\mathsf{Set}$, 而 $\mathcal T$ 的模型可视为映射 $FX\to X$, 表达了所有运算在 $X$ 上这一具体结构中的求值. 沿这一思路可以继续推广得到单子上的代数的概念.
定义
通过语法
一个代数理论的语法是如下资料:
- 若干个类型;
- 若干个函数符号, 每个函数符号有有限个输入类型和一个输出类型; (输入类型的个数称为元数, $0$ 元函数称为常量)
- 若干条等式, 每个等式的两端由各类型的变量以及函数符号构成.
给定上述语法资料, 可以生成一个语法范畴:
- 其对象为变量的序列, 每个变量有一个类型;
- 态射为变量代换, 新的变量是依赖于旧的变量的公式 (由旧变量与函数符号组合而成).
通过语法范畴
一个代数理论 (的语法范畴) 是一个具有有限积的范畴 $\mathcal T$.
若范畴 $\mathcal T$ 中有一个对象 $x$ 使得每个对象都形如 $x^n$ ($n\in\mathbb{N}_{\geq 0}$), 则称之为单类型 (simgle-sorted) 代数理论.
单类型代数理论又称为 Lawvere 理论.
例
幺半群
幺半群指的是积幺半范畴中的结合代数, 它是一种非常有代表性的代数理论.
幺半群的代数理论的语法范畴如下:
- 其对象为有限集;
- 态射 $\{x_1,\cdots,x_n\}\to \{y_1,\cdots,y_m\}$ 为形如 $y_i = f_i(x_1,\cdots,x_n)$ 的变量代换, 每个 $f_i$ 为幺半群的理论中的公式, 即 $\{x_1,\cdots,x_n\}$ 上的一个列表; 等价地, 一个态射是 $\{y_1,\cdots,y_m\}$ 到 $\{x_1,\cdots,x_n\}$ 生成的自由幺半群的一个集合映射.
性质
自由–遗忘伴随
对于单类型代数理论 $\mathcal{T}$, 有自由–遗忘伴随
$$
U\colon \mathsf{Alg}_{\mathcal{T}} \leftrightarrows \mathsf{Set} \colon F,
$$
其中自由函子 $F$ 为
$$
F(X) = \bigcup_{n\geq 0} X^n\times\operatorname{Hom}_{\mathcal T}(x^n,x).
$$
自由与遗忘的复合 $UF\colon\mathsf{Set} \to \mathsf{Set}$ 是一个单子, 而 $\mathcal T$-代数等同于该单子上的代数. 换言之, 上述伴随是单子性的.
特别地, $\mathcal{T}$ 的始代数, 即 $\mathsf{Alg}_{\mathcal{T}}$ 的始对象, 是由空集自由生成的 $\mathcal{T}$-代数 $F(0) = \operatorname{Hom}_{\mathcal{T}}(1,x)$.
值得注意的是, 考虑一个新的代数理论 $\mathcal{T}[X]$, 其语法为 $\mathcal{T}$ 的语法加上 $X$ 的每个元素作为常量; 那么集合 $X$ 上的自由代数 $F(X)$ 也可理解为 $\mathcal{T}[X]$ 的始代数, 即空集自由生成的 $\mathcal{T}[X]$-代数.