ていへんかけるたかさわるに

数学: 射の合同関係,
数学: 射の合同 (続き)
数学: 同値関係の生成
の続き.

昨日どの箇所がわかっていなくて証明が進まないのかわかった.

現在進めている議論は次のようなものである.

圏 $\mathscr{\mathscr{C}}$ の射の全体 $\mathrm{Ar}(\mathscr{C})$ を $A$ とおく. $R$ を $A$ 上の任意の関係とする.
\begin{equation*}
\newcommand{\Ar}[1]{\mathrm{Ar}{#1}}
\newcommand{\ar}{\mathrm{ar}}
\newcommand{\arop}{\Opp{\mathrm{ar}}}
\newcommand{\Hom}{\mathrm{Hom}}
\newcommand{\Id}[1]{\mathrm{id}_{#1}}
\newcommand{\Mr}[1]{\mathrm{#1}}
\newcommand{\Ms}[1]{\mathscr{#1}}
\newcommand{\Ob}[1]{\mathrm{Ob}(#1)}
\newcommand{\Opp}[1]{{#1}^{\mathrm{op}}}
\newcommand{\Pos}{\mathbf{Pos}}
\newcommand{\q}{\hspace{1em}}
\newcommand{\Quot}[2]{{#1}\,/\,{#2}}
\newcommand{\qq}{\hspace{0.5em}}
\newcommand{Rest}[2]{{#1}|{#2}}
\newcommand{\Src}[1]{\mathrm{source}(#1)}
\newcommand{\Tgt}[1]{\mathrm{target}(#1)}
R_0 = \bigcup_{(f_1, f_2) \in R} \left\{\, (\Src{f_1}, \Src{f_2}) , (\Tgt{f_1}, \Tgt{f_2}) \,\right\}
\end{equation*} とおく.
これより $\mathscr{C}$ の対象 $O = \Ob{\Mr{C}}$ 上の $R_0$ を含む一意的な同値関係 $E_0$ が生成される.

$A$ に属する射からなる形式列の集合 $A^e$ を次のように定義する.
まず
\begin{equation*}
A^e_n = \left\{\, f_1 \cdots f_n \mid f_1,..., f_n \in A.\,\, \Src{f_i}\, E_0 \,\Tgt{f_{i+1}}\, (i = 1,..., n - 1 \,\right\}
\end{equation*} とおき, $A^e_n \, (n = 0, 1,...)$ を用いて $A^e$ を $A^e_n \, (n = 0, 1,...)$ の非交和として
\begin{equation*}
A^e = \coprod_{n=0}^{\infty} A^e_n
\end{equation*} と定義する.

$A$ において合成可能な射の対の集合 $P$ を
\begin{equation*}
P = \left\{\, (f, g) \mid f, g \in A.\,\Src{f} = \Tgt{g} \,\right\}
\end{equation*} とおき, $A^e$ 上の関係 $R_1$ を
\begin{equation*}
R_1 = \left\{\, (fg, f \circ g) \mid (f, g) \in P \,\right\}
\end{equation*} で定め, $R_1$ が生成する $A^e$ 上の同値関係を $E_1$ とする.

これにより $A^e$ の $E_1$ による商空間
\begin{equation*}
\hat{A} = \Quot{A^e}{E_1}
\end{equation*} と商写像
\begin{equation*}
q_1 : A^e \to \hat{A}
\end{equation*} が構成される.

わかっていなかったのは $\hat{A}$ がどのような構造を持つ集合か, $q_1$ が写像としてどのような性質を持つかという点だった.
$\hat{A}$ の構造を明らかにして, それに対する商写像 $q_1 : A^e \to \hat{A}$ の性質を明らかにしておくことで議論が一つ次の段階に進むのである.

論理の進め方を始めから 1 つずつ正しいかどうかチェックし, 必要ならば証明を与えるようにしていったらわかった.

まるで print デバッグのようで楽しかった. ちょっとでも進むことができると嬉しい.