Birkhoff's variety theorem from Freyd's adjoint functor theorem

2.ならば1.は簡単なので、1.から2.を示す。

$\mathrm{\Sigma }\text{-Alg}$を$\mathrm{\Sigma }$代数とその準同型のなす圏、$\mathcal{K}$をその充満部分圏だと見なす。このとき$\mathcal{K}$は明らかにlocally smallであり、また直積代数と部分代数で閉じていることからsmall completeかつ集合の圏$\text{Set}$への忘却関手が極限を保つ。さらに部分代数で閉じていることから各$(A\downarrow U)$が解集合条件を満たすことも従うので、一般随伴関手定理から左随伴$F:\text{Set}\to \mathcal{K}$が存在。この随伴におけるunitを一つ取り${\eta }^F$とする。

変数の集合を$\text{Var}$とすると随伴から、$\mathcal{K}$の任意のobject$B$への任意のvaluation $J:\text{Var}\to UB$は、${\eta }_{\text{Var}}^F$を通して一意的な準同型$\tilde{J}$で分解できる。

valuation

このとき任意の$\mathrm{\Sigma }\text{-term}$$t$について$[[t]{]}_{B,J}=[[t]{]}_{B,U\tilde{J}{\eta }_{\text{Var}}^F}=\tilde{J}([[t]{]}_{F\text{Var},{\eta }_{\text{Var}}^F})$であるので、$\mathcal{K}$の全てのobjectは次で定義される$\mathrm{\Sigma }$上の公理の集合$E$を満たす。

$$E=\{s=t\mid [[s]{]}_{F\text{Var},{\eta }_{\text{Var}}^F}=[[t]{]}_{F\text{Var},{\eta }_{\text{Var}}^F}\}$$

逆に、任意の$(\mathrm{\Sigma },E)$代数は$\mathcal{K}$に属することを示せば、証明は完了である。

$(\mathrm{\Sigma },E)\text{-Alg}$を$(\mathrm{\Sigma },E)$代数全体のなす$\mathrm{\Sigma }\text{-Alg}$の充満部分圏とする。このとき先ほどと同様に一般随伴関手定理から、忘却関手$\mathcal{U}:\mathcal{K}\to (\mathrm{\Sigma },E)\text{-Alg}$及び$\mathbb{U}:(\mathrm{\Sigma },E)\text{-Alg}\to \text{Set}$は共に左随伴を持つ。集合$A$に対し自由$(\mathrm{\Sigma },E)$代数$\mathbb{F}A$はその構成がよく知られていて、集合$A$の元を0変数関数として言語$\mathrm{\Sigma }$に加えた$(\mathrm{\Sigma }\bigsqcup A)\text{-term}$のうち変数を含まないもの全体の集合の、$E$から誘導される同値関係による剰余からなる。またこのとき${\eta }_A^{\mathbb{F}}$は$a\mapsto [a]$である。

adjoint

今、$U=\mathbb{U}\mathcal{U}$より左随伴の一意性から$F\simeq \mathcal{F}\mathbb{F}$が従うので、以下では$F=\mathcal{F}\mathbb{F}$とする。またこのとき${\eta }^F=(\mathbb{U}{\eta }_{\mathbb{F}}^{\mathcal{F}}){\eta }^{\mathbb{F}}$と取れる。

もし${\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}$が単射でなければ、ある$\mathrm{\Sigma }\text{-term}$$t$,$u$が存在して$[t]\ne [u]$かつ${\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([t])={\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([u])$が成立するが、このとき

$$\begin{array}{rl}[[t]{]}_{F(\text{Var}),{\eta }_{\text{Var}}^F}& =[[t]{]}_{F(\text{Var}),\mathbb{U}{\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}{\eta }_{\text{Var}}^{\mathbb{F}}}\\ & ={\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([[t]{]}_{\mathbb{F}(\text{Var}),{\eta }_{\text{Var}}^{\mathbb{F}}})\\ & ={\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([t])\\ & ={\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([u])\\ & ={\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([[u]{]}_{\mathbb{F}(\text{Var}),{\eta }_{\text{Var}}^{\mathbb{F}}})\\ & =[[u]{]}_{F(\text{Var}),\mathbb{U}{\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}{\eta }_{\text{Var}}^{\mathbb{F}}}\\ & =[[u]{]}_{F(\text{Var}),{\eta }_{\text{Var}}^F}\end{array}$$

が従うので、$E$の定義から$\mathbb{F}\text{Var}$が$(\mathrm{\Sigma },E)$代数であることに矛盾する。したがって${\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}$は単射である。同様に任意の無限集合$S$に対し${\eta }_{\mathbb{F}S}^{\mathcal{F}}$が単射であることを示す。

任意に$\mathbb{UF}S$の元を2つを固定すれば、それらをそれぞれ$[[t]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J}$, $[[u]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J}$と表せるような、$\mathrm{\Sigma }\text{-term}$$t$,$u$及び写像$J:\text{Var}\to S$が自由代数の構成を考えれば存在する。特に$J$が単射であるようなものが存在するので、そのような$J$とそのretraction$s:S\to \text{Var}$を取る。

unit

すると任意の$\mathrm{\Sigma }\text{-term}$$k$に対し、${\eta }_{\mathbb{F}S}^{\mathcal{F}}([[k]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J})=[[k]{]}_{FS,\mathbb{U}{\eta }_{\mathbb{F}S}^{\mathcal{F}}{\eta }_S^{\mathbb{F}}J}=[[k]{]}_{FS,UFJ\mathbb{U}{\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}{\eta }_{\text{Var}}^{\mathbb{F}}}=FJ{\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}([[k]{]}_{\mathbb{F}\text{Var},{\eta }_{\text{Var}}^{\mathbb{F}}})$となる。

今、$UFJ$はsection$UFs$を持つため単射であり、${\eta }_{\mathbb{F}\text{Var}}^{\mathcal{F}}$は既に見たとおり単射なので、${\eta }_{\mathbb{F}S}^{\mathcal{F}}([[t]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J})={\eta }_{\mathbb{F}S}^{\mathcal{F}}([[u]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J})$ならば$[[t]{]}_{\mathbb{F}\text{Var},{\eta }_{\text{Var}}^{\mathbb{F}}}=[[u]{]}_{\mathbb{F}\text{Var},{\eta }_{\text{Var}}^{\mathbb{F}}}$である。さらにこのとき$[[t]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J}=[[t]{]}_{\mathbb{F}S,\mathbb{UF}J{\eta }_{\text{Var}}^F}=\mathbb{F}J([[t]{]}_{\mathbb{F}\text{Var},{\eta }_{\text{Var}}^{\mathbb{F}}})=\mathbb{F}J([[u]{]}_{\mathbb{F}\text{Var},{\eta }_{\text{Var}}^{\mathbb{F}}})=[[u]{]}_{\mathbb{F}S,\mathbb{UF}J{\eta }_{\text{Var}}^F}=[[u]{]}_{\mathbb{F}S,{\eta }_S^{\mathbb{F}}J}$であるから、${\eta }_{\mathbb{F}S}^{\mathcal{F}}$は単射である。

ここまでで任意の無限集合$S$に対し${\eta }_{\mathbb{F}S}^{\mathcal{F}}$が単射であることがわかったので、$\mathcal{K}$は部分代数及び準同型像で閉じていることから$\mathbb{F}S$は全て$\mathcal{K}$に含まれる。さらに左随伴は余極限を保つことから、任意の非空$(\mathrm{\Sigma },E)$代数$A$に対し$\mathbb{F}({\bigsqcup }_{J:\text{Var}\to \mathbb{U}A}\text{Var})$から全射準同型$[\tilde{J}{]}_{J:\text{Var}\to \mathbb{U}A}$が伸び、よって$A$も$\mathcal{K}$に含まれる。

coproduction

最後に空集合だが、空集合が$(\mathrm{\Sigma },E)$代数であることと$\mathrm{\Sigma }$に0変数関数記号が含まれないことが同値なので、空集合は$(\mathrm{\Sigma },E)$代数ならば任意の$(\mathrm{\Sigma },E)$代数の部分代数になるため$\mathcal{K}$に含まれる。

したがって任意の$(\mathrm{\Sigma },E)$代数は$\mathcal{K}$に属するので、$\mathcal{K}=(\mathrm{\Sigma },E)\text{-Alg}$であることがわかった。