圏の定義
from 射の定義
圏の定義
Wolframでの定義
>A category consists of three things:
>a collection of objects,
>for each pair of objects a collection of morphisms (sometimes call "arrows") from one to another,
>and a binary operation defined on compatible pairs of morphisms called composition.
p.12
この「射の集まり」を「射の類」と呼んでました
恒等射がなんで付け加えられてるんだろう
Category -- from Wolfram MathWorldでは射の従うべき条件に恒等射がある
なるほど、並べ方が違うだけで内容は同じか
なるほど～
定義上は対象が先なのか
概念上は対象より射のほうが重要と聞いたことがある
1. 対象の集まり
これを{\rm ob}(\mathscr{A})と表記する
「Aが圏\mathscr Aの対象である」ことをA\in{\rm ob}(\mathscr A)と書く
これを\mathscr A(A,B)と表記する
\mathscr A(A,B)は圏の対象の数だけ無数に存在する
「fが圏\mathscr AのAからBへの射である」ことをf\in\mathscr A(A,B)と書く
\mathscr A(B,C)\times\mathscr A(A,B)\ni (f,g)\xmapsto{\circ}f\circ g\in\mathscr A(A,C)
圏の対象の数だけ無数に存在する
4. \forall A\in{\rm ob}(\mathscr A)についてAの恒等射{\rm id}_A\in\mathscr A(A,A)
これは恒等射の存在則\forall A\in{\rm ob}(\mathscr A).\mathscr A(A,A)\neq\varnothingとして単位法則と合体させたほうがスッキリすると思う
結合法則：\forall h\in\mathscr A(C,D)\forall g\in\mathscr A(B,C)\forall f\in\mathscr A(A,B).(h\circ g)\circ f=h\circ(g\circ f)
単位法則：\forall f\in\mathscr A(A,B).f\circ{\rm id}_A=f={\rm id}_B\circ f
\forall A,B,A',B'\in{\rm ob}(\mathscr A).\mathscr A(A,B)\cap\mathscr A(A',B')\neq\varnothing\implies A=A'\land B=B'
射の集まりは交わりを持たない
不注意に集合論の記号を使ってしまっているが、まあ言いたいことは伝わるだろう
つまり、上の条件を満たすなら、どんなものを対象や射にしてもま～～～～～ったく問題ない
「4\land単位法則」の代わりに、単位元の存在を導入しても(おそらく)差し支えない
単位元の存在：\forall A\in{\rm ob}(\mathscr A)\exist i\in\mathscr A(A,A)\forall B\in{\rm ob}(\mathscr A)\forall f\in\mathscr A(A,B)\forall g\in\mathscr A(B,A).f\circ i=f\land i\circ g=gー(4*)
以下、圏の定義にはこの条件を用いることにする
(4*)から、iが一意であることを示せる
(4*)
\implies(4*)\land\forall A\in{\rm ob}(\mathscr A)\forall i,i'\in\mathscr A(A,A).
\begin{dcases}\forall B\in{\rm ob}(\mathscr A)\forall f\in\mathscr A(A,B)\forall g\in\mathscr A(B,A).f\circ i=f\land i\circ g=g\\\forall B\in{\rm ob}(\mathscr A)\forall f\in\mathscr A(A,B)\forall g\in\mathscr A(B,A).f\circ i'=f\land i'\circ g=g\end{dcases}
\implies\begin{dcases}\forall B\in{\rm ob}(\mathscr A)\forall f\in\mathscr A(A,B).f\circ i=f\\\forall B\in{\rm ob}(\mathscr A)\forall g\in\mathscr A(B,A).i'\circ g=g\end{dcases}
\implies\begin{dcases}\forall f\in\mathscr A(A,A).f\circ i=f\\\forall g\in\mathscr A(A,A).i'\circ g=g\end{dcases}
\implies\begin{dcases}i'\circ i=i'\\i'\circ i=i\end{dcases}
\implies i'=i
\underline{\therefore\forall A\in{\rm ob}(\mathscr A)\exist !i\in\mathscr A(A,A)\forall B\in{\rm ob}(\mathscr A)\forall f\in\mathscr A(A,B)\forall g\in\mathscr A(B,A).f\circ i=f\land i\circ g=g\quad}_\blacksquare
当然だが単位元の存在の一意性と全く同じ証明法である
おもしろい