単項式関手のあいだのホムセット - (2nd) 檜山正幸のキマイラ飼育記

$\require{color} \newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }% \newcommand{\Using}{\quad \Keyword{Using } }% \newcommand{\mrm}[1]{\mathrm{#1} }$ ダイアグラム・チェイシング（図式に沿った要素の追跡）の代わりに、集合のあいだの同型を使う。

記法を簡単にするために、 ${\bf Poly}$ のホムセットをブラケットで $[-, -]$ 、集合圏の内部ホム〈指数 | 関数集合 | アロー型〉をベキ〈累乗〉形式 $-^-$ で書く。

まず、集合圏の指数法則：

$\text{Cartesian pair }:\: (B\times C)^A \cong B^A \times C^A\\ \quad (B\times C)^A \ni f \mapsto (f;\pi^1, f;\pi^2) \in B^A \times C^A \text{ and inverse}\\ \text{unCurrying }:\: (C^A)^B \cong C^{A\times B}\\ \quad (C^A)^B \ni \lambda\,b.\lambda\, a.f(a, b) \mapsto \lambda\,(a, b).f(a, b) \in C^{A\times B} \text{ and inverse}$

シグマ型とパイ型（依存型理論の言葉、圏論では余極限と極限）は次のように書く。

$\quad \sum_{x\in X}F(x)\\ \quad \prod_{x\in X}F(x)$

$F(x)$ が $x$ に依存しない定数のときは：

$\text{sigma to prod }:\: \sum_{x\in X}A \cong X\times A\\ \text{prod to sigma }:\: X\times A \cong \sum_{x\in X}A \:\text{ (inverse of 'sigma to prod')}\\ \text{pi to exp }:\: \prod_{x\in X}A \cong A^X$

ホム双関手は、第一変数に関して反変余連続（余極限を極限に移す）、第二変数に関して連続（極限を極限に移す）だから：

$\text{cocont }:\: [\sum_{x\in X}F(x), B] \cong \prod_{x\in X}[F(x), B]\\ \text{cont }:\: [A, \prod_{y\in Y}G(y)] \cong \prod_{y\in Y}[A, G(y)]$

米田の補題は：

$\text{Yoneda }:\: [y^A, F(y)] \cong F(A)$

以上を使って計算する。

$\quad [By^A, Dy^C]\\ = [B\times y^A, Dy^C]\\ \Using \text{prod to sigma} \\ \cong [\sum_{b\in B}y^A, Dy^C]\\ \Using \text{cocont} \\ \cong \prod_{b\in B}[y^A, Dy^C]\\ \Using \text{Yoneda} \\ \cong \prod_{b\in B} DA^C\\ \Using \text{pi to exp} \\ \cong (DA^C)^B\\ = (D \times A^C)^B \\ \Using \text{Cartesian pair} \\ \cong D^B \times (A^C)^B \\ \Using \text{unCurrying} \\ \cong D^B \times A^{C\times B} \\ \cong D^B \times A^{B\times C}$

したがって、

$\quad {\bf Poly}(By^A, Dy^C) \cong \mrm{Map}(B, D)\times \mrm{Map}(B\times C, A)$