並進式【translational notation】を検討・提案する。
特徴
- 圏論の各記法と関連付けがし易い。実際それらにインスパイアされた。
- 二方向規則【two-way rule、竹内による式の表示法】
- ストリング図【string diagram】
- 可換図式【commutative diagram】
- 箙表現
- ハッセ図
- 数式
- 結合の文章順記法【operation sequence as text sequence】
- テキスト形式(メモ帳アプリなど)で記載し、そのまま、または $\TeX$ ソースでも可読性がある。
今回は以下のルールにしています。好みで変更することも可能ですが、全体の整合性を保持するのに考慮が必要です。
\newcommand\sets{\mathrm{Set}}
\newcommand\op{^{\mathrm{op}}}
\newcommand\iv{^{-1}}
\newcommand\⇨{\text{⇨}} % 関手
\newcommand\➡{\text{➡}} % 自然変換
\newcommand\cone{\mathrm{Cone}}
\newcommand\cocone{\mathrm{Cocone}}
\newcommand\colim{\mathrm{colim}}
\newcommand\lett{\,\text{let}\,}
\newcommand\and{\,\text{and}\,}
\newcommand\st{\,\text{s.t.}\,} % such that
\newcommand\ie{\,\text{i.e.}\,}
\newcommand\eq[1]{\begin{array}{}#1\end{array}} % 式
\newcommand\a[1]{&[#1]&} % 射
\newcommand\so{⋯} % 省略対象
\newcommand\sa{&⋯&} % 省略射
\newcommand\spn{&\|&} % 並進を跨った射
\newcommand\h{&[\ ]&} % ホムセット
\newcommand\p[1]{\langle #1 \rangle} % 直積
\newcommand\ap[1]{&[\langle #1 \rangle]&} % 直積の射
\renewcommand\i[1]{&[1_{#1}]&} % 恒等射(規定の文字の定義を上書き)
\newcommand\t[1]{[\![#1]\!]} % 並進式(規定の文字の定義を上書き)
オブジェクト | 並進式の方向 | 式の方向 | 式の結合記号 |
---|---|---|---|
直積 | 上→下 | 左→右 | $\p{a,b}$ |
射 | 左→右 | 左→右 | $f⨾g$ |
垂直合成 | 左→右 | 左←右 | $G∘F$ |
水平合成 | 上←下 | 左←右 | $G∙F$ |
自然変換 | 左→右 | 左→右 | $n⨾m$ |
並進式の検証
対象と射と圏
※射と矢を大かっこでくくるのは、ストリング図の影響です。
\eq{
\text{対象}&\text{射}→&\text{対象}&\text{圏}\\
\text{頂点}&\text{矢}→&\text{頂点}&\text{箙}&\text{:説明用}\\ \hdashline
a \a{f} b &∈A \\
}
またはケットを流用する。※本投稿では使用しない。
\eq{
a &|f \rangle& b &∈A \\
}
これは以下を意味する。
\eq{
\text{射}&\text{対象}& &\text{対象}&\text{圏}\\ \hdashline
f:& a &→& b &∈A \\
}
射の合成、箙上の道
\eq{
& a \a{f &⨾& g} c \\
:=&a \a{f}b\a{g} c \\
}
射の結合律
\eq{
& a \a{(f &⨾& g) &⨾& h} d \\
=& a((\a{f} b \a{g})c \a{h}) d \\
=& a \a{f} b \a{g} c \a{h} d \\
=& a (\a{f} b (\a{g} c \a{h}))d \\
=& a \a{f &⨾& (g &⨾& h )}d \\
}
可換図式は、先頭対象同士と末尾対象同士が同一の、2個の並進式の等式で表現される。
\eq{
& a \a{f} b \a{g} d \\
=& a \a{h} c \a{k} d \\
}
または、先頭対象と末尾対象を、罫線文字を用いてつなげる。※本投稿では使用しない。
\eq{
& a \a{f} b \a{g} \text{┐} \\
↺& \text{└} \a{h} c \a{k} d \\
}
恒等射
\eq{
& b \i{b} b \\
=& b \a{b} b &\text{※1}\\
=& b \sa \so &\text{※2}\\
=&\so \sa b &\text{※2}\\
}
※1 恒等射を対象と同一視して表記を合わせることが可能。
※2 同じ対象と射を省略可能(本投稿ではアンダースコア)。ストリング図の縦線に対応。
恒等射のスライディング則
\eq{
& a \a{f &⨾& 1_b} b \\
=& a \a{f} b \i{b} b \\
=& a \a{f} b \sa \so \\
=&\so \sa a \a{f} b \\
=& a \i{a} a \a{f} b \\
=& a \a{1_a &⨾& f} b \\
}
モノ
\eq{
& &∀& &\text{is mono}\\
& a \a{x} b \a{f} c \\
=& a \a{y} b \a{f} c \\
⟹&a \a{x} b \\
=& a \a{y} b \\
}
エピ
\eq{
& &\text{is epi}& &∀ \\
& a \a{f} b \a{x} c \\
=& a \a{f} b \a{y} c \\
⟹& && b \a{x} c \\
=& && b \a{y} c \\
}
分裂エピモノ性
\eq{
& && b \a{m} a \a{e} b && \\
=& && b \i{b} && b && \\ \hdashline
\lett&&& && a \a{e} b \a{x} c \\
=& && && a \a{e} b \a{x} c \\ \hdashline
∴& && && && b \a{x} c \\
=& && b && \i{b} b \a{x} c && \\
=& && b \a{m} a \a{e} b \a{x} c \\
=& && b \a{m} a \a{e} b \a{y} c \\
=& && b && \i{b} b \a{y} c \\
=& && && && b \a{y} c \\ \hdashline
\lett&c \a{x} b \a{m} a \\
=&c \a{y} b \a{m} a \\ \hdashline
∴
& c \a{x} b && && \\
=&c \a{x} b \i{b} && b \\
=&c \a{x} b \a{m} a \a{e} b \\
=&c \a{y} b \a{m} a \a{e} b \\
=&c \a{y} b \i{b} && b \\
& c \a{y} b && && \\
}
逆射、同型
\eq{
& a \a{f} b \a{g} a \\
=& a && \i{a} a \\
\and& && b \a{g} a \a{f} b \\
=& && b \i{b} && b \\
}
終対象
\eq{
& 1∀ &2∃!& & \text{※}\\
& a \a{h} 1 \\
}
※述語論理の量化子の前に数値で順序を付け、並進式の順序と独立させる。
始対象
\eq{
& &2∃!& 1∀\\
& 0 \a{h} a \\
}
集合の要素は終対象(1点集合)からの射と同一視が可能。
\eq{
& \{*\} \a{a} A &∈\sets \\
⟺& &a∈& A &∈\sets \\
}
双対圏
\eq{
& c \a{g} b \a{f} a &∈A\op \\
=& c \a{g &⨾& f} a &∈A\op \\ \hdashline
⟺&a \a{f} b \a{g} c &∈A \\
=& a \a{f &⨾& g} c &∈A \\
}
圏の直積
\eq{
&\p{a,a'}\ap{f,f'}\p{b,b'}&∈A×B \\
=&\p{ a \a{f} b &∈A \\
&, a' \a{f'} b' }&∈B \\
}
圏の直積の合成
\eq{
& \p{a,a'} \a{\p{f,f'} &⨾& \p{g,g'}}\p{c,c'}&∈A×B \\
=&\p{a,a'} \ap{f,f'}\p{b,b'}\ap{g,g'} \p{c,c'}&∈A×B \\
=&\p{ a \a{f} b \a{g} c &∈A \\
&, a' \a{f'} b' \a{g'} c' }&∈B \\
=&\p{ a \a{f &⨾& g} c &∈A \\
&, a' \a{f' &⨾& g'} c' }&∈B \\
=&\p{a,a'} \a{\p{f⨾g &,& f'⨾g'}} \p{c,c'}&∈A×B \\
}
圏の直積のスライディング則
\eq{
& \p{a,a'}\a{\p{f,1_{a'}} &⨾&\p{1_b,f'}}\p{b,b'}&∈A×B \\
=&\p{a,a'}\ap{f,1_{a'}}\p{b,a'}\ap{1_b,f'}\p{b,b'}&∈A×B \\
=&\p{ a \a{f} b \i{b} b &∈A \\
&, a' \i{a'} a' \a{f'} b' }&∈B \\ \hdashline
=&\p{ a \a{f} && b &∈A \\
&, a' && \a{f'} b' }&∈B \\
=&\p{a,a'} && \ap{f,f'} \p{b,b'}&∈A×B \\
=&\p{ a && \a{f} b &∈A \\
&, a' \a{f'} && b' }&∈B \\ \hdashline
=&\p{ a \i{a} a \a{f} b &∈A \\
&, a' \a{f'} b' \i{b'} b' }&∈B \\
=&\p{a,a'}\ap{1_a,f'}\p{a,b'}\ap{f,1_{b'}}\p{b,b'}&∈A×B \\
=&\p{a,a'}\a{\p{1_a,f'} &⨾&\p{f,1_{b'}}}\p{b,b'}&∈A×B \\
}
関手 $F:A\➡B$
\eq{
&\t{ F \sa \so &∈B^A &\text{※}\\
&, a \a{f} b }&∈A \\
=&\t{F &F& F &∈B^A \\
&, a \a{f} b }&∈A \\
=& Fa \a{Ff} Fb &∈B \\ \hdashline
=&\t{F && &∈B^A \\
&, (a \a{f} b)}&∈A \\
=& F(a \a{f} b) &∈B \\
}
※同じ関手(対象)と恒等自然変換(射)を省略可能。ストリング図の縦線に対応。
関手の凖同型
\eq{
&\t{ F \sa && \so &∈B^A \\
&, a \a{f &⨾& g} c} &∈A \\
=& Fa \a{F(f &⨾& g)} Fc &∈B \\ \hdashline
=&\t{ F \sa \so \sa \so &∈B^A \\
&, x \a{f} b \a{g} c} &∈A \\
=& Fa \a{Ff} Fb \a{Fg} Fc &∈B \\ \hdashline
=&\t{ F \sa \sa \so &∈B^A \\
&, a \a{f &⨾& g} c} &∈A \\
=& Fa \a{Ff &⨾& Fg} Fc &∈B \\ \hdashline
=&\t{ F && && &∈B^A \\
&, x \a{f} b \a{g} c} &∈A \\
=& F(a \a{f} b \a{g} c) &∈B \\
}
関手は恒等射を恒等射に移す
\eq{
& Fa \a{F(1_a)} Fa &∈B \\
=&\t{F \sa \so &∈B^A\\
&, a \i{a} a }&∈A \\
=& Fa \i{Fa} Fa &∈B \\
=& Fa \a{Fa} Fa &∈B \\
=& Fa \sa \so &∈B \\
}
恒等関手
\eq{
&\p{1_A \sa \so &∈A^A \\
&, a \a{f} b }&∈A \\
=& a \a{f} b &∈A \\
}
双関手 $F:A×B\➡C$
\eq{&\t{ F \sa \so &∈C^{A×B} \\
& , \p{a,a'} \ap{f,f'} \p{b,b'} &∈A×B \\
=&,F\p{a,a'} \a{F\p{f,f'}}F \p{b,b'}}&∈C \\ \hdashline
=&\t{ F \sa \so &∈C^{A×B} \\
&,\p{ a \a{f} b &∈A \\
&, a' \a{f'} b' }}&∈B \\
}
双関手の一意性:各圏の対象を固定した、ある性質を満たす関手 $F,G$ で $T$ 一つに決まる。
\eq{
=&T\p{a,a'} \a{T\p{f,f'}} && T\p{b,b'} \\
&\t{ T \sa && \so \\
&, a \a{f} && b \\
&, a' \a{f'} && b'}\\
=&\t{T \sa \so \sa \so \\
&, a \a{f} b \sa \so \\
&, \so \sa a' \a{f'} b'}\\
=&T\p{a,a'} \a{G_{a'}f} T\p{b,a'} \a{F_bf'} T\p{b,b'} \\
}
双関手の準同型。ある性質とは、以下の等式の括弧内の等式性。
\eq{
& T\p{a,b} \a{T\p{f&⨾&g&,&f'&⨾&g'}} T\p{c,c'} \\
=&T\p{a,a'} \a{G_{a'}(f&⨾&g)} T\p{c,a'} \a{F_b(f'&⨾&g')} T\p{c,c'} \\
=&T\p{a,a'} \a{G_{a'}f} (T\p{b,a'} \a{G_{a'}g} T\p{c,a'} \a{F_cf'} T\p{c,b'}) \a{F_cg'} T\p{c,c'} \\
=&T\p{a,a'} \a{G_{a'}f} (T\p{b,a'} \a{F_bf'} T\p{b,b'} \a{G_{b'}g} T\p{c,b'}) \a{F_cg'} T\p{c,c'} \\
=&T\p{a,a'} \a{T\p{f&,&f'}} T\p{b,b'} \a{T\p{g&,&g'}} T\p{c,c'} \\
}
自然変換 $n:F\⇨G$ (対象への作用)
\eq{
& F \a{n} G &∈B^A \\
=&\{\t{F \a{n} G &∈B^A \\
&, a \sa \so}\}_a&∈A \\
=&\{ Fa \a{n_a} Ga \}_a&∈B \\
}
自然変換の自然性公理(スライディング則)
\eq{&Fa \a{Ff &⨾& n_b} Gb &∈B \\
=& Fa \a{Ff} Fb \a{n_b} Gb &∈B \\ \hdashline
=&\t{\so \sa F \a{n} G &∈B^A \\
&, a \a{f} b \sa \so }&∈A \\
=&\t{ F \a{n} G \sa \so &∈B^A \\
&, \so \sa a \a{f} b} &∈A \\ \hdashline
=& Fa \a{n_a} Ga \a{Gf} Gb &∈B \\
=& Fa \a{n_a &⨾& Gf} Gb &∈B \\
}
恒等自然変換の自然性公理
\eq{&Fa \a{Ff &⨾& 1_{Fb}} Fb &∈B \\
=& Fa \a{Ff} Fb \i{Fb} Fb &∈B \\ \hdashline
=&\t{\so \sa F \a{1_F} F &∈B^A \\
&, a \a{f} b \sa \so }&∈A \\
=&\t{ F \i{F} F \sa \so &∈B^A \\
&, \so \sa a \a{f} b }&∈A \\ \hdashline
=& Fa \i{Fa} Fa \a{Ff} Fb &∈B \\
=& Fa \a{1_{Fa}&⨾& Ff} Fb &∈B \\
}
自然変換(射への作用)
\eq{&Fa \a{n∙f} && Gb &∈B \\
:=&\t{F \a{n} && G &∈B^A \\
& , a \a{f} && b} &∈A \\ \hdashline
=&\t{\so \sa F \a{n} G &∈B^A \\
&, a \a{f} b \sa \so }&∈A \\
=&\t{ F \a{n} G \sa \so &∈B^A \\
&, \so \sa a \a{f} b }&∈A \\
}
対角関手
\eq{&Δ_ai \a{Δ_fi &⨾& Δ_bu} Δ_bj &∈C \\
=& a \a{f} b \sa \so &∈C \\
=& Δ_ai \a{Δ_fi} Δ_bi \a{Δ_bu} Δ_bj &∈C \\
=&\t{Δ_a \a{Δ_f} Δ_b \sa \so &∈C^I \\
&, \so \sa i \a{u} j }&∈I \\
=&\t{Δ \sa \so \sa \so &∈C^{C×I} \\
&, a \a{f} b \sa \so &∈C \\
&, \so \sa i \a{u} j }&∈I \\ \hdashline
=&\t{Δ \sa \so \sa \so &∈C^{C×I} \\
&, \so \sa a \a{f} b &∈C \\
&, i \a{u} j \sa \so }&∈I \\
=&\t{\so \sa Δ_a \a{Δ_f} Δ_b &∈C^I \\
&, i \a{u} j \sa \so }&∈I \\
=& Δ_ai \a{Δ_au} Δ_aj \a{Δ_fj} Δ_bj &∈C \\
=& \so \sa a \a{f} b &∈C \\
=& Δ_ai \a{Δ_au &⨾& Δ_fj} Δ_bj &∈C \\
}
対象を終対象(1点集合)からの関手と同一視可能。
\eq{
&\t{Δ_a \sa \so &∈C^1 \\
&, * \i{*} *}&∈1 \\
=& a \i{a} a &∈C \\
}
射を自然変換と同一視可能。(スライディング則が自明に成り立つ)
\eq{&Δ_a* \a{Δ_f1_* &⨾& Δ_b1_*} Δ_b* &∈C \\
=& a \a{f} b \sa \so &∈C \\
=& Δ_a* \a{Δ_f1_*} Δ_b* \a{Δ_b1_*} Δ_b* &∈C \\
=&\t{Δ_a \a{Δ_f} Δ_b \sa \so &∈C^1 \\
&, \so \sa * \i{*} * }&∈1 \\
=&\t{Δ \sa \so \sa \so &∈C^{C×1} \\
&, a \a{f} b \sa \so &∈C \\
&, \so \sa * \i{*} * }&∈1 \\ \hdashline
=&\t{Δ \sa \so \sa \so &∈C^{C×1} \\
&, \so \sa a \a{f} b &∈C \\
&, * \i{*} * \sa \so }&∈1 \\
=&\t{\so \sa Δ_a \a{Δ_f} Δ_b &∈C^1 \\
&, * \i{*} * \sa \so }&∈1 \\
=& Δ_a* \a{Δ_a1_*} Δ_a* \a{Δ_f1_*} Δ_b* &∈C \\
=& \so \sa a \a{f} b &∈C \\
=& Δ_a* \a{Δ_a1_* &⨾& Δ_f1_*} Δ_b* &∈C \\
}
自然変換の垂直合成【2圏間合成】
(圏論一般の用語に倣っている。文字列の進む方向を上下として考えれば良い)
\eq{& F \a{n &⨾& m} H &∈B^A \\
:=& F \a{n} G \a{m} H &∈B^A \\
=&\{\t{F \a{n} G \a{m} H &∈B^A \\
&, a \sa \so \sa \so }\}_a&∈A \\
=&\{ Fa \a{n_a} Ga \a{m_a} Ha \}_a&∈B \\
}
自然変換の垂直合成の自然性公理(スライディング則)
\eq{&Fa \a{Ff&⨾& (n &⨾& m)_b} Hb &∈B \\
& Fa \a{Ff&⨾& n_b &⨾& m_b} Hb &∈B \\
=& Fa \a{Ff} Fb \a{n_b} Gb \a{m_b} Hb &∈B \\ \hdashline
=&\t{\so \sa F \a{n} G \a{m} H &∈B^A \\
&, a \a{f} b \sa \so \sa \so }&∈A \\
=&\t{ F \a{n} G \sa G \a{m} H &∈B^A \\
&, \so \sa a \a{f} b \sa \so }&∈A \\
=&\t{ F \a{n} G \a{m} H \sa \so &∈B^A \\
&, \so \sa \so \sa a \a{f} b }&∈A \\ \hdashline
=& Fa \a{n_a} Ga \a{m_a} Ha \a{Hf} Hb &∈B \\
=& Fa \a{n_a&⨾& m_a &⨾& Hf} Gb &∈B \\
=& Fa \a{(n &⨾& m)_a &⨾& Hf} Gb &∈B \\
}
自然変換の水平合成【3圏間合成】とそのスライディング則
(圏論一般の用語に倣っている。文字列の進む方向を上下として考えれば良い)
\eq{&\{F'Fa\a{n'_a∙n_a} && G'Ga \}_a&∈C^A \\
=& F'F \a{n' ∙n} && G'G &∈C^A \\
=&\t{ F' \a{n'} && G' &∈C^B \\
&, F \a{n} && G }&∈B^A \\
=&\{\t{F' \a{n'} && G' &∈C^B \\
&, F \a{n} && G &∈B^A \\
&, a \sa && \so }\}_a&∈A \\ \hdashline
:=&\{F'Fa \a{n'_a∙F_a} G'Fa \a{G'a∙n_a} G'Ga \}_a&∈C^A \\
=& F'F \a{n' ∙F} G'F \a{G' ∙n} G'G &∈C^A \\
=&\t{ F' \a{n'} G' \sa \so &∈C^B \\
&, \so \sa F \a{n} G }&∈B^A \\
=&\{\t{F' \a{n'} G' \sa \so &∈C^B \\
&, \so \sa F \a{n} G &∈B^A \\
&, a \sa \so \sa \so }\}_a&∈A \\ \hdashline
=&\{ F'F \a{F'a∙n_a} F'Ga \a{n'_a∙Ga} G'Ga \}_a&∈C^A \\
=& F'F \a{F' ∙n} F'G \a{n' ∙G} G'G &∈C^A \\
=&\t{ \so \sa F' \a{n'} G' &∈C^B \\
&, F \a{n} G \sa \so }&∈B^A \\
=&\{\t{\so \sa F' \a{n'} G' &∈C^B \\
&, F \a{n} G \sa \so &∈B^A \\
&, a \sa \so \sa \so }\}_a&∈A \\
}
恒等自然変換 $1_F = F$ とおくことが可能。
\eq{& F'F \a{1_{F'}∙n} F'G &∈B^A \\
=:& F'F \a{F'∙n} F'G &∈B^A \\
=&\t{ F' \sa \so &∈B^B \\
&, F \a{n} G }&∈B^A \\
=&\{\t{F' \sa \so &∈B^B \\
&, F \a{n} G &∈B^A \\
&, a \sa \so }\}_a&∈A \\
}
垂直合成と水平合成のスライディング則
\eq{&F'F \a{(n' &⨾& m')&∙&(n&⨾& m)} H'H &∈C^A \\ \hdashline
=&\t{F' \a{n' &⨾& G' & & &⨾& m'} H' &∈C^B \\
&, F \a{n &⨾& G & & &⨾& m } H }&∈B^A \\
=&\t{F' (\a{n'} G' \a{m'})H' \sa \so \sa \so &∈C^B \\
&, \so \sa \so \sa F(\a{n} G \a{m}) H }&∈B^A \\
=&\t{F' \a{n'} G' \a{m'} H' \sa \so \sa \so &∈C^B \\
&, \so \sa \so \sa F \a{n} G \a{m} H }&∈B^A \\
=&\t{F' \a{n'} G' \sa G' \a{m'} H' \sa \so &∈C^B \\
&, \so \sa F \a{n} G \sa G \a{m} H }&∈B^A \\
=&\t{F' \a{n'} G' \sa \so \sa G' \a{m'} H' &∈C^B \\
&, F \a{n} G \sa \so \sa G \a{m} H }&∈B^A \\ \hdashline
=& F'F \a{(n' &∙& n) &⨾& (m' &∙& m)} H'H &∈C^A \\
}
自然同型
\eq{&& & Ga \a{Gf} Gb & & &∈B \\
=&\t{& & G \sa \so & & &∈B^A \\
&, & & a \a{f} b & & }&∈A \\ \hdashline
=&\t{G \a{n\iv} F \sa F \a{n} G &∈B^A \\
&, \so \sa a \a{f} b \sa \so }&∈A \\
=& Ga \a{n\iv_a} Fa \a{Ff} Fb \a{n_b} Gb &∈B \\
}
\eq{
& Ga \a{Gf} Gb &∈B \\ \hdashline
≅&Fa \a{Ff} Fb &∈B &\text{※}\\
}
※二方向規則が表現されている。
$n$ が自然変換⟺ $∀x, n_x$ は同型射
$n$ が自然変換、 $∀x, m_x = (n_x)\iv$ は同型射⟹$m$ は自然変換
\eq{
=&\t{G \a{m} F \sa && && \so &∈B \\
&, \so \sa x \a{f} && && y }&∈B \\ \hdashline
=& Gx \a{m_x} Fx \a{Ff} && && Fy &∈B \\
=&( Gx \a{m_x} Fx \a{Ff} Fy) \a{n_y &⨾& m_y} Fy &∈B \\
=&( Gx \a{m_x} Fx \a{Ff} Fy) \a{n_y} Gy \a{m_y} Fy &∈B \\ \hdashline
=&\t{G \a{m} F \sa F \a{n} G \a{m} F &∈B^A \\
&, \so \sa x \a{f} y \sa \so \sa \so }&∈A \\
=&\t{G \a{m} F \a{n} G \sa G \a{m} F &∈B^A \\
&, \so \sa \so \sa x \a{f} y \sa \so }&∈A \\ \hdashline
=& Gx \a{m_x} Fx \a{n_x}(Gx \a{Gf} Gy \a{m_y} Fy) &∈B \\
=& Gx \a{m_x &⨾& n_x}(Gx \a{Gf} Gy \a{m_y} Fy) &∈B \\
=& Gx && && \a{Gf} Gy \a{m_y} Fy &∈B \\ \hdashline
=&\t{\so && && \sa G \a{m} F &∈B^A \\
&, x && && \a{f} y \sa \so }&∈B \\
}
双関手の間の自然変換の自然性公理(スライディング則)
\eq{&F\p{a,b} \a{F\p{f,g} &⨾& n_\p{a',b'}} G\p{a',b'} &∈C \\
=& F\p{a,b} \a{F\p{f,g}} F\p{a',b'} \a{n_\p{a',b'}} G\p{a',b'} &∈C \\ \hdashline
=&\t{\so \sa F \a{n} G &∈C^{A×B} \\
&,\p{a \a{f} a' \sa \so &∈A \\
&, b \a{g} b' \sa \so }}&∈B \\
=&\t{F \a{n} G \sa \so &∈C^{A×B} \\
&,\p{\so \sa a \a{f} a' &∈A \\
&, \so \sa b \a{g} b' }}&∈B \\ \hdashline
=& F\p{a,b} \a{n_\p{a,b}} G\p{a,b} \a{G\p{f,g}} G\p{a',b'} &∈C \\
=& F\p{a,b} \a{n_\p{a,b} &⨾& G\p{f,g}} G\p{a',b'} &∈C \\
}
双関手間の自然変換の一意性:各圏の対象を固定した自然変換で一つに決まる。
\eq{
& F\p{a,b}\a{F\p{f,g}}&&F\p{a',b'}\a{n_{a',b'}}G\p{a',b'} &∈C \\
=&\t{ \so \sa && F \a{n} G &∈C^{A×B} \\
&, a \a{f} && a' \sa \so &∈A \\
&, b \a{g} && b' \sa \so }&∈B \\
=&\t{ \so \sa \so \sa F \a{n} G &∈C^{A×B} \\
&, \so \sa a \a{f} a' \sa \so &∈A \\
&, b \a{g} b' \sa \so \sa \so }&∈B \\
=&\t{ \so \sa F \a{n} G \sa \so &∈C^{A×B} \\
&, \so \sa \so \sa a \a{f} a' &∈A \\
&, b \a{g} b' \sa \so \sa \so }&∈B \\
=&\t{ F \a{n} G \sa \so \sa \so &∈C^{A×B} \\
&, \so \sa \so \sa a \a{f} a' &∈A \\
&, \so \sa b \a{g} b' \sa \so }&∈B \\
=&\t{ F \a{n} && G \sa \so &∈C^{A×B} \\
&, \so \sa && a \a{f} a' &∈A \\
&, \so \sa && b \a{g} b' }&∈B \\
=& F\p{a,b}\a{n_{a,b}}&&G\p{a,b}\a{G\p{f,g}}G\p{a',b'} &∈C \\
}
homセット
\eq{
& a\a{a⨾b} b &∈A \\
=& a \h b &∈A \\
=&\{a \a{h} b \}_h&∈A \\
=& a \a{A(a,b)} b &∈A & \text{※}\\
}
※圏論一般の表記法
homセットとhom関手と自然変換の自然性
\eq{
& (a' \a{f} a \h b) \a{g} b' &∈A \\
=&\{(a' \a{f} a \a{h} b) \a{g} b' \}_h&∈A \\
=&\{ a' \a{f} (a \a{h} b \a{g} b')\}_h&∈A \\
=& a' \a{f} (a \h b \a{g} b') &∈A \\
}
⟺
\eq{
& a⨾b \a{f⨾b} a'⨾b \a{a'⨾g} a'⨾b'&∈\sets \\
=& a⨾b \a{a⨾g} a⨾b' \a{f⨾b'} a'⨾b'&∈\sets \\
}
∴
\eq{
&\t{ a⨾- \a{f⨾-} a'⨾- \sa \so &∈\sets \\
&, \so \sa b \a{g} b' }&∈A \\ \hdashline
=& a⨾b \a{f⨾b} a'⨾b \a{a'⨾g} a'⨾b'&∈\sets \\
=& a⨾b \a{a⨾g} a⨾b' \a{f⨾b'} a'⨾b'&∈\sets \\ \hdashline
=&\t{\so \sa a⨾- \a{f⨾-} a'⨾- &∈\sets \\
&, b \a{g} b' \sa \so }&∈A \\
}
また
\eq{
&\t{ \so \sa -⨾b \a{-⨾g} -⨾b' &∈\sets \\
&, a \a{f⨾} a' \sa \so }&∈A\op \\ \hdashline
=& a⨾b \a{f⨾b} a'⨾b \a{a'⨾g} a'⨾b' &∈\sets \\
=& a⨾b \a{a⨾g} a⨾b' \a{f⨾b'} a'⨾b' &∈\sets \\ \hdashline
=&\t{-⨾b \a{-⨾g} -⨾b' \sa \so &∈\sets \\
&, \so \sa a \a{f⨾} a' }&∈A\op \\
}
hom系の式変形
\eq{
& \so \sa a \a{f} b &∈C \\
=& a \i{a} a \a{f} b &∈C \\
=&\t{ \spn a⨾- \sa \so &∈\sets \\
&, * \i{} a \a{f} b }&∈C \\
=&\t{ \spn a⨾- \sa \so &∈\sets \\
&, * \a{f} b \sa \so }&∈C \\
=&\t{ \spn b⨾- \a{f⨾-} a⨾- &∈\sets \\
&, * \i{} b \sa \so }&∈C \\
}
$n : (a⨾-) \⇨ K : C\op\➡\sets)$ 集合値関手への自然変換の式変形
\eq{
& && a⨾- \a{n} K &∈\sets \\
=&\{\t{ && a⨾- \a{n} K &∈\sets \\
&, d \sa \so \sa \so }\}_d&∈C \\
=&\{\t{ \spn a⨾- \a{n} K &∈\sets \\
&, * \i{} a \h d }\}_d&∈C \\
=& \t{ \spn a⨾- \a{n} K &∈\sets \\
&, * \i{} a \h - }&∈C \\
}
米田写像 $y_{K,a}$
\newcommand\pin{{n∈(a⨾-)⨾K}}
\eq{
& && && &y_{K,a}(n)∈& Ka& (\pin)& \\
⟺&\{ * && && \a{y_{K,a}(n)} Ka & \}_\pin&∈\sets \\
=&\{\t{ \spn a⨾- && \a{y_{K,a}(n)} K & &∈\sets^C \\
&, * \i{} a \sa \so \sa \so &}\}_\pin&∈C \\
\xlongequal{f:=1}
&\{\t{ \spn a⨾- && \a{y_{K,a}(n)} K & &∈\sets^C \\
&, * \i{} a \a{f} d \sa \so &}\}_{\pin,f∈a⨾d}&∈C \\
=&\{\t{ \spn a⨾- && \a{y_{K,a}(n)} K & &∈\sets^C \\
&, * \i{} a \h d \sa \so &}\}_{\pin,d}&∈C \\
=&\{\t{ \spn a⨾- \a{n} K \a{y_{K,a}} K & &∈\sets^C \\
&, * \i{} a \h d \sa \so &}\}_{\pin,d}&∈C \\
=&\{\t{ && a⨾- \a{n} K \a{y_{K,a}} K & &∈\sets^C \\
&, && d \sa \so \sa \so &}\}_{\pin,d}&∈C \\
=&\{ && a⨾- \a{n} K \a{y_{K,a}} Ka & \}_\pin&∈\sets \\
=& && a⨾- \h K \a{y_{K,a}} Ka & &∈\sets \\
=& &&((a⨾-) &⨾& K) \a{y_{K,a}} Ka & &∈\sets \\ \hdashline
:=&\t{ \spn a⨾- && \h K & &∈\sets^C \\
&, * \a{!} a && \sa \so &} &∈C \\
=&\{\t{ \spn a⨾- && \a{n} K & &∈\sets^C \\
&, * \a{!} a && \sa \so &}\}_\pin&∈C \\
=&\{\t{ \spn a⨾- && \a{n} K & &∈\sets^C \\
&, * \a{!} a && \i{a} a &}\}_\pin&∈C \\
=&\{ * && && \a{n_a∙1_a} Ka & \}_\pin&∈\sets \\
⟺& && && &n_a∙1_a∈& Ka& (\pin)& \\
}
逆向きの米田写像 $Y_{K,a}$
\renewcommand\pin{{x∈Ka}}
\eq{
& && &Y_{K,a}(x)∈& (a⨾-)⨾K& (\pin)& \\
⟺&\{ * && \a{Y_{K,a}(x)} (a⨾-)⨾K & \}_\pin&∈\sets \\
=&\{ * \a{x} Ka \a{Y_{K,a}} (a⨾-)⨾K & \}_\pin&∈\sets \\
=& && Ka \a{Y_{K,a}} (a⨾-)⨾K & &∈\sets \\ \hdashline
:=&\t{ \spn K \sa \so & &∈\sets^C \\
&, * \a{?} a \h - & }&∈C \\
=&\{\t{ \spn K \sa \so & &∈\sets^C \\
&, * \a{x} a \h - &}\}_\pin&∈C \\
=&\{\t{ \spn K \sa \so & &∈\sets^C \\
&, * \a{x} a \a{f} d &}\}_{\pin, f∈a⨾d}&∈C \\
=&\{\t{* \a{x} Ka \a{Kf} Kd &}\}_{\pin, f∈a⨾d}&∈C \\
=&\{\t{* && \a{Kf(x)} Kd &}\}_{\pin, f∈a⨾d}&∈C \\
⟺& && &Kf(x)∈& Kd & (\pin, f∈a⨾d)& \\
}
\eq{
& && a⨾- \a{n} K && &∈\sets \\
\xmapsto{y}&\t{\spn a⨾- \a{n} K && &∈\sets^C \\
&, * \a{!} a \sa \so && }&∈C \\
\xmapsto{Y}&\t{\spn a⨾- \a{n} K \sa \so &∈\sets^C \\
&, * \a{!} a \sa \so \h - }&∈C \\
=& && a⨾- \a{n} K && &∈\sets \\
}
\eq{
&\t{ \spn K && &∈\sets^C \\
&, * \a{x} a && }&∈C \\
\xmapsto{Y}&\t{\spn K \sa \so &∈\sets^C \\
&, * \a{x} a \h - }&∈C \\
\xmapsto{y}&\t{\spn K && &∈\sets^C \\
&, * \a{x} a && }&∈C \\
}
hom関手との合成
\eq{
& && a'⨾Fa \a{a'⨾Ff} a'⨾Fb &∈\sets \\
=&\t{&& a'⨾F- \sa \so &∈\sets \\
&, && a \a{f} b }&∈A \\
=&\t{&& a'⨾- \sa \so &∈\sets \\
&, && F \sa \so &∈B^A \\
&, && a \a{f} b }&∈A \\
=&\t{\spn F \sa \so &∈B^A \\
&,a' \h a \a{f} b }&∈A \\
}
∴
\eq{
&\t{ && a'⨾F- &∈\sets \\
&, && ? }&∈A \\
=&\t{&& a'⨾- &∈\sets \\
&, && F &∈B^A \\
&, && ? }&∈A \\
=&\t{\spn F &∈B^A \\
&,a' \h ? }&∈A \\
}
また
\eq{
& Fa⨾b' \a{Ff⨾b'} Fb⨾b' && &∈\sets \\
=&\t{F-⨾b' \sa \so && &∈\sets \\
&, a \a{f} b && }&∈A \\
=&\t{-⨾b' \sa \so && &∈\sets \\
&, F \sa \so && &∈B^A \\
&, a \a{f} b && }&∈A \\
=&\t{F \sa \so \spn &∈B^A \\
&, a \a{f} b \h b'}&∈A \\
}
∴
\eq{
&\t{F-⨾b' && &∈\sets \\
&, ? && }&∈A \\
=&\t{-⨾b' && &∈\sets \\
&, F && &∈B^A \\
&, ? && }&∈A \\
=&\t{ F \spn &∈B^A \\
&, ? \h b'}&∈A \\
}
コンマ圏 $(F⇉G)$
\eq{
&\p{a,h,b}\ap{f,& &g}\p{a',h',b'}&∈(F⇉G)\\ \hdashline
=&\t{F \a{h} G \sa \so &∈C^{\text{below}}\\
&, a \spn && &∈A\\
&, \spn b \a{g} b' }&∈B\\ \hdashline
=& Fa \a{h} Gb \a{Gg} Gb' &∈C\\
=& Fa \a{Ff} Fa' \a{h'} Gb' &∈C\\ \hdashline
=&\t{\so \sa F \a{h'} G &∈C^{\text{below}}\\
&, a \a{f} a' \spn &∈A\\
&, && \spn b' }&∈B\\
}
コンマ圏 $(F⇉b):=(F⇉!)$
\eq{
&\p{a,h} \a{f} && \p{a',h'}&∈(F⇉b)\\ \hdashline
=&\t{F \a{h} ! \sa \so &∈C^A\\
&, a \spn b \sa \so }&∈A\\ \hdashline
=& Fa \a{h} b \sa \so &∈C\\
=& Fa \a{Ff} Fa' \a{h'} b &∈C\\ \hdashline
=&\t{\so \sa F \a{h'} ! &∈C^A\\
&, a \a{f} a' \spn b }&∈A\\
}
スライス圏 $A/b:=(1_A⇉b)=(1_A⇉!)$
\eq{
&\p{a,h}\a{f}&&\p{a',h'}&∈A/b\\ \hdashline
=& a \a{h} b \sa \so &∈A\\
=& a \a{f} a' \a{h'} b &∈A\\
}
$F$ から $b$ への普遍射 $:=(F⇉b)$ の終対象
\eq{
& 1∀ &2∃!& && 1= \\
&\p{a,h}\a{f} &&\p{a',h'} &∈(F⇉b)\\ \hdashline
=&\t{F \a{h} ! \sa \so &∈C^A\\
&, a \spn b \sa \so }&∈A\\ \hdashline
=& Fa \a{h} b \sa \so &∈C\\
=& Fa \a{Ff} Fa' \a{h'} b &∈C\\ \hdashline
=&\t{\so \sa F \a{h'} ! &∈C^A\\
&, a \a{!f} a' \spn b }&∈A\\
}
コンマ圏 $(a⇉G):=(!⇉G)$
\eq{
&\p{h,b}&& \a{g}\p{h',b'}&∈(a⇉G)\\ \hdashline
=&\t{! \a{h} G \sa \so &∈C^B\\
&, a \spn b \a{g} b' }&∈B\\ \hdashline
=& a \a{h} Gb \a{Gg} Gb' &∈C\\
=& \so \sa a \a{h'} Gb' &∈C\\ \hdashline
=&\t{\so \sa ! \a{h'} G &∈C^B\\
&, \so \sa a \spn b' }&∈B\\
}
余スライス圏 $a/B:=(B⇉1_B)=(!⇉1_B)$
\eq{
&\p{h,b}&&\a{g}\p{h',b'}&∈a/B\\ \hdashline
=& a \a{h} b \a{g} b' &∈B\\
=& \so \sa a \a{h'} b' &∈B\\
}
$a$ から $G$ への普遍射 $:=(a⇉G)$ の始対象
\eq{
& 0= && &2∃!& 1∀ \\
&\p{h,b} && \a{g} \p{h',b'}&∈(a⇉G)\\ \hdashline
=&\t{! \a{h} G \sa \so &∈C^B\\
&, a \spn b \a{g} b' }&∈B\\ \hdashline
=& a \a{h} Gb \a{Gg} Gb' &∈C\\
=& \so \sa a \a{h'} Gb' &∈C\\ \hdashline
=&\t{\so \sa ! \a{h'} G &∈C^B\\
&, \so \sa a \spn b' }&∈B\\
}
随伴
前提: $F:A⇄B:G$ は関手
$w:F⊣G:A⇄B$
$⟺ w:B(F-,?)≅A(-,G?)$
$⟺ ∀a,b, w_{a,b}:B(Fa,b)≅A(a,Gb)$
随伴の自然性
\eq{
& Fa⨾b \a{Ff⨾g} Fa'⨾b' \a{w_{a',b'}} a'⨾Gb' &∈\sets \\
=&Fa⨾b \a{w_{a,b}} a⨾Gb \a{f⨾Gg} a'⨾Gb' &∈\sets \\
}
∴ $∀h$
\eq{
& Fa'\a{Ff} Fa \a{h} b \a{g} b' &∈B \\
=& &Ff⨾& h &⨾g& && &∈B_1 \\
≅& &Ff⨾& h &⨾g& ⨾ &w_{a',b'}& &∈A_1 \\
=& h &⨾& ( &Ff⨾g& ⨾ &w_{a',b'}& ) &∈A_1 \\
=& h &⨾& (Fa⨾b \a{Ff⨾g} Fa'⨾b' \a{w_{a',b'}} a'⨾Gb') &∈A_1 \\
=& h &⨾& (Fa⨾b \a{w_{a,b}} a⨾Gb \a{f⨾Gg} a'⨾Gb') &∈A_1 \\
=& h &⨾& ( &w_{a,b}& ⨾ &f⨾Gg& ) &∈A_1 \\
=& (h &⨾& &w_{a,b})& ⨾ &(f⨾Gg& ) &∈A_1 \\
=& &f⨾& (h &⨾w_{a,b})& ⨾ &Gg& &∈A_1 \\
=& a' \a{f} a \a{h⨾w} Gb \a{Gg} Gb' &∈A \\
}
∴
\eq{
& Fa' \a{Ff} Fa \a{h} b \a{g} b' &∈B \\
≅& a' \a{f} a \a{h⨾w} Gb \a{Gg} Gb' &∈A \\
}
※二方向規則が表現されている。
⟺
\eq{
&\t{\so \sa F \a{h} && &∈B^A \\
&, a' \a{f} a \spn && &∈A \\
&, && \spn b \a{g} b'}&∈B \\
≅&\t{ && \a{h⨾w} G \sa \so &∈A^B \\
&, a' \a{f} a \spn && &∈A \\
&, && \spn b \a{g} b'}&∈B \\
}
\newcommand\Dt{D^\sim}
※二方向規則をストリング図で表したものが表現されている。
極限はコンマ圏 $(Δ⇉\Dt) (Δ:C\➡C^I, D:I\➡C, \Dt:{*}\➡C^I = D)$ の終対象
\eq{
& 1∀ &2∃!& && 1= \\
&\p{y,g} \a{h} && \p{x,f}&∈(Δ⇉\Dt) \\ \hdashline
=&\t{Δ \a{g} \Dt \sa \so &∈(C^I)^{\text{below}} \\
&, y \spn && &∈C \\
&, \spn * \sa \so }&∈\{*\} \\ \hdashline
=& Δ_y \a{g} \Dt* \sa \so &∈C \\
=& Δ_y \a{Δ_h} Δ_x \a{f} \Dt* &∈C \\ \hdashline
=&\t{\so \sa Δ \a{f} \Dt &∈(C^I)^{\text{below}} \\
&, y \a{h} x \spn &∈C \\
&, && \spn * }&∈\{*\} \\
}
自然変換 $g:Δ_y\⇨D = \cone(y,D) \ie y$ を頂点とする $D$ の錐のスライディング則
\eq{
& y \a{g_i} D_i \a{D_u} D_j &∈C \\ \hdashline
=&\t{Δ_y \a{g} D \sa \so &∈C^I \\
&, \so \sa i \a{u} j }&∈I \\
=& Δ_yi \a{g_i} D_i \a{D_u} D_j &∈C \\
=& Δ_yi \a{Δ_yu} Δ_yj \a{g_j} D_j &∈C \\
=&\t{\so \sa Δ_y \a{g} D &∈C^I \\
&, i \a{u} j \sa \so }&∈I \\ \hdashline
=& \so \sa y \a{g_j} D_j &∈C \\
=& y \a{g_j} && D_j &∈C \\
}
上記2つを組み合わせて整理した、極限
\eq{
& && x \a{f_i} D_i \a{D_u} D_j \\
=& && x \a{f_j} && D_j \\ \hdashline
\and∀y,g&y && \a{g_i} D_i \a{D_u} D_j \\
=& y && \a{g_j} && D_j \\
∃!h\st& y && \a{g_i} D_i && \\
=& y \a{h} x \a{f_i} D_i && \\
\and& y && \a{g_j} && D_j \\
=& y \a{h} x \a{f_j} && D_j \\
}
余極限はコンマ圏 $(\Dt⇉Δ) (Δ:C\➡C^I, D:I\➡C, \Dt:{*}\➡C^I = D)$ の始対象
\eq{
& 0= && &2∃!& 1∀ \\
& \p{x,f} && \a{h} \p{y,g} &∈(\Dt⇉Δ) \\ \hdashline
=&\t{\so \sa \Dt \a{g} Δ &∈(C^I)^{\text{below}} \\
&, && \spn y &∈C \\
&, \so \sa * \spn }&∈\{*\} \\ \hdashline
=& \so \sa \Dt* \a{g} Δ_y &∈C \\
=& \Dt* \a{f} Δ_x \a{Δ_h} Δ_y &∈C \\ \hdashline
=&\t{\Dt \a{f} Δ \sa \so &∈(C^I)^{\text{below}} \\
&, \spn x \a{h} y &∈C \\
&, * \spn && }&∈\{*\} \\
}
自然変換 $g:D\⇨Δ_y = \cocone(D,y) \ie y$ を頂点とする $D$ の余錐のスライディング則
\eq{
& D_i \a{D_u} D_j \a{g_j} y &∈C \\ \hdashline
=&\t{\so \sa D \a{g} Δ_y &∈C^I \\
&, i \a{u} j && }&∈I \\
=& D_i \a{D_u} D_j \a{g_j} Δ_yj &∈C \\
=& D_i \a{g_i} Δ_yi \a{Δ_yu} Δ_yj &∈C \\
=&\t{ D \a{g} Δ_y \sa \so &∈C^I \\
&, \so \sa i \a{u} j }&∈I \\ \hdashline
=& D_i \a{g_i} y \sa \so &∈C \\
=& D_i && \a{g_i} y &∈C \\
}
上記2つを組み合わせて整理した、余極限
\eq{
& D_i \a{D_u} D_j \a{f_j} x && \\
=& D_i && \a{f_i} x && \\ \hdashline
\and∀y,g&D_i \a{D_u} D_j \a{g_j} && y \\
=& D_i && \a{g_i} && y \\
∃!h\st& D_i && \a{g_i} && y \\
=& D_i && \a{f_i} x \a{h} y \\
\and& && D_j \a{g_j} && y \\
=& && D_j \a{f_j} x \a{h} y \\
}
技術情報
$\TeX$ で小さなコマンドを定義すると、ソースの可読性が高まったり、記号を切り替えたり、と便利です。
名前 | 英語 | 表示例 | $\TeX$定義文 | その他 |
---|---|---|---|---|
式 | equation | 省略 | \newcommand\eq[1]{\begin{array}{}#1\end{array}} |
|
射 | arrow | $[f]$ or $\ket{f}$ | \newcommand\a[1]{&[#1]&} |
& を含める |
同様対象 | same object | ⋯ | \newcommand\so{⋯} |
|
同様射 | same arrow | ⋯ | \newcommand\sa{&⋯&} |
& を含める |
並進を跨る射 | span | $\|$ | \newcommand\spn{&\|\|&} |
& を含める |
ホムセット | hom | $[\ ]$ | \newcommand\h{&[\ ]&} |
& を含める |
直積 | product | $\p{a,b}$ | \newcommand\p[1]{\langle #1 \rangle} |
|
直積の射 | a & p | $[\p{a,b}]$ | \newcommand\ap[1]{&[\langle #1 \rangle]&} |
& を含める |
恒等射 | identity | $1_a$ | \renewcommand\i[1]{&[1_{#1}]&} |
& を含める、上書き |
並進式 | translational | $\t{F,a [f] b} $ | \renewcommand\t[1]{[\![#1]\!]} |
上書き。mathjaxではllbracket等が規定で利用不可 |
※本投稿でも Markdown 内で $\TeX$ を使用する際に活用しています。Markdownのソースを参照してみてください。
更新履歴
- 2025/02/25a 新規公開
- 2025/02/26a 文章順結合の演算子を変更(;→⨾)。その演算子の記号誤記を修正。
- 2025/02/28a モノ、エピ、分裂エピモノ性、逆射、終対象、始対象、双関手の一意性、双関手間の自然変換の一意性、極限、余極限を追加。
- 2025/02/28a 双関手の間の自然変換の自然性公理(スライディング則)を修正。
- 2025/03/01a 双関手の準同型を修正。
- 2025/03/04a homセットの並進式を追加、随伴の並進式を一部調整。
- 2025/03/04a 記号の見直し(アンダースコアとハイフンが似ているため、アンダースコアを点線に変更)。
参考文献
- 中平健治著, ストリング図で学ぶ圏論の基礎, 森北出版, 2025.
- 朝芝秀人著, グラフ表現で可視化する圏論, 共立出版, 2024.
- S.マックレーン著, 三好博之, 高木理訳, 圏論の基礎, 丸善出版, 2012.
- S.アウディ著, 前原和寿訳 圏論 原著第2版, 共立出版, 2015.
- T.レンスター著, 斎藤恭司監修, 土岡俊介訳, ベーシック圏論, 丸善出版, 2017.
- 雪田修一著, 圏論入門 Haskellで計算する具体例から, 日本評論社, 2020.
- https://en.wikipedia.org/wiki/Composition_of_relations (結合の文章順記法について)