代数的構造による圏論(9) - エレファント・ビジュアライザー調査記録

トポス(1)

この段階で数学的帰納法を使うことによって図式を使わずに説明することができるようになったと思うのですが、簡単にはいかないのでトポスについてもう少し調べてみたいと思います。

[4]、[5]、[6]、[7]の本を持っていたので少し読んでみようと思います。[4]、[5]は型理論の本でトポスに関する記述もあるようです。[7]はトポスの本のようです。[6]は圏論全般の本のようですがトポスに関する記述があります。ただ英語のトポスの本を読むのはたいへんなので、[2]、[3]の本を持っていたのでまずこれから読んで見たいと思います。

まずトポスの定義から見ていきます。

[1] 圏論の道案内～矢印でえがく数学の世界～

[1]のトポスの定義は以下のようになっています。

定義 7.2 (トポス) 圏 $\mathcal{C}$ が CCC であり、部分対象分類子を持つとき、初等トポス(elementary topos)あるいは単にトポスと呼びます。ここで部分対象分類子(subobject classifier)とは $\mathcal{C}$ の射 $1 \xrightarrow{t} \Omega$ で、任意の単射 $A \xrightarrow{m} B$ に対して射 $B \xrightarrow{\chi_m} \Omega$ で $\require{AMScd}$ \begin{CD}
A @> !_A >> 1 \\
@V m VV @VV t V \\
B @>> \chi_m > \Omega
\end{CD} が引き戻しの図式となるようなものが一意に存在するものをいいます。このとき $\chi_m$ を $m$ の特性射(characteristic morphism)と呼びます。 $t$ は真(True)とも呼ばれ、また True とも書かれます。そして $\Omega$ は真理値対象(truth value object)と呼ばれます。

[2] 圏論による論理学―高階論理とトポス

部分対象分類子の定義、以下の定義 1 (トポス)は[1]と同じです。

定義 1 (トポス) 圏が以下の条件 (1)～(4) を満たすときトポスと呼びます。

(1) 終対象が存在する。
(2) 任意の対象 $A, B$ に対して積 $A \times B$ が存在する。
(3) 任意の対象 $A, B$ に対して冪 $B^A$ が存在する。
(4) 部分対象分類子が存在する。

<1> 終対象、積、部分対象分類子が存在するなら、イコライザーが存在する。

[証明]【 $A \overset{f}{\underset{g}{\rightrightarrows}} B$ とします。[1]で $\binom{f}{g}$ と書かれていた射をここでは $\langle f, g \rangle$ と書いています。 $\Delta_B = \langle 1_B, 1_B \rangle$ とし $B \times B \xrightarrow{\delta_B} \Omega$ を図式(1) \begin{CD}
B @> !_B >> 1 \\
@V \Delta_B VV @VV t V \\
B \times B @>> \delta_B > \Omega
\end{CD} が引き戻しの図式となる射とします。 $A \xrightarrow{\langle f, g \rangle} B \times B \xrightarrow{\delta_B} \Omega$ に対して図式(2) \begin{CD}
C @> !_C >> 1 \\
@V e VV @VV t V \\
A @>> \delta_B \circ \langle f, g \rangle > \Omega
\end{CD} が引き戻しの図式となる射 $C \xrightarrow{e} A$ が存在します。*1

$X \xrightarrow{p} C$ とすると、図式(3) \begin{CD}
X @> !_X >> 1 \\
@V e \circ p VV @VV t V \\
A @>> \delta_B \circ \langle f, g \rangle > \Omega
\end{CD} は可換となります。図式(2)が引き戻しの図式であることから $e \circ p = e \circ u$ となる $X \xrightarrow{u} C$ が一意的に存在します。一意性より $e \circ p = e \circ u'$ ならば $u = u'$ となります。よって $e \circ p = e \circ q$ ならば $p = q$ となるので $e$ は単射となります。*2

図式(4) \begin{CD}
C @> !_C >> 1 \\
@V \langle f, g \rangle \circ e VV @VV t V \\
B \times B @>> \delta_B > \Omega
\end{CD} が可換で図式(1)が引き戻しの図式であることから、 $\langle f, g \rangle \circ e = \Delta_B \circ v$ を満たす $C \xrightarrow{v} B$ が一意的に存在します。よって $f \circ e = \pi_1 \circ \langle f, g \rangle \circ e = \pi_1 \circ \Delta_B \circ v = 1_B \circ v = v$ 、 $g \circ e = \pi_2 \circ \langle f, g \rangle \circ e = \pi_2 \circ \Delta_B \circ v = 1_B \circ v = v$ となり $f \circ e = g \circ e$ となります。

$D \xrightarrow{h} A$ が $f \circ h = g \circ h$ を満たすとします。 $\langle f, g \rangle \circ h = \langle f \circ h, g \circ h \rangle = \langle f \circ h, f \circ h \rangle = \Delta_B \circ f \circ h$ となって、図式(5) \begin{CD}
D @> f \circ h >> B @> !_B >> 1 \\
@V h VV @V \Delta_B VV @VV t V \\
A @>> \langle f, g \rangle > B \times B @>> \delta_B > \Omega
\end{CD} は可換となります。図式(1)が引き戻しの図式であることから $D \xrightarrow{w} C$ が一意的に存在して $e \circ w = h$ となります。

よって $C \xrightarrow{e} A$ は $A \overset{f}{\underset{g}{\rightrightarrows}} B$ のイコライザーとなっています。】

<2> 積、イコライザーが存在するなら、引き戻しが存在する。
[証明]【 $A \xrightarrow{f} C \xleftarrow{g} B$ とすると、イコライザーが存在することから \begin{CD}
X @> e >> A \times B \\
@V e VV @VV g \circ \pi_2 V \\
A \times B @>> f \circ \pi_1 > C
\end{CD} が可換となるイコライザー $X \xrightarrow{e} A$ が存在します。\begin{CD}
Y @> q >> B \\
@V p VV @VV g V \\
A @>> f > C
\end{CD} が可換とすると、\begin{CD}
Y @> \langle p, q \rangle >> A \times B \\
@V \langle p, q \rangle VV @VV g \circ \pi_2 V \\
A \times B @>> f \circ \pi_1 > C
\end{CD} は可換となり、 $X \xrightarrow{e} A$ はイコライザーなので $Y \xrightarrow{u} X$ で $e \circ u = \langle p, q \rangle$ であるものが存在します。 $\pi_1 \circ e \circ u = \pi_1 \circ \langle p, q \rangle = p$ 、 $\pi_2 \circ e \circ u = \pi_2 \circ \langle p, q \rangle = q$ となるので \begin{CD}
X @> \pi_2 \circ e >> B \\
@V \pi_1 \circ e VV @VV g V \\
A @>> f > C
\end{CD} は引き戻しの図式となります。】

<3> 定義 1 の (1)～(4) が成立するなら、始対象、直和、押し出しが存在する。この証明は省略されています。

定義 2 (トポス) 圏が以下の条件 (1)～(4) を満たすときトポスと呼びます。

(1) 終対象が存在する。
(2) 任意の射 $A \to C \gets B$ に対して引き戻しが存在する。
(3) 任意の対象 $A, B$ に対して冪 $B^A$ が存在する。
(4) 部分対象分類子が存在する。

<4> 終対象と引き戻しが存在するなら、積が存在する。
[証明]【図式(1) \begin{CD}
X @> g >> B \\
@V f VV @VVV \\
A @>>> 1
\end{CD} を引き戻しの図式とします。 $A \xleftarrow{p} Y \xrightarrow{q} B$ とすると、
\begin{CD}
Y @> q >> B \\
@V p VV @VVV \\
A @>>> 1
\end{CD} は可換となります。図式(1)が引き戻しの図式であることから、 $Y \xrightarrow{u} X$ で $f \circ u = p$ 、 $g \circ u = q$ であるものが存在します。よって $A \xleftarrow{f} X \xrightarrow{g} B$ は積の図式となります。】　

[3] 層・圏・トポス―現代的集合像を求めて

定義 (部分対象分類子) 部分対象分類子(subobject classifier)とは $\mathcal{C}$ の射 $1 \xrightarrow{t} \Omega$ で、以下の二つの条件を満たすものをいいます。

(1) 任意の $B \xrightarrow{f} \Omega$ に対して $A \xrightarrow{g} B$ で \begin{CD}
A @> !_A >> 1 \\
@V g VV @VV t V \\
B @>> f > \Omega
\end{CD} が引き戻しの図式となるようなものが存在する。

(2) 任意の単射 $A \xrightarrow{m} B$ に対して射 $B \xrightarrow{\chi_m} \Omega$ で \begin{CD}
A @> !_A >> 1 \\
@V m VV @VV t V \\
B @>> \chi_m > \Omega
\end{CD} が引き戻しの図式となるようなものが一意に存在する。

部分対象分類子の定義は[1]の定義に条件(1)が追加されたものです。

定義 (トポス) 圏 $\mathcal{C}$ が CCC であり、部分対象分類子を持つとき、トポスと呼びます。

トポスの定義も同様に[1]の定義に条件(1)が追加されたものとなっています。

[4] Introduction to Higher-Order Categorical Logic

Part II Type theory and toposes
- 3 The internal language of a topos

定義 (部分対象分類子) 部分対象分類子(subobject classifier)とは $\mathcal{C}$ の射 $1 \xrightarrow{t} \Omega$ で、以下の二つの条件を満たすものをいいます。

(1) 任意の $B \xrightarrow{f} \Omega$ に対して $B \xrightarrow{f} \Omega$ と $B \xrightarrow{!_B} 1 \xrightarrow{t} \Omega$ のイコライザー $A \xrightarrow{g} B$ が存在する
(2) [3]の(2)と同じ

トポスの定義では自然数対象を持つという条件が増えています。自然数対象の定義は[1]と同じです。

定義 3.1 (トポス) 圏 $\mathcal{C}$ が CCC であり、部分対象分類子と自然数対象を持つとき、トポスと呼びます。

[5] Categories, Types, and Structures

2 Constructions
- 2.7 Subobject Classifiers and Topoi

定義 2.7.2 (トポス) [2]定義 2 と同じです。

[6] Computational Category Theory

7 Toposes
- 7.2 Toposes

定義 26 (トポス) 圏が以下の条件 (1)～(3) を満たすときトポスと呼びます。

(1) 有限図式に対する極限が存在する(有限完備)。有限図式に対する余極限が存在する(有限余完備)。
(2) 任意の対象 $A, B$ に対して冪 $B^A$ が存在する。
(3) 部分対象分類子が存在する。

[7] Sheaves in Geometry and Logic

IV. First Properties of Elementary Topoi
- 1. Definition of a Topos

定義 (トポス) 圏が以下の条件 (1)～(4) を満たすときトポスと呼びます。

(1) 終対象が存在する。
(2) 任意の射 $A \to C \gets B$ に対して引き戻しが存在する。
(3) 部分対象分類子が存在する。
(4) 任意の対象に対して、以下の条件を満たす対象、射が存在する:
- 任意の射 $B \times A \xrightarrow{f} \Omega$ に対して、以下の図式を可換にする射 $A \xrightarrow{g} PB$ が一意的に存在する:

\begin{CD}
B \times A @> f >> \Omega \\
@V 1_B \times g VV @| \\
B \times PB @>> \in_B > \Omega
\end{CD}

文献(本)

[1] 圏論の道案内～矢印でえがく数学の世界～

圏論の道案内～矢印でえがく数学の世界～数学への招待

作者:西郷甲矢人,能美十三
技術評論社

Amazon

[2] 圏論による論理学―高階論理とトポス

圏論による論理学―高階論理とトポス

作者:清水義夫
東京大学出版会

Amazon

[3] 層・圏・トポス―現代的集合像を求めて

層・圏・トポス―現代的集合像を求めて

作者:竹内外史
日本評論社

Amazon

[4] Introduction to Higher-Order Categorical Logic

Introduction to Higher-Order Categorical Logic (Cambridge Studies in Advanced Mathematics, Series Number 7)

作者:Lambek, J.,Scott, P. J.
Cambridge University Press

Amazon

[5] Categories, Types, and Structures

Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist (FOUNDATIONS OF COMPUTING SERIES)

作者:Asperti, Andrea,Longo, Giuseppe
Mit Pr

Amazon

[6] Computational Category Theory

Computational Category Theory (Prentice-hall International Series in Computer Science)

作者:Rydeheard, D. E.,Burstall
Prentice Hall

Amazon

[7] Sheaves in Geometry and Logic

Sheaves in Geometry and Logic: A First Introduction to Topos Theory (Universitext)

作者:MacLane, Saunders
Springer

Amazon

*1:この理由は不明。引き戻しが存在すると仮定すると成り立ちますが、後で引き戻しの存在の証明に使われているのでそれでは意味がない。集合の場合は $h = \delta_B \circ \langle f, g \rangle$ とおくと $C = h^{-1}(true) = \bigcup \{ X \mid X \subseteq A \ で図式が可換 \}$ となります。集合のように書くと $C \xrightarrow{e} A = \{ X \xrightarrow{m} A \mid \ 単射で図式が可換 \}$ という射が存在すると仮定すれば成り立ちます。\begin{CD} X @> !_X >> 1 \\ @V m VV @VV t V \\ A @>> \delta_B \circ \langle f, g \rangle > \Omega \end{CD}