かじもとにっき

自分用メモ

圏論(1)

数学 圏論

定義 (quiver)

\mathcal Oと\mathcal Aを共にclassとする。

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom})\text{ is a quiver } \equivDef \mathrm{cod}\text{ and }\mathrm{dom}\text{ are functions into }\mathcal O\text{ over }\mathcal A\text{.}

また、x,y \in \mathcal Oに対し、

x \leftarrow y \eqDef \{ f \in \mathcal A : \mathrm{cod}.f = x \wedge \mathrm{dom}.f = y \}\text{.}

定義から明らかに、

\langle\cup x,y \in \mathcal O :: x \leftarrow y \rangle = \mathcal A

が成り立つ。

定義 (deductive system)

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a deductive system } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom})\text{ is a quiver } \\
\;\wedge \mathrm{id}\text{ is a function over }\mathcal O \\
\;\wedge \langle\forall x \in \mathcal O :: \mathrm{id}_x \in x \leftarrow x \rangle \\
\;\wedge \circ\text{ is a function over }\mathcal O \times \mathcal O \times \mathcal O \\
\;\wedge \langle\forall x,y,z \in \mathcal O :: \circ_{x,y,z}\text{ is a function into }x \leftarrow z\text{ over }(x \leftarrow y) \times (y \leftarrow z) \rangle\text{.}

x,y,zが文脈から明らかな時、f \circ_{x,y,z} gをf \circ gのように省略して書く。

f,g \in \mathcal Aの時、定義から

\langle\forall x,y,z \in \mathcal O : f \in x \leftarrow y \wedge g \in y \leftarrow z : f \circ g \in x \leftarrow z\rangle

だが、これは1-point ruleによって

\mathrm{dom}.f=\mathrm{cod}.g \Rightarrow \mathrm{cod}(f \circ g) = \mathrm{cod}.f \wedge \mathrm{dom}(f \circ g) = \mathrm{dom}.g

と同値。

定義 (category)

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a category } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a deductive system } \\
\;\wedge \langle\forall w,x \in \mathcal O, f \in w \leftarrow x :: \mathrm{id}_w \circ_{w,w,x} f = f = f \circ_{w,x,x} \mathrm{id}_x \rangle \\
\;\wedge \langle\forall w,x,y,z \in \mathcal O, f \in w \leftarrow x, g \in x \leftarrow y, h \in y \leftarrow z \\
\quad\quad :: (f \circ_{x,y,z} g) \circ_{x,z,w} h = f \circ_{x,y,w} (g \circ_{y,z,w} h) \rangle\text{.}

定義 (small category, locally small category)

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a small category } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a category } \wedge \mathcal O\text{ is a set } \wedge \mathcal A\text{ is a set.}

(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a locally small category } \equivDef \\
\,(\mathcal O, \mathcal A, \mathrm{cod}, \mathrm{dom}, \mathrm{id}, \circ)\text{ is a category } \wedge \langle\forall x,y \in \mathcal O :: x \leftarrow y\text{ is a set } \rangle\text{.}

参考文献

  • M. Arbib and E. Manes. Arrows, Structures and Functors — The Categorical Imperative. Academic Press, 1975.
  • S. Awodey. Category Theory. 2d ed. Oxford University Press, 2010.
  • M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, 1990.
  • R.C. Backhouse. Mathematics of Program Construction. Unpublished.
  • R. Bird and O. de Moor. Algebra of Programming. Series in Computer Science. Prentice-Hall, 1997.
  • D. Gries. Foundations for Calculational Logic. In M. Broy, B. Schieder, eds., Mathematical Methods in Program Development. Springer, 1997.
  • E.J. Lemmon. Introduction to Axiomatic Set Theory. Routledge & Kegan Paul, 1968.
  • D. Gries and F.B. Schneider. A Logical Approach to Discrete Math. Springer-Verlag, 1993.
  • S. Mac Lane. Categories for the Working Mathematician. 2d ed. Springer-Verlag, 1998.
  • G. Tourlakis. Lectures in Logic and Set Theory Vol. 1: Mathematical Logic. Cambridge University Press, 2003.
  • G. Tourlakis. Lectures in Logic and Set Theory Vol. 2: Set Theory. Cambridge University Press, 2003.
  • G. Tourlakis. Mathematical Logic. John Wiley & Sons, 2008.