デカルト圏の等式的定義

そういう事情で、今度は定義を書き写す。もう、二度手間じゃねーか、バカヤロ＞自分

• 参考：等式的双デカルト圏のための等式群 - 檜山正幸のキマイラ飼育記 メモ編
• 参考：トレース付きモノイド圏の対角、一様性など - 檜山正幸のキマイラ飼育記 メモ編

まずは、ランベック／スコット（J.Lambek, P.J.Scott）本P.52 "Cartesian closed categories equationally presented"から引用。さすがに、ランベックだけあって、次のように言っている（強調は檜山）：

A category is a deductive system in which the following equations hold between proofs:

次の記法はオリジナル（ランベック／スコット）と違う。

• 終対象を1と書く。（オリジナルはT）
• Aから終対象への射を!_Aと書く。（オリジナルは○_A）
• 結合はdiagrammatic order

で、デカルト圏の等式的な定義：

1. f = !_A , for all f:A→1
2. <f, g>;π_A,B = f , for all f:C→A, g:C→B
3. <f, g>;π'_A,B = g , for all f:C→A, g:C→B
4. <h;π_A,B, h;π_A,B> = h , for all h:C→A×B

最初の主張を言い換えると：

• id₁ = !₁,
• f;!_B = !_A , for all f:A→B

これらから導かれるもの：

• 分配律 h;<f, g> = <h;f h;g>
• id_A×id_C = id_A×C

ここで、f×g の定義は：

• f×g := <π_A,C;f, π'_A,C;g>

これらから、交替律が出る。

さて一方、"The Maximality of Cartesian Categories" by Kosta Dosen, Zoran Petric （http://arxiv.org/abs/math/9911059）では、次の公理化を採用している。

1. <f, g>;π_A,B = f for all f:C→A, g:C→B
2. <f, g>;π'_A,B = g for all f:C→A, g:C→B
3. h;<f, g> = <h;f h;g> （分配律）
4. <π_A,B, π'_A,B> = id_A×B
5. f = !_A , for all f:A→1

同じ論文で、直積の結合性、対称性、単位性などを示すために、いろいろな自然変換を定義している。これも書き写す。オリジナルと記号法は違う（が、標準的かどうか自信はない）。

1. α_A,B,C := <<π_A,B×C, π'_A,B×C;π_B,C>, π'_A,B×C;π'_B,C> : A×(B×C) → (A×B)×C
2. α'_A,B,C := <π_A×B,C;π'_A,B, <π_A×B,C;π'_A,B, π'_{A×B, C}>> : (A×B)×C → A×(B×C)
3. σ_A,B := <π'_A,B, π_A,B> : A×B → B×A
4. Δ_A := <id_A, id_A> : A → A×A
5. λ_A := <!_A, id_A> : A → 1×A
6. ρ_A := <id_A, !_A> : A → A×1

これらを用いて、(A×B, π_A,B, π'_A,B) が直積対象、射影システムであること（普遍性）を示す。その他の自然変換（射の族）も使って、×がモノイド積であることを示す。