bonotakeの日記

元・ソフトウェア工学系研究者、今・AI系エンジニア

Cartesian closed かつ distributive な圏で x × x = x ² を示す

違った方面から攻めてみた。なんか途中。tex の frac を使ったので見づらい。
[tex: \frac{\large X \to^{} A \times A} {\frac{\large X \to^f A \hspace{4em} X \to^g A} {\frac{\large X + X \to^{\[f,g\]} A} {\frac{\large (X \times 1) + (X \times 1) \to^{\[f,g\]} A} {\frac{\large X \times (1+1) \to^{\[f,g\]'} A}{\large X \longrightarrow^{\small curry(\[f,g\]')} A^2}] ただし、 X \times (1 + 1) \simeq (X \times 1) + (X \times 1)
ここから、hom(-,A \times A) \simeq hom(-, A^2)
h = hom(-,A \times A), \hspace{3em} h' = hom(-, A^2) とおくと、米田の補題を使って
I^{op}(A \times A) \simeq nat(h, I^{op}) \simeq  nat(h', I^{op}) \simeq I^{op}(A^2)
(ただし、I^{op} : C \to C^{op} は、対象を保存し、射の向きを反対にするだけの反変関手)。∴  A \times A \simeq A^2



うう、なんか気持ち悪い証明になってしまった…米田の補題など持ち出す必要があったのだろうか。合ってるのか?これは。

注:bonotakeは、amazon.co.jpを宣伝しリンクすることによってサイトが紹介料を獲得できる手段を提供することを目的に設定されたアフィリエイト宣伝プログラムである、 Amazonアソシエイト・プログラムの参加者です。