プレーンテキストと文章順合成記号で理解する圏論

前提

前提スキル
- 述語論理と集合論の記号の扱いに慣れていることが望ましいです。
- 記号一覧：=∴∵⇒⇔¬∧∨∀∃∈∋⊂⊃∩∪
- ∵命題や説明を記号で記載することで、文字数を少なく抑え、目への入りやすさを高めるためです。
前提作業
- 本資料では等幅フォントを前提とした整形データを記載しています。しかし現時点のQiitaでは等幅フォントを指定して投稿する手段がありません。著者の意図通りの整形したテキストデータを閲覧するため、後述「注意」の作業をお願いします。
前提認識
- 圏論, category theory【, カテゴリー論】は多くの方が理解した方が良い、という認識が前提です。
更新頻度
- 筆者が身につけた成果を不定期に反映していく予定です。
文章表現
- 以下をまとめて「取り扱い」と表現します。
  - 編集・転用・推敲・見直し・バージョンアップ・共有・公開。
- 以降の節から「である」調で表現します。

圏論を容易に理解するための方針

プレーンテキストをテキストエディタで操作する。
文章順に積み重ねる合成記号を主に使用する。

標準フォーマットについて

世間では、数式・図式の標準フォーマットを利用して表現しがち。

標準フォーマット：LaTeX, MathJax, MathML

背景

他のフォーマットは事実上無い。

課題

取り扱いながら理解を進めるのに不向き。
図式だけでは情報が不足しがちで、図式を辿るために前後の数式+文章で意味を補う必要がある。
- 図式内の各オブジェクトの位置づけ(前提、固定、束縛(∀∃)、導出・構成される)、見た目で分かりづらい。
- 図式を辿る事による証明方法をdiagram chasingというが、実際は「論理」を辿る必要があり、標準の図式のみではその情報が不足していると感じる(特に著者にとって)。
図式と数式+文章で情報が分散しがちになるため、頭の中の関連付けでワーキングメモリがあふれてしまい、理解の妨げになる(特に著者にとって)。
ブログや情報共有サイトなど他環境を利用した共有や転用に、互換性の配慮が必要。最悪は画像化が必要。
- nforum.ncatlab.org(フォーラムのほうです)の複数の投稿では、行列(array)の各セルに対象(A,B,C,...)や矢印(searrowなど)を記載して図式を表現している。

本資料の方針

プレーンテキストを利用する。

等幅フォントを利用する。
- ∵文字によって幅のバリエーションを少なくすることで、整形を易しくする。
マルチバイト文字を利用する。
- 矢印文字を利用する。
- 矢印を接続するのに罫線文字を利用する。
理解を促進する表示方略。
- 意味が強結合な図式・数式・文章を、なるだけ近くに配置する。
- 行を１つの階層(レイヤー)とみなし、情報を複数行にうまく重ねる。
- 縦横の繋がりを明確化するため、インデントで整形する。
- 式を並べるとき、同じ文字がなるだけ縦に並ぶようにする。

メリット

取り扱いながら理解を進めるのが容易。
WYSIWYG(What You See Is What You Get見たままを得られる)。見たまま以上は得られない、見たままでしかない、とも言える。
フォーマットがほぼ不要で、図式と式の間に文法上の区別が不要。
共有に必要な配慮は、主に等幅・空白・インデントに限られる。
整形・インデントに縦横の制限が大きいため、逆に世間の圏論の図式にない、縦横の関連の発見やその共有に繋がりやすい。
情報が分散しがちな弱点を補い、理解を促すことができる。

デメリットとその回避策

文字のバリエーション(フォント・太字・斜体)が表現できない。表現するには可変長のLaTeXコードが必要。
- 半角全角、ギリシャ文字などの違いでバリエーションを出す。
上付き下付き文字が表現できない。表現するには可変長のLaTeX文が必要。
- LaTeX文の「^_」マークでそのまま表現してなんとかカバーする。
- H_A→Ｃ(-,A)などLaTeXコードが出ない表現を規定にする。
- 下付き文字が数字や添字の場合、プログラム変数風に「_」を省略して見やすくする。
数学記号の表現力が乏しい。
- マルチバイト文字を使用して、圏論の範囲をなんとかカバーする。
図式の表現力が乏しい、特に斜めの矢印について。
- マルチバイト文字の矢印と罫線文字を使用してなんとかカバーする。
編集などの作業で整形・インデントが崩れがち。
- 図式を見直し再検討する契機としてポジティブにとらえる。
プレーンテキストのみだと共有に不向き。
- マークダウンで外枠を整える。プレーンテキストの範疇で済む。
- マークダウンでコードブロックの言語をうまく選択することで、等幅フォントが適用されるよう調整する。
qiitaのマークダウン投稿では、等幅フォントを指定することができない。
- 注意に記載の手段でなんとかカバーする。

筆記用具で書かせる方法について

世間では、筆記用具(デジタルを含む)で書かせがち。

背景

標準フォーマットは、取り扱いながら理解を進めるのに不向き。
他のフォーマットは事実上無い。

課題

取り扱いが難しい。
絵心(図心)が乏しかったり、筆記がきたないと、見直し時に自分でも解読不能になる(特に著者)。
ネットで共有するのに画像化が必要。
- 画像化・動画にすると検索性が低く、見返しが面倒。
- OCRは図式を読み取るのに不向き。
情報表示領域とファイル保存領域の二種類の余白が足りなくなりがち。
- アナログなら両者は重複。
- デジタル筆記用具でも余白を作るのにひと手間かかりそう。

本資料の方針

プレーンテキストを利用する。(再掲)

メリット

著者が今回開発(?)した書き方を真似すれば、絵心(図心)や筆記のきたなさに左右されなくなる。
検索性が高く、見返しが楽。
余白が足りなくなることはほぼない。※記憶装置の容量によるがプレーンテキストなので保存容量は小さめ。

文章逆順合成記号について

数学標準では「g∘f(x)」と書いて「要素xに最初に関数fを作用させ、次にgを作用させる」文章逆順合成を意味する。

背景

歴史的(恣意的)なもの。
- 文章順合成記号が標準になっているパラレルワールドが可能、という意味で恣意的。

課題

左から右へ読む文章の中で、右から左に合成が表記されるのは、順番が逆になっており、圏論を理解するのに主要な障壁になる(特に著者)。
分かりづらくなる心理学的背景の推定。
- 図式・数式間で向きを随時脳内変換する必要がある。
- 一部だけ逆さメガネしているような難易度。
- 脳内変換に慣れないと、ワーキングメモリのマジックナンバーをすぐに超過してしまう。
- 上記が得意な方が高等数学に進みやすいのか。

世間の対応策

図式の矢印を、右から左の方向にする((西郷-道案内))。
文章順合成記号(Left-to-right composition)を設け、両方使用可能にする。
- f>>g：F#言語, Groovy言語 https://rosettacode.org/wiki/Function_composition
- f>>>g：Haskel言語のControl.Category https://hackage.haskell.org/package/base-4.19.1.0/docs/Control-Category.html
- andThen：Haskel言語, Scala言語, Java8以降のFunction。
- f⨟g：Z記法 (U+2A1F)(太いセミコロン)。((Fong-Spivak))p12。
- ;：(Asciiのセミコロン)((Awodey))p11
- ※「後置」の用語は逆ポーランド記法の意味に取られるので避けた。
  - 後置≒逆ポーランド記法の表記例:f g ∘

本資料の方針

文章順合成記号を主に使用する。記号は「;」を採用する。
- ∵プレーンテキストでの書きやすさのため。
- ∵半角文字なので表示場所を取らないため。
合成の省略は数学標準の文章逆順合成記号「∘」にだけ認める。そのため「;」の記号は省略不可である。
- ∵曖昧さを防ぐため。
- ∵現行(世間・歴史)との接続も大切なため。
合成を省略したほうが理解しやすそうなとき、数学標準の文章逆順合成記号の表記をメインにする。
- 本資料では、関手の作用で文章逆順合成記号の表記をメインにしている。

メリット

頭の中で楽に、脳内変換少なく反芻し自動復習することができるから、身につきやすい。
文章順と文章逆順を行ったり来たりする検討と試行、それ自体が反芻になり身につきやすい。

デメリットとその回避策

数学標準の文章逆順合成記号に慣れている方には負荷に感じるかも。
- サブとして「∘」(数学標準の文章逆順合成記号)による同じ意味の式を併記する。
「;」の記号は省略不可にしているため、煩雑になりがち。
- 省略記法をメインにする。

注意

本資料では等幅フォントを前提とした整形データを記載しています。
しかし現時点のQiitaでは等幅フォントを指定して投稿する手段がありません。
著者の意図通りの整形されたテキストデータを閲覧するために、以下のいずれかの作業をお願いします。

Markdownファイルをダウンロードする。
- Qiitaページの左側にある「…」から「Markdownで本文を見る」をクリック
- ダウンロードされたmdファイルをテキストエディタで開く。
- テキストエディタのフォントを等幅フォントに変える。
  - Windowsではメモ帳が規定で等幅フォント「MS ゴシック」。
  - Ubuntuでは「noto sans mono cjk jp」を適用する。
- 適宜編集することで、理解を深めることもできます。
ブラウザのアドオンを利用する。
- ブラウザにstylusアドオンを導入
- qiita.comの該当ページにアクセス。
- 拡張機能→stylus→拡張機能を開く。
- 「スタイルをUserCSSとして新規作成」をチェック。
- 表示されたURLをクリックすると、CSS編集画面が開く。
- 以下のようにfont-familyをmonospaceに上書きする。
- CSSが反映されるように、更新など適宜ブラウザを操作する。

@-moz-document domain("qiita.com/xxxxxxxx") { /* この行はアドオンで生成されている */
    * {font-family:monospace!important} /* この行を挿入し、フォントを上書きする */
} /* この行はアドオンで生成されている */

凡例

▼▼▼
{圏の記号}(独自)
  ∵テキスト表現の図式にて圏の範囲を見やすくするため
図式  数式+文章
▲▲▲
▽▽▽
サブ記法の図式
△△△
【サブ記法】
((参考文献)) 参考文献の詳細
◎:可換(独自)
  ∵↻が環境やフォントによって半角幅が割り当てられ整形に不利。
  ∵可換と恒等射で記号を区別することで検索性を高める。
⦿:恒等射(独自)
  ∵同上
○:対象　●:強調対象　◇:要素　→:射　⇨:関手(独自)
➡:自然変換(独自)
  ∵⇑⇓が環境やフォントによって半角幅が割り当てられ整形に不利。
  ∵⇒は命題論理の必要条件の意味、コンマ圏の区切りの意味で使用され、重複を嫌った。
:性質「性質名」
∃!h:条件に対してhが一意に存在する

記号一覧

IMEからの変換は面倒なので、コピペするための一覧です。

┌─┐┌┬┐┏━┓┏┳┓
│　│├┼┤┃　┃┣╋┫
└─┘└┴┘┗━┛┗┻┛
⇖↖ ↑⇧⬆⇑⇈ ↗⇗ ↔⇔⇄⇆￣＿
⇇⇐⬅⇦←○→⇨➡⇒⇉●◇◎⦿
⇙↙ ↓⇩⬇⇓⇊ ➘⇘ ↕⇕⇅
∩∧⊥ ∴∵∅×＋∏∐∑
⊣＜⊂∈∘∋⊃＞⊢
∪∨⊤ ∀∃≅≃≒
αΑalpha βΒbeta γΓgamma δΔdelta εΕepsilon ζΖzeta ηΗeta θΘtheta ιΙiota κΚkappa λΛlambda μΜmu νΝnu ξΞxi οΟomicron πΠpai ρΡrho σΣsigma τΤtau υΥupsilon φΦphi χχchi ψΨpsi ωΩomega
ＡＢＣＤＥＦＧＨＩＪＫＬＭＮＯＰＱＲＳＴＵＶＷＸＹＺ:圏・関手用の全角アルファベット

圏論を理解するための考え方

物理学では、剛体・質点という理想的なオブジェクトを想定することで、有効な性質を効果的に調べ、明確に記述している。圏論でも「交換可能」や「ちょうど一つ」という考え方を導入し、剛体のように塊にし、塊の間の相互作用を調べ、記述している。このような考え方は圏論に限らず、代数学・数学全般にある。
物理現象は、ある数学的モデルと突き合わせることで理解していく。数学的現象も、別のある数学的モデルと突き合わせることで理解していく。圏論は突き合わせ自体を理解することを目的の一つとして設計されている。
バスケットボールのトラベリング(軸足ルール)のように、圏論でも対象または射を軸にして、生成される概念の相互作用を調べ、記述していく。動点固定法を地でいっている。

圏

以下から構成されるＣを圏, category と呼ぶ :定義、独自∵プレーンテキストでは太字を表現できないため、全角で代替する。
- 対象, objectとその集まり, class :用語
  A,B,C,...∈Ｃ_0【= Obj(Ｃ) = ob(Ｃ)】:表記例
- 射, morphism【, 矢, arrow】とその集まり :用語
  f:X→Y∈Ｃ_1【= Mor(Ｃ) = arr(Ｃ)】:表記例、「1」の記号は恒等射・圏の射集合・終対象で使用し文脈で意味を区別させる。
  X;f ∈Ｃ_0 :表記:文章順合成記号、対象を射とみなして表記
【= f(X)】:表記:数学標準の文章逆順合成、右から左への合成、左からの作用
【= fX】:表記:数学標準の文章逆順合成記号の省略版
- ドメイン, domain【, 域, 始域, source】
  と余ドメイン, codomain【, 余域, 終域, target】:用語
  前提: f:X→Y∈Ｃ_1
  dom(f) = X ∈Ｃ_0 :表記
  cod(f) = Y ∈Ｃ_0 :表記
- 合成, composition :用語
  前提: f:X→Y, g:Y→Z
  f;g:X→Z∈Ｃ(X,Z) :表記:文章順合成記号
【= g∘f:X→Z】:表記:数学標準の文章逆順合成記号
【= gf:X→Z】:表記:数学標準の文章逆順合成記号の省略表記
  ; :Ｃ(X,Y)×Ｃ(Y,Z)→Ｃ(X,Z) :補足説明:一部表記は後出
【∘:Ｃ(Y,Z)×Ｃ(X,Y)→Ｃ(X,Z)】:補足説明:一部表記は後出
- 恒等射, identity :用語
  1_X = 1【= id_X = id】:X→X :表記例、_Xなしは省略表記、「1」の記号は恒等射・圏の射集合・終対象で使用し文脈で意味を区別させる。
- 結合律, associative law :用語、公理
  前提: f:A→B, g:B→C, h:C→D
  (f;g);h = f;(g;h) = f;g;h
【h∘(g∘f) = (h∘g)∘f = h∘g∘f】
- 単位法則 :用語、公理
  ∀f:X→Y, f = f;1_Y【= 1_Y∘f】
  ∀g:Y→Z, g = 1_Y;g【= g∘1_Y】

対象または射の間の「=」について、前提・言及なしに、
対象律、反射律、推移律を満たす二項関係として使用されている(著者の調査の範囲)。
※前提となる述語論理に含まれるものなのか？

hom集合, hom-set【, 射集合, 射の類, hom-class】:用語
Ｃ(X,Y) :表記
【= hom(X,Y)】:表記
【= hom_Ｃ(X,Y)】:表記
【= H^X(Y)】:表記
【= H_Y(X)】:表記
【= ^Yh(X) = ^Yh_X】:表記、数学標準の文章逆順合成記号「∘」との一貫性を考慮して定義したものと推定する。((西郷-道案内))
【= h_X(Y) = ^Yh_X】:表記、同上。
【= Mor(X,Y)】:表記
【= Mor_Ｃ(X,Y)】:表記
【= A(X,Y)】:表記
【= arr(X,Y)】:表記
= {f|f:X→Y} :定義
Ｃ(X,Y)⊂Ｃ_1 :補足説明
Ｃ(X,Y)∈{Set}_1 :補足説明:各Ｃ(X,Y)が集合の場合、一部表記は後出

▼▼▼
{Ｃ}
X f Y  :補足説明:文字が同じ行に並ぶことで、ある種の視認性が増す。
○→○ :補足説明:ほぼ常に、射の始点終点の記号「○」を記載する∵様々な種類の視認性を増す。

○X ∈Ｃ_0
↓f ∈Ｃ_1
○Y ∈Ｃ_0 :補足説明:文字が同じ列に並ぶことで、ある種の視認性が増す。関手が登場するとより感じられる。

X○-f→○Y :補足説明:他の階層と比較するとき、射・始点終点・文字を1列に並べる。「○」があることで、文字が対象を表すのか、射を表すのか、の視認性が増す。

○X ○Y ∈Ｃ_0
└→┘f ∈Ｃ(X,Y)⊂Ｃ_1 :補足説明:対象関連と射関連をそれぞれ一行にまとめることで、ある種の視認性が増す。

○X ○Y ○Z
└→┘    f           ∈Ｃ(X,Y)
    └→┘g           ∈Ｃ(Y,Z)
└→┴→┘
└──→┘f;g【= g∘f】∈Ｃ(X,Z) :説明:合成

○A ○B ○C ○D
└→┘                f             ∈Ｃ(A,B)
    └→┘            g             ∈Ｃ(B,C)
        └→┘        h             ∈Ｃ(C,D)
└──→┘          f;g【= g∘f】    ∈Ｃ(A,C)
    └──→┘      g;h【= h∘g】    ∈Ｃ(B,D)
└──→┴→┘  (f;g);h【= h∘(g∘f)】∈Ｃ(A,D)
└→┴──→┘= f;(g;h)【= (h∘g)∘f】∈Ｃ(A,D)
└→┴→┴→┘=   f;g;h【= h∘g∘f】  ∈Ｃ(A,D) :補足説明:カッコを省略可
└────→┘(f;g);h = f;(g;h) = f;g;h【⇔ h∘(g∘f) = (h∘g)∘f = h∘g∘f】:説明:結合律

○X ○Y ○Z
    ⦿     1(恒等射) :記号、独自
└→┘     f
└→⦿     = f;1【= 1∘f】
    └→┘ g
    ⦿→┘ = 1;g【= g∘1】:説明:単位律
▲▲▲

Ｃ
= (Ｃ_0,Ｃ_1):表記
【= (Obj(Ｃ),Mor(Ｃ))】:表記
【= (ob(Ｃ),arr(Ｃ))】:表記

可換図式, commutative diagram :用語
▼▼▼
{Ｃ}
○X ○Y ○Z
└→┴→┘f;g【= g∘f】
    ◎    :記号、独自:可換であることを示す、省略されることもある
└──→┘h = f;g【= g∘f】:補足説明:可換⇔「=」が成り立っている
▲▲▲

恒等射の一意性 :性質
証明:
仮定: 1, 1' ∈Ｃ(Y,Y)は恒等射
∀f ∈Ｃ(X,Y), ∀g ∈Ｃ(Y,Z),
f;1【= 1∘f】= f ∵仮定
f;1'【= 1'∘f】= f ∵仮定
1;g【= g∘1】= g ∵仮定
1';g【= g∘1'】= g ∵仮定
∴f;1 = f の f に 1' を代入して 1';1 = 1'
【⇔ 1∘f = f の f に 1' を代入して 1∘1'= 1'】
∴1';g = g の g に 1 を代入して 1';1 = 1
【⇔ g∘1' = g の g に 1 を代入して 1∘1'= 1】
∴1 = 1';1 = 1'
【⇔ 1 = 1∘1' = 1'】//

圏の定義は、Ｃの射の列
▼▼▼
○X0-f1→○X1-f2→...-fn→○Xn
▲▲▲
(n>=0)から、ちょうど一つの射
▼▼▼
    f1;f2;...;fn (結合順序に依存せず)
X0○→○Xn
▲▲▲
が構成できるように設計されている。((Leinster))p13

前提: Ｃは圏
Ｃは局所小, locally small :用語
定義:⇔ ∀X,Y∈Ｃ_0, Ｃ(X,Y)は集合

Σ^*はΣの双対命題, duality :用語
定義:命題Σを以下で置き換える
f;gをg;f【g∘fをf∘g】
domをcod
codをdom

双対原理, duality principle :用語
CT⇒Σ ならば CT⇒Σ^* :性質
補足説明、ある命題が真ならば、その命題の双対命題も真。

fはモノ, mono【, モノ射, モニック, monic, mono-morphism, 単型射, 単射, injection】:用語
定義:⇔∀x,y∈Ｃ(∀A, dom(f)), x;f = y;f【f∘x = f∘y】⇒ x = y
▼▼▼
{Ｃ}
∀x  fはモノ
○⇉○→○ x;f = y;f ⇒ x = y
∀y   【⇔ f∘x = f∘y ⇒ x = y】
▲▲▲

fはエピ, epi【, エピ射, エピック, epic, epi-morphism, 全型射, 全射, surjection】:用語
定義:⇔∀x,y∈Ｃ(cod(f),∀B), f;x = f;y【x∘f = y∘f】⇒ x = y :(上の命題の双対命題)
▼▼▼
{Ｃ}
fはエピ   ∀x
     ○→○⇉○ f;x = f;y ⇒ x = y
          ∀y【⇔ x∘f = y∘f ⇒ x = y】
▲▲▲

前提: Ｃは圏
前提: e:X⇄Y:s
s;e【= e∘s】= 1_Y ⇒ eはエピ かつ sはモノ :性質「分裂エピモノ性」
証明:
仮定: e;y = e;y'【⇔ y∘e = y'∘e】
∴ y
= 1;y【= y∘1】∵単位律
= s;e;y【= y∘e∘s】∵条件
= s;e;y'【= y'∘e∘s】∵仮定
= 1;y'【= y'∘1】∵条件
= y' ∵単位律
∴eはエピ
仮定: x;s = x';s
∴ x
= x;1【= 1∘x】∵単位律
= x;s;e【= s∘e∘x】∵条件
= x';s;e【= s∘e∘x'】∵仮定
= x';1【= 1∘x'】∵条件
= x' ∵単位律
∴sはモノ //

前提: Ｃは圏
前提: e:Y⇄Y:s
前提: s;e【= e∘s】= 1_Y
eは分裂エピ射, split epi-morphism :用語
sは分裂モノ射, split mono-morphism :用語
sはeの切断, section【, 右逆射, right inverse, 断面, splitting】:用語
eはsのレトラクション(引き込み), retraction【, 左逆射, left inverse】:用語
BはAのレトラクト, retract :用語

gはf:X→Yの逆射, inverse :用語
⇔ g = f^-1 :表記、説明:逆射の一意性、後で証明
定義:⇔ f;g = 1_X, g;f = 1_Y
【⇔ g∘f = 1_X, f∘g = 1_Y】

f:X→Yは同型射, iso, iso-morphism :用語
定義:⇔fは逆射を持つ
⇔∃g∈Ｃ(Y,X), f;g = 1_X, g;f = 1_Y
【⇔ ∃g∈Ｃ(Y,X), g∘f = 1_X, f∘g = 1_Y】
⇔∃!f^-1∈Ｃ(Y,X), f;f^-1 = 1_X, f^-1;f = 1_Y
【⇔ ∃!f^-1∈Ｃ(Y,X), f^-1∘f = 1_X, f∘f^-1 = 1_Y】:説明:逆射の一意性、後で証明
⇔fは分裂モノかつ分裂エピ

XとY∈Ｃ_0は同型, iso-morphic :用語
⇔ X≅Y :表記
定義:⇔ ∃f∈Ｃ(X,Y), fは同型射

逆射の一意性 :性質
証明:
仮定: x,y∈Ｃ(Y,X)はfの逆射
∴ f;x = 1_X, x;f = 1_Y, f;y = 1_X, y;f = 1_Y
【⇔x∘f = 1_X, f∘x = 1_Y, y∘f = 1_X, f∘y = 1_Y】
∴f;x = 1_X = f;y
【⇔ x∘f = 1_X = y∘f】でfは分裂エピ射なのでエピ射なので x = y
∴x;f = 1_Y = y;f
【⇔ f∘x = 1_Y = f∘y】でfは分裂モノ射なのでモノ射なので x = y //

fは双射, bi-morphism【, 全単射】:用語
定義:⇔ fはモノかつエピ

同型射 ⇒ モノ、エピ :性質
証明:
「分裂エピモノ性」を以下に適用する
f;f^-1 = 1, f^-1;f = 1
【⇔ f^-1∘f = 1, f∘f^-1 = 1】//

f;g【= g∘f】はモノ ⇒ fはモノ :性質
証明:
仮定: h;f = k;f【f∘h = f∘k】
∴ h;f;g = k;f;g【g∘f∘h = g∘f∘k】
∴ h = k ∵f;g【= g∘f】はモノ //

f;g【= g∘f】はエピ ⇒ gはエピ :性質(上の命題の双対命題)
証明:
仮定: g;h = g;k【⇔ h∘g = k∘g】
∴ f;g;h = f;g;k【⇔ h∘g∘f = k∘g∘f】
∴ h = k ∵f;g【= g∘f】はエピ //

f,gはモノ ⇒ f;g【= g∘f】はモノ :性質
証明:
仮定: h;f;g = k;f;g【⇔ g∘f∘h = g∘f∘k】
∴ h;f = k;f【⇔ f∘h = f∘k】∵gはモノ
∴ h = k ∵fはモノ //

f,gはエピ ⇒ f;g【= g∘f】はエピ :性質(上の命題の双対命題)
証明:
仮定: f;g;h = f;g;k【⇔ h∘g∘f = k∘g∘f】
∴ g;h = g;k【⇔ h∘g = k∘g】∵fはエピ
∴ h = k ∵gはエピ //

  (a) fは同型射
⇔(b) fはモノかつ分裂エピ :性質
⇔(c) fは分裂モノかつエピ :性質
⇔(d) fは分裂モノかつ分裂エピ :性質
証明:
仮定:(a)
同型射 ⇒ モノ,同型射 ⇒ エピは前で証明
fは同型射 ⇒ f^-1はfの逆射
         ⇒  f^-1は分裂モノかつ分裂エピ
∴(b)(c)(d)
仮定:(b)
∴∃g, g;f【= f∘g】= 1 ∵fは分裂エピ
 (f;g);f【= f∘(g ∘f)】
=f;(g;f)【= (f∘ g)∘f】
=f;1【= 1∘f】∵fは分裂エピ
=f
=1;f【= f∘1】
∴f;g【= g∘f】= 1 ∵fはモノ
∴g=f^-1
∴(a)
仮定:(c)
∴∃g, f;g【= g∘f】= 1 ∵fは分裂モノ
 f;(g;f)【= (f∘ g)∘f】
=(f;g);f【= f∘(g ∘f)】
=1;f【= f∘1】∵fは分裂モノ
=f
=f;1【= 1∘f】
∴g;f【= f∘g】= 1 ∵fはエピ
∴g=f^-1
∴(a)
仮定:(d)
分裂モノ ⇒ モノ
分裂エピ ⇒ エピ は前で証明
∴(b)(c) //

集合圏, 集合と写像の圏, Set, Sets, category of sets :用語
Set = (Set_0,Set_1)
集合圏の対象は集合、Set_0 = |Set| = {集合} = 集合の集まり
集合圏の射  は写像 f⊂X×Yかつ x1=x2∈X⇒f(x1)=f(x2)∈Yを満たす任意のもの(f:X→Yと表記する)、Set_1 = {f|f:X→Yは写像} = 写像の集まり
X,Y∈Set_0, f∈Set(X,Y)⊂Set_1
集合圏の射の合成は関数の合成：x;(f;g) = (x;f);g【⇔ (g∘f)(x) = g(f(x))】
集合圏の恒等射は恒等写像：x;1_X【= 1_X(x)】= x

1は圏Ｃの終対象, terminal object :用語
定義:⇔ 1∈Ｃ_0 かつ ∀Y∈Ｃ_0, ∃!h∈Ｃ(Y,1)
⇔ 1∈Ｃ_0 かつ ∀Y∈Ｃ_0, Ｃ(Y,1)が1元集合
⇔ 1∈Ｃ_0 かつ ∀Y∈Ｃ_0, |Ｃ(Y,1)|=1
▼▼▼
●1
↑∃!h
○∀Y
▲▲▲
補足説明:本資料では終対象から極限を定義
補足説明:「1」の記号は恒等射・圏の射集合・終対象で使用し文脈で意味を区別させる。

0は圏Ｃの始対象, initial object :用語(上の命題の双対命題)
定義:⇔ 0∈Ｃ_0 かつ ∀Y∈Ｃ_0, ∃!h∈Ｃ(0,Y)
⇔ 0∈Ｃ_0 かつ ∀Y∈Ｃ_0, Ｃ(0,Y)が1元集合
⇔ 0∈Ｃ_0 かつ ∀Y∈Ｃ_0, |Ｃ(0,Y)|=1
▼▼▼
●0
↓∃!h
○∀Y
▲▲▲
補足説明:本資料では始対象から余極限を定義

終対象は同型を除いて一意 :性質
証明:
仮定: XとYは終対象
▼▼▼
{Ｃ}
○X ○Y
└→┘ ∃!u ∵Yは終対象
└←┘ ∃!v ∵Xは終対象
▲▲▲
u;v【=v∘u】:X→X, 1_X:X→X, v;u【=u∘v】:Y→Y, 1_Y:Y→Y
Xは終対象なのでf:X→Xとなるfは一意∴f=u;v【=v∘u】=1_X
Yは終対象なのでg:Y→Yとなるgは一意∴g=v;u=【=u∘v】1_Y
∴X ≅ Y //

始対象は同型を除いて一意 :性質(上の命題の双対命題)
証明:
仮定: XとYは始対象
▼▼▼
{Ｃ}
○X ○Y
└→┘ ∃!u ∵Xは始対象
└←┘ ∃!v ∵Yは始対象
▲▲▲
u;v【=v∘u】:X→X, 1_X:X→X, v;u【=u∘v】:Y→Y, 1_Y:Y→Y
Xは始対象なのでf:X→Xとなるfは一意∴f=u;v【=v∘u】=1_X
Yは始対象なのでg:Y→Yとなるgは一意∴g=v;u【=u∘v】=1_Y
∴X ≅ Y //

関手

前提: Ａ,Ｂは圏
Ｆ【= (Ｆ_0,Ｆ_1) = (Ｆ,Ｆ)】:Ａ⇨Ｂは関手, functor【, 函手】:用語
定義:⇔
- Ｆ_0:Ａ_0⇨Ｂ_0 :説明:関手ＦはＡのすべての対象に作用する
- Ｆ_1:Ａ_1⇨Ｂ_1 :説明:関手ＦはＡのすべての射に作用する、下の性質に含まれるので一般には明記されない
- ∀X,Y ∈Ａ_0, Ｆ_1:Ａ(X,Y)⇨Ｂ(ＦX,ＦY)
           【⇔ Ｆ_1:Ａ(X,Y)⇨Ｂ(X;Ｆ,Y;Ｆ)】:説明:ドメインとコドメインを保つ
- ∀X∈Ａ_0, Ｆ(1_X) = 1_ＦX
       【⇔ 1_X;Ｆ = 1_(X;Ｆ)】:説明:恒等射を保つ
- ∀f:X→Y, ∀g:Y→Z, Ｆ(f;g) = Ｆf;Ｆg
                【⇔ (f;g);Ｆ = (f;Ｆ);(g;Ｆ)
                  ⇔  Ｆ(g∘f) = Ｆg∘Ｆf】:説明:合成を保つ、すなわち準同型
▼▼▼
  {Ａ} Ｆ  ⇨ {Ｂ}
∀X○  Ｆ_0⇨ ○ＦX【=X;Ｆ】:説明:対象に作用する
∀f↓◎Ｆ_1⇨ ↓Ｆf【=f;Ｆ】:説明:射に作用する、ドメインとコドメインを保つ
∀Y○  Ｆ_0⇨ ○ＦY【=Y;Ｆ】
{Set} :補足説明:ＡとＢが局所小の場合
○Ａ(∀X,∀Y)
⇩Ｆ_( X,  Y)
○Ｂ(ＦX,ＦY)
【=Ｂ(X;Ｆ,Y;Ｆ)】:説明:ドメインとコドメインを保つ

{Ａ}  ∀X○ ⦿1_X
⇩Ｆ Ｆ_0⇩ ⇩Ｆ_1
{Ｂ} ＦX ○ ⦿1_ＦX = Ｆ(1_X)
  【X;Ｆ      1_{X;Ｆ} = 1_X;Ｆ】:説明:恒等射を保つ

{Ａ}
○X ○Y ○Z ∀
└→┘      ∀f
    └→┘  ∀g
└→┴→┘
└──→┘  f;g【= g∘f】
⇩Ｆ
{Ｂ}
【X;Ｆ Y;Ｆ Z;Ｆ】
ＦX ＦY ＦZ
○  ○  ○
└→┘     Ｆf     【=  f;Ｆ       =    Ｆf】
    └→┘     Ｆg 【=        g;Ｆ =Ｆg    】
└→┴→┘ Ｆf;Ｆg 【=(f;Ｆ);(g;Ｆ)=Ｆg∘Ｆf】
└──→┘ =Ｆ(f;g)【=     (f;g);Ｆ=Ｆ(g∘f)】:説明:合成を保つ、すなわち準同型
▲▲▲

関手の定義は、Ａの射の列
▼▼▼
○X0-f1→○X1-f2→...-fn→○Xn
▲▲▲
(n>=0)から、ちょうど一つの可能なＢの射
▼▼▼
○ＦX0-Ｆ(f1;f2;...;fn)→○ＦXn
▲▲▲
▽▽▽
○(X0;Ｆ)-(f1;f2;...;fn);Ｆ→○(Xn;Ｆ)
○ＦX0-Ｆ(fn∘...∘f2∘f1)→○ＦXn
△△△
(結合・作用順序に依存せず)が構成できるように設計されている。((Leinster))p21

例: RDB
前提:Ｃ=(Ｃ_0,Ｃ_1)=(Ｃ,Ｃ)
1つのデータベーススキーマ≅圏の一部のグラフ
▼▼▼
{Ｃ}       FK1     ∈Ｃ(TBL0,TBL1)⊂Ｃ_1
Ｃ_0∋TBL0┬→TBL1 ∈Ｃ_0
          └→TBL2 ∈Ｃ_0
           FK2     ∈Ｃ(TBL0,TBL2)⊂Ｃ_1
▲▲▲
圏の要素を表で表示
▼▼▼
|arrow   source target|  |vertex|
|(矢印) (始点) (終点)|  |(頂点)|
|FK0     TBL0   TBL1  |  |TBL0  |
|FK1     TBL0   TBL2  |  |TBL1  |
                         |TBL2  |
▲▲▲
1つのインスタンス≅1つの関手
▼▼▼
       TBL0               TBL1   TBL2
{Ｃ}  |ID   FK1  FK2 |   |ID  | |ID  |
   Ｆ_0⇩   ⇩Ｆ_1
{Set} |id00 id10 id20|   |id10| |id20|
      |id01 id10 id21|   |id11| |id21|
      |id02 id11 id21|
▲▲▲
1つのインスタンスをグラフ表示
▼▼▼
{Ｃ}     Ｆ⇨ {Set}
○TBL1 Ｆ_0⇨ ○{id10,     id11}
↑     Ｆ_1⇨ ↑  ↑_↖_   ↑_
○TBL0 Ｆ_0⇨ ○{id00,id01,id02}
↓     Ｆ_1⇨ ↓  ↓￣ ￣➘↓￣
○TBL2 Ｆ_0⇨ ○{id20,     id21}
▲▲▲

前提: Ｆ:Ａ⇨Ｂは関手
Ｆが対象について単射 定義:⇔Ｆ_0:Ａ_0⇨Ｂ_0 が単射
Ｆが対象について全射 定義:⇔Ｆ_0:Ａ_0⇨Ｂ_0 が全射
Ｆが射について単射 定義:⇔Ｆ_1:Ａ_1⇨Ｂ_1 が単射
Ｆが射について全射 定義:⇔Ｆ_1:Ａ_1⇨Ｂ_1 が全射

前提: Ｆ:Ａ⇨Ｂは関手
Ｆが忠実, faithful :用語
定義:⇔ ∀X,Y∈Ａ_0, ∀f,f':X→Y, Ｆf = Ｆf' ⇒ f = f'
【⇔ ∀X,Y∈Ａ_0, ∀f,f':X→Y, f;Ｆ = f';Ｆ ⇒ f = f'】
説明:fが高々1個 ⇔ 最大1個 ⇔ (0個 or 1個) ⇔ 2個以上存在すればそれらは等しい。((Leinster))p29
▼▼▼
{Set}
○Ａ(∀X,∀Y)∋  f = f'   {Ａ}
⇩Ｆ_{ X,  Y}     _⇑
○Ｂ(ＦX,ＦY)∋Ｆf = Ｆf' {Ｂ}
▲▲▲
▽▽▽
{Set}              ∀f ∀f'
○Ａ(∀X,∀Y   )∋   f = f'    {Ａ}
⇩Ｆ_{X,   Y   }      _⇑
○Ｂ( X;Ｆ,Y;Ｆ)∋f;Ｆ = f';Ｆ {Ｂ}
△△△

前提: Ｆ:Ａ⇨Ｂは関手
Ｆは充満, full :用語
定義:⇔ ∀X,Y∈Ａ_0, ∀g:ＦX→ＦY, ∃f:X→Y, g = Ｆf
【⇔ ∀X,Y∈Ａ_0, ∀g:X;Ｆ→Y;Ｆ, ∃f:X→Y, g = f;Ｆ】
説明:fが少なくても1個 ⇔ 最小1個 ⇔ 1個以上 ⇔ 存在する。((Leinster))p29
▼▼▼
{Set}
○Ａ(∀X,∀Y)∋∃f          {Ａ}
⇩Ｆ_{ X,  Y}
○Ｂ(ＦX,ＦY)∋∀g, g = Ｆf {Ｂ}
▲▲▲
▽▽▽
{Set}
○Ａ(∀X,∀Y)   ∋∃f           {Ａ}
⇩Ｆ_{X,   Y}
○Ｂ( X;Ｆ,Y;Ｆ)∋∀g, g = f;Ｆ {Ｂ}
△△△

前提: Ｆ:Ａ⇨Ｂは関手
前提: X,Y∈Ａ_0
X≅Y ⇒ ＦX≅ＦY :性質((Leinster))p31
証明:
f:X→Y, g:Y→X, f;g = 1, g;f = 1 ∵X≅Y
Ｆf;Ｆg = Ｆ1_X = 1_ＦX, Ｆg;Ｆf = Ｆ1_Y = 1_ＦY
ＦX≅ＦY //

前提: Ｆ:Ａ⇨Ｂは充満忠実関手
前提: X,Y∈Ａ_0
f∈Ａ_1は同型 ⇔ Ｆf∈Ｂ_1は同型 :性質
証明:
⇒は前の性質
仮定: Ｆf:ＦA→ＦA'は同型射
仮定: h:Ｆf^-1とする
∃g:Y→X, h=Ｆg ∵Ｊは充満
f;g = 1, g;f = 1 ∵Ｊは忠実
∴⇐が成り立つ //

前提: Ｆ:Ａ⇨Ｂは充満忠実関手
前提: X,Y∈Ａ_0
∀g:ＦX→ＦY∈Ｂ_1は同型, ∃f:X→Yは同型, Ｆf = g :性質
証明:
∃f:X→Y, g=Ｆf ∵Ｆは充満
前の性質よりfは同型 //

前提: Ｆ:Ａ⇨Ｂは充満忠実関手
前提: X,Y∈Ａ_0
X,Y∈Ａ_0は同型 ⇔ ＦX,ＦY∈Ｂ_1は同型 :性質((Leinster))p124
証明:
⇒はＦが関手なので成り立つ。
⇐は前の性質より成り立つ //

自然変換

前提: Ａ,Ｂは圏
前提: Ｆ,Ｇ:Ａ⇨Ｂは関手
n:Ｆ➡Ｇは自然変換, natural transformation :表記 :用語
定義:⇔ n_X={f:ＦX→ＧX|X∈Ａ_0}⊂Ｂ_1 かつ ∀f:X→Y, Ｆf;n_Y = n_X;Ｇf
【⇔ n_X={f:X;Ｆ→X;Ｇ|X∈Ａ_0}⊂Ｂ_1 かつ ∀f:X→Y, (f;Ｆ);n_Y = n_X;(f;Ｇ)
  ⇔ n_X={f:ＦX→ＧX|X∈Ａ_0}⊂Ｂ_1 かつ ∀f:X→Y, n_Y∘Ｆf = Ｇf∘n_X】自然性公理 :用語
n_Xを自然変換nのX成分, component【, コンポーネント】と呼ぶ :用語
▼▼▼
{[Ａ,Ｂ]}                             {Set}
    ┌  {Ａ} →∀X●-∀f→○∀Y→  ∈Ａ(∀X, ∀Y)
    │            ⇩  ⇩  ⇩
Ｆ●├⇨{Ｂ} →ＦX●-Ｆf→○ＦY→  ∈Ｂ(ＦX, ＦY)
 n⬇│          n_X↓  ◎  ↓n_Y       :用語:自然性公理
Ｇ○└⇨     →ＧX○-Ｇf→○ＧY→  ∈Ｂ(ＧX, ＧY)
▲▲▲
▽▽▽
{[Ａ,Ｂ]}                                {Set}
    ┌  {Ａ}  →∀X●─∀f→○∀Y→   ∈Ａ(∀X, ∀Y)
    │             ⇩   ⇩  ⇩
Ｆ●├⇨{Ｂ} →X;Ｆ●-f;Ｆ→○Y;Ｆ→  ∈Ｂ(X;Ｆ,Y;Ｆ)
 n⬇│           n_X↓  ◎   ↓n_Y        :用語:自然性公理
Ｇ○└⇨     →X;Ｇ○-f;Ｇ→○Y;Ｇ→  ∈Ｂ(X;Ｇ,Y;Ｇ)
△△△
自然変換の定義は、Ａの各射 f:X→Y について、Ｂの射 ＦX→ＧY【X;Ｆ→Y;Ｇ】がちょうど一つできるように設計されている。
「ちょうど一つ」とは上記が可換図式であることを含意している。((Leinster))p33
自然性公理は、属{n_X}が全てのX∈Ａ_0にわたって「一様」に定義されているという考え方を捉えている。((Leinster))p35

自然変換 :表記
▼▼▼
┌ Ｆ⇨┐
{Ａ}n⬇{Ｂ}
└ Ｇ⇨┘
▲▲▲

関手圏, functor category【, category of functors】:用語
前提: Ａ,Ｂは圏
関手圏の対象は関手Ｆ:Ａ⇨Ｂ
関手圏の射  は自然変換 n:Ｆ➡Ｇ
合成は垂直合成, vertical composition :用語
n0;n1【n1∘n0】:表記
[Ａ,Ｂ] = Ｂ^Ａ【= Fun(Ａ,Ｂ)= Funct(Ａ,Ｂ)】:表記
▼▼▼
{Ａ} {Ｂ}
└Ｆ⇨┘
  n0⬇
└Ｇ⇨┘
  n1⬇
└Ｈ⇨┘
▲▲▲
[Ａ,Ｂ](Ｆ,Ｇ) = 関手圏[Ａ,Ｂ]の関手Ｆから関手Ｇへの自然変換の集まり :意味
Ｃ(X,Y) (圏Ｃの対象Aから対象Bへの射の集まり)の表記を適用したもの :補足説明

前提: Ａ,Ｂは圏
前提: Ｆ,Ｇ:Ａ⇨Ｂは関手
n:Ｆ≅Ｇは自然同型, natural isomorphism :表記 :用語
定義:⇔ nは[Ａ,Ｂ]の同型射

前提: Ｆ,Ｇ:Ａ⇨Ｂは関手
前提: α:Ｆ➡Ｇは自然変換
αは自然同型 ⇔ ∀X∈Ａ, α_X:ＦX→ＧXは同型射
          【⇔ ∀X∈Ａ, α_X:X;Ｆ→X;Ｇは同型射】:性質「自然変換の同型」
証明:
仮定: αは自然同型
∴∃β, β;α = 1_Ｇ, α;β = 1_Ｆ
【⇔ ∃β, α∘β = 1_Ｇ, β∘α = 1_Ｆ】
▼▼▼
┌────Ｆ⇨┐
{Ａ}α⬇ ∃β⬆{Ｂ}
└────Ｇ⇨┘
▲▲▲
∴∀A∈Ａ, β_A;α_A = 1_ＧA, α_A;β_A = 1_ＦA
【⇔ ∀A∈Ａ, β_A;α_A = 1_(A;Ｇ), α_A;β_A = 1_(A;Ｆ)
  ⇔ ∀A∈Ａ, α_A∘β_A = 1_ＧA, β_A∘α_A = 1_ＦA】
∴ α_A:ＦA→ＧA
【⇔ α_A:A;Ｆ→A;Ｇ】は同型射
仮定: ∀X∈Ａ, α_X:ＦX→ＧX
 【⇔ ∀X∈Ａ, α_X:X;Ｆ→X;Ｇ】は同型射
∴∃β, β_X:ＧX→ＦX, β_X;α_X = 1_ＧX, α_X;β_X = 1_ＦX
【⇔ ∃β, β_X:X;Ｇ→X;Ｆ, β_X;α_X = 1_(X;Ｇ), α_X;β_X = 1_(X;Ｆ)
  ⇔ ∃β, β_X:ＧX→ＦX, α_X∘β_X = 1_ＧX, β_X∘α_X = 1_ＦX】
▼▼▼
      α_X
ＦX○  ⇄ ○ＧX
   │ β_X │
Ｆf↓ α_Y ↓Ｇf
ＦY○  ⇄ ○ＧY
      β_Y
▲▲▲
▽▽▽
       α_X
X;Ｆ○  ⇄  ○X;Ｇ
    │ β_X  │
f;Ｆ↓ α_Y  ↓f;Ｇ
Y;Ｆ○  ⇄  ○Y;Ｇ
       β_Y
△△△
   β_X; Ｆf            【=  β_X;  (f;Ｆ)             =            Ｆf ∘β_X 】
= (β_X; Ｆf);(α_Y ;β_Y)【= (β_X; (f;Ｆ));(α_Y ;β_Y) = (β_Y∘ α_Y)∘(Ｆf ∘β_X)】
=  β_X;(Ｆf ; α_Y);β_Y 【=  β_X;((f;Ｆ);  α_Y);β_Y  =  β_Y∘(α_Y ∘ Ｆf)∘β_X 】
=  β_X;(α_X ; Ｇf);β_Y 【=  β_X; (α_X; (f;Ｇ));β_Y  =  β_Y∘(Ｇf ∘  α_X)∘β_X 】∵αは自然変換
= (β_X; α_X);(Ｇf ;β_Y)【= (β_X;  α_X);((f;Ｇ);β_Y) = (β_Y∘ Ｇf)∘(α_X ∘β_X)】
=              Ｇf ;β_Y 【=              (f;Ｇ);β_Y  =  β_Y∘ Ｇf            】
∴βは自然変換 //

前提: Ｆ:Ａ×Ｂ⇨Ｃ
Ｆ^A(B) = Ｆ(A,B)   :定義:関手の対象の対応
Ｆ^A(g) = Ｆ(1_A,g) :定義:関手の射  の対応
Ｆ^A:Ｂ⇨Ｃは関手  :性質((Leinster))p31
証明:
Ｆ(f;f',g;g') = Ｆ(f,g);Ｆ(f',g')でf = f' = 1_Aとして
Ｆ^A(g;g') = Ｆ(1_A,g;g') = Ｆ(1_A;1_A,g;g') = Ｆ(1_A,g);Ｆ(1_A,g') = Ｆ^A(g);Ｆ^A(g')
【Ｆ(f'∘f,g'∘g) = Ｆ(f',g')∘Ｆ(f,g)でf = f' = 1_Aとして
Ｆ^A(g'∘g) = Ｆ(1_A,g'∘g) = Ｆ(1_A;1_A,g'∘g) = Ｆ(1_A,g')∘Ｆ(1_A,g) = Ｆ^A(g')∘Ｆ^A(g)】//

前提: Ｆ:Ａ×Ｂ⇨Ｃ
Ｆ_B(A) = Ｆ(A,B)   :定義:関手の対象の対応
Ｆ_B(f) = Ｆ(f,1_B) :定義:関手の射  の対応
Ｆ_B:Ａ⇨Ｃは関手  :性質
証明: 上の性質と同様 //

前提: Ｆ:Ａ×Ｂ⇨Ｃ
Ｆ^A(B) = Ｆ_B(A) :性質
Ｆ_B(f);Ｆ^A'(g) = Ｆ^A(g);Ｆ_B'(f) :性質((Leinster))p31
証明:
Ｆ^A(B) = Ｆ(A,B) = Ｆ_B(A)
  Ｆ_B(f)  ;Ｆ^A'  (g)
= Ｆ(f,1_B);Ｆ(1_A',g)
= Ｆ(f,g)
= Ｆ(1_A,g);Ｆ(f,1_B')
= Ｆ^A  (g);Ｆ_B'(f)
【Ｆ^A'(g)∘Ｆ_B(f)  
=Ｆ(1_A',g)∘Ｆ(f,1_B)
=Ｆ(f,g)
=Ｆ(f,1_B')∘Ｆ(1_A,g)
=Ｆ_B'(f)∘Ｆ^A(g)】//

前提: Ａ,Ｂ,Ｃは圏
Ｆ^AとＦ_Bの性質を満たす関手Ｆ:Ａ×Ｂ⇨Ｃは存在し、かつ1つである :性質((Leinster))p31
証明:
Ｆ(A,B) = Ｆ^A(B) = Ｆ_B(A) :定義:関手の対象の対応
Ｆ(f,g) = Ｆ_B(f);Ｆ^A'(g) = Ｆ^A(g);Ｆ_B'(f) :定義:関手の射の対応
  Ｆ(f;f',g;g')
= Ｆ_B(f;f');Ｆ^A''(g;g')
= (Ｆ_B(f); Ｆ_B(f'));(Ｆ^A''(g) ;Ｆ^A''(g'))
=  Ｆ_B(f);(Ｆ_B(f') ; Ｆ^A''(g));Ｆ^A''(g')
=  Ｆ_B(f);(Ｆ^A'(g) ; Ｆ_B'(f'));Ｆ^A''(g')  ∵Ｆ^AとＦ_Bの性質
= (Ｆ_B(f); Ｆ^A'(g));(Ｆ_B'(f') ;Ｆ^A''(g'))
= Ｆ(f,g);Ｆ(f',g')
【Ｆ(f'∘f,g'∘g)
=Ｆ^A''(g'∘g)∘Ｆ_B(f'∘f)
=(Ｆ^A''(g')∘Ｆ^A''(g))∘(Ｆ_B(f')∘Ｆ_B(f))
=Ｆ^A''(g')∘(Ｆ^A''(g)∘Ｆ_B(f'))∘Ｆ_B(f)
=Ｆ^A''(g')∘(Ｆ_B'(f')∘Ｆ^A'(g))∘Ｆ_B(f)  ∵Ｆ^AとＦ_Bの性質
=(Ｆ^A''(g')∘Ｆ_B'(f'))∘(Ｆ^A'(g)∘Ｆ_B(f))
=Ｆ(f',g')∘Ｆ(f,g)】
∴Ｆ:Ａ×Ｂ⇨Ｃを構成できた
仮定: Ｇ:Ａ×Ｂ⇨Ｃは同じ性質を満たす関手
  Ｇ(f,g)
= Ｇ(1_A;f,g;1_B')
= Ｇ(f,1_B);Ｇ(1_A',g)
= Ｇ_B(f);Ｇ^A'(g)
= Ｆ_B(f);Ｆ^A'(g) ∵性質を満たすものは同じという前提
= Ｆ(f,1_B);Ｆ(1_A',g)
= Ｆ(1_A;f,g;1_B')
= Ｆ(f,g)
【Ｇ(f,g)
= Ｇ(f∘1_A,1_B'∘g)
= Ｇ(1_A',g)∘Ｇ(f,1_B)
= Ｇ^A'(g)∘Ｇ_B(f)
= Ｆ^A'(g)∘Ｆ_B(f) ∵性質を満たすものは同じという前提
= Ｆ(1_A',g)∘Ｆ(f,1_B)
= Ｆ(f∘1_A,1_B'∘g)
= Ｆ(f,g)】
∴ Ｆ = Ｇ //

前提: Ｆ,Ｇ:Ａ×Ｂ⇨Ｃ
∀A∈Ａ, ∃Ｆ^A,Ｇ^A:Ａ⇨Ｃ
∀B∈Ｂ, ∃Ｆ^B,Ｇ^B:Ａ⇨Ｃ
(α_A,B:Ｆ(A,B)→Ｇ(A,B))_{A∈Ａ,B∈Ｂ}は自然変換Ｆ➡Ｇ
⇔(1)(2)がともに成り立つ
(1) ∀A∈Ａ, (α_A,B:Ｆ^A(B)→Ｇ^A(B))_{B∈Ｂ}は自然変換Ｆ^A➡Ｇ^A
(2) ∀B∈Ｂ, (α_A,B:Ｆ_B(A)→Ｇ_B(A))_{A∈Ａ}は自然変換Ｆ_B➡Ｇ_B :性質((Leinster))p46
証明:
⇒を示す。
仮定: Ｆ➡Ｇは自然変換
Ｆ(f,g);α_A',B’ = α_A,B;Ｇ(f,g) ∵仮定
A=A', f=1_Aとすると(1)がなりたつ
B=B', g=1_Bとすると(2)がなりたつ
⇐を示す。
以下が可換になる
▼▼▼
Ｆ^A (B )○-α_A ,B →○Ｇ^A (B )
Ｆ^A (g )↓          ↓Ｇ^A (g ) ∵(1)
Ｆ^A (B')○-α_A ,B'→○Ｇ^A (B')
         ||          ||
Ｆ_B'(A )○-α_A ,B'→○Ｇ_B'(A )
Ｆ_B'(f )↓          ↓Ｇ_B'(f ) ∵(2)
Ｆ_B'(A')○-α_A',B'→○Ｇ_B'(A')
▲▲▲
∴Ｆ(f,g)         ;α_A',B'
= Ｆ^A(g);Ｆ_B'(f);α_A',B'
= α_A ,B;Ｇ^A (g );Ｇ_B'(f ) ∵図式より
= α_A ,B;Ｇ(f,g)
【α_A',B'∘Ｆ(f,g)
=α_A',B'∘Ｆ^A(g)∘Ｆ_B'(f)
=Ｇ_B'(f)∘Ｇ^A (g)∘α_A ,B ∵図式より
=Ｇ(f,g)∘α_A ,B】//

前提: Ａ,Ｂは圏
Ａ,Ｂは圏同値, 自然同値, equivalencd of categories :用語
⇔ Ａ≃Ｂ :記号
定義:⇔∃Ｆ:Ａ⇄Ｂ:∃Ｇ, Ｆ;Ｇ ≅ 1_Ａ, Ｇ;Ｆ ≅ 1_Ｂ
   【⇔∃Ｆ:Ａ⇄Ｂ:∃Ｇ, Ｇ∘Ｆ ≅ 1_Ａ, Ｆ∘Ｇ ≅ 1_Ｂ】
⇔ ∃Ｆ:Ａ⇄Ｂ:∃Ｇ, η:1_Ａ→Ｆ;Ｇとε:Ｇ;Ｆ→1_Ｂは自然同型
【⇔ ∃Ｆ:Ａ⇄Ｂ:∃Ｇ, η:1_Ａ→Ｇ∘Ｆとε:Ｆ∘Ｇ→1_Ｂは自然同型】

「同じ」概念の比較
対象 所属       性質
元   ある集合   同一 x=y
関数 ある集合   同一 f=g
対象 ある圏     同一 X=Y
射   ある圏     同一 f=g
圏   -          同一 Ａ=Ｂ
関手 ある関手圏 同一 Ｆ=Ｇ
対象 ある圏     同型 X≅Y ⇔ ∃f:X⇄Y:∃g, f;g = 1_X, g;f = 1_Y
                        【⇔ ∃f:X⇄Y:∃g, g∘f = 1_X, f∘g = 1_Y】
関手 ある関手圏 自然同型 Ｆ≅Ｇ ⇔ ∃α∈[Ａ,Ｂ](Ｆ,Ｇ), ∃β∈[Ａ,Ｂ](Ｇ,Ｆ), α;β = 1_Ｆ, β;α = 1_Ｇ
                              【⇔ ∃α∈[Ａ,Ｂ](Ｆ,Ｇ), ∃β∈[Ａ,Ｂ](Ｇ,Ｆ), β∘α= 1_Ｆ, α∘β = 1_Ｇ】
圏   ある関手圏 同型 Ａ≅Ｂ ⇔ ∃Ｆ:Ａ⇄Ｂ:∃Ｇ, Ｆ;Ｇ = 1_Ａ, Ｇ;Ｆ = 1_Ｂ
                          【⇔ ∃Ｆ:Ａ⇄Ｂ:∃Ｇ, Ｇ∘Ｆ = 1_Ａ, Ｆ∘Ｇ = 1_Ｂ】
圏   ある関手圏 同値 Ａ≃Ｂ ⇔ ∃Ｆ:Ａ⇄Ｂ:∃Ｇ, Ｆ;Ｇ ≅ 1_Ａ, Ｇ;Ｆ ≅ 1_Ｂ
                          【⇔ ∃Ｆ:Ａ⇄Ｂ:∃Ｇ, Ｇ∘Ｆ ≅ 1_Ａ, Ｆ∘Ｇ ≅ 1_Ｂ】

hom関手

Ｃ((),-):Ｃ^op⇨[Ｃ,Set] つまり反変関手を以下のように定める(自然性公理・関手の準同型などが成り立つように定める) :定義
各A∈Ｃ^op_0           について、Ｃ(A,-)∈[Ｃ,Set]_0 :hom共変関手, hom関手, hom functor:用語と性質
各A∈Ｃ^op_0と各B∈Ｃ_0について、Ｃ(A,B)∈Set_0 :関手の対象の定義
各A∈Ｃ^op_0と各b∈Ｃ_1について、Ｃ(A,b)∈Set_1 :関手の射  の定義
各a∈Ｃ^op_1           について、Ｃ(a,-)∈[Ｃ,Set](Ｃ(A ,-),Ｃ(A',-))⊂[Ｃ,Set]_1 つまり自然変換
各a∈Ｃ^op_1と各B∈Ｃ_1について、Ｃ(a,B)∈Set_1 :自然変換Ｃ(a,-)のB成分
Ｃ(A,b:B→B') 定義:= {(x, x;b【=b∘x】)|x∈Ｃ(A,B)}⊂Ｃ(B',B)×Ｃ(A,B') :関数を直積の部分として表示
Ｃ(a:A'→A,B) 定義:= {(x, a;x【=x∘a】)|x∈Ｃ(A,B)}⊂Ｃ(A',A)×Ｃ(A',B) :関数を直積の部分として表示
▼▼▼
{Ｃ^op}⇨{[Ｃ,Set]}┌  {Ｃ}         →B● ────b→○B'→
       └Ｃ((),-)  │                  ⇩        ⇩  ⇩
A ●   ⇨Ｃ(A ,-)●├⇨{Set} →Ｃ(A ,B)●─Ｃ(A ,b)→○Ｃ(A ,B')→
a ↑   ⇨Ｃ(a ,-)⬇│          Ｃ(a ,B)↓      ◎    ↓Ｃ(a ,B')
A'○   ⇨Ｃ(A',-)○└⇨      →Ｃ(A',B)○─Ｃ(A',b)→○Ｃ(A',B')→
▲▲▲
別記号体系での図式
▽▽▽
{Ｃ^op}⇨{[Ｃ,Set]}┌  {Ｃ}        →B●────b→○B'→
       └H^-       │                 ⇩       ⇩  ⇩
A ●   ⇨   H^-A ●├⇨{Set} →H^A (B)●─H^A (b)→○H^A (B')→
a ↑   ⇨   H^-a ⬇│          H^a (B)↓     ◎    ↓H^a (B')
A'○   ⇨   H^-A'○└⇨      →H^A'(B)○─H^A'(b)→○H^A'(B')→
△△△
別記号体系での図式((西郷-道案内))
▽▽▽
{Ｃ^op}⇨{[Ｃ,Set]}┌  {Ｃ}        →B●────b→○B'→
       └h_-       │                 ⇩       ⇩  ⇩
A ●   ⇨    h_A ●├⇨{Set} →h_A (B)●─h_A (b)→○h_A (B')→
a ↑   ⇨    h_a ⬇│          h_a (B)↓     ◎    ↓h_a (B')
A'○   ⇨    h_A'○└⇨      →h_A'(B)○─h_A'(b)→○h_A'(B')→
△△△
別記号体系での図式(独自、実験的、文章逆順合成記号∘から類推)
※補足説明:圏論標準での「-∘a」記号はこの図式の「B;a」相当でも使用されるので、知らずにいると理解を妨げるかもしれない。
▽▽▽
{Ｃ^op}⇨{[Ｃ,Set]}┌  {Ｃ}     →B●─b ─→○B'→
       └-∘()       │             ⇩    ⇩  ⇩
A ●   ⇨    -∘A ●├⇨{Set} →B∘A ●─b∘A →○B'∘A→
a ↑   ⇨    -∘a ⬇│          B∘a ↓   ◎   ↓B'∘a
A'○   ⇨    -∘A'○└⇨      →B∘A'○─b∘A'→○B'∘A'→
△△△
別記号体系での図式(独自、実験的、文章順合成記号を使用)
▽▽▽
{Ｃ^op}⇨{[Ｃ,Set]}┌  {Ｃ}     →B●── b→○B'→
       └();-       │             ⇩    ⇩  ⇩
A ●   ⇨    A ;-●├⇨{Set} →A ;B●─A ;b→○A';B'→
a ↑   ⇨    a ;-⬇│          a ;B↓   ◎   ↓a ;B'
A'○   ⇨    A';-○└⇨      →A';B○─A';b→○A';B'→
△△△
文章順合成記号による独自図式で、Set内の途中演算をかっこで示す。
▽▽▽
{Ｃ^op}⇨{[Ｃ,Set]}┌  {Ｃ}        →B●─────── b→○B'→
       └();-       │                ⇩              ⇩  ⇩
A ●   ⇨    A ;-●├⇨{Set} →A(;x);B●─── A(;x;B);b→○A(;x;B;b);B'→
a ↑   ⇨    a ;-⬇│        a(;A;x);B↓         ◎        ↓a(;A;x;B;b);B'
A'○   ⇨    A';-○└⇨  →A'(a;A;x);B○─A'(;a;A;x;B);b→○A'(a;A;x;B;b);B'→
△△△

Ｃ(-,()):Ｃ⇨[Ｃ^op,Set] つまり共変関手を以下のように定める(自然性公理・関手の準同型などが成り立つように定める) :定義
  :米田埋め込み, Yoneda embeddingと呼ぶ :用語
各B∈Ｃ_0              について、Ｃ(-,B)∈[Ｃ^op,Set]_0 :hom反変関手, hom contravariant functor:用語と性質
各B∈Ｃ_0と各A∈Ｃ^op_0について、Ｃ(A,B)∈Set_0 :関手の対象の定義
各B∈Ｃ_0と各a∈Ｃ^op_1について、Ｃ(a,B)∈Set_1 :関手の射  の定義
各b∈Ｃ_1              について、Ｃ(-,b)∈[Ｃ^op,Set](Ｃ(-,B ),Ｃ(-,B'))⊂[Ｃ^op,Set]_1 つまり自然変換
各b∈Ｃ_1と各A∈Ｃ^op_1について、Ｃ(A,b)∈Set_1 :自然変換Ｃ(-,b)のA成分
Ｃ(a:A'→A,B) 定義:= {(x, a;x【=x∘a】)|x∈Ｃ(A,B)}⊂Ｃ(A',A)×Ｃ(A',B) :関数を直積の部分として表示:再掲
Ｃ(A,b:B→B') 定義:= {(x, x;b【=b∘x】)|x∈Ｃ(A,B)}⊂Ｃ(B',B)×Ｃ(A,B') :関数を直積の部分として表示:再掲
▼▼▼
{Ｃ}⇨{[Ｃ^op,Set]}┌{Ｃ^op}        ←A●←──a ──○A'←
    └Ｃ(-,())     │                  ⇩        ⇩  ⇩
B ●⇨   Ｃ(-,B )●├⇨{Set} →Ｃ(A,B )●─Ｃ(a,B )→○Ｃ(A',B )→
b ↓⇨   Ｃ(-,b )⬇│          Ｃ(A,b )↓     ◎     ↓Ｃ(A',b )
B'○⇨   Ｃ(-,B')○└⇨      →Ｃ(A,B')○─Ｃ(a,B')→○Ｃ(A',B')→
▲▲▲
別記号体系での図式
▽▽▽
{Ｃ}⇨{[Ｃ^op,Set]}┌{Ｃ^op}       ←A●←───a─○A' ←
    └H_-          │                 ⇩       ⇩  ⇩
B ●⇨       H_B ●├⇨{Set} →H_B (A)●─H_B (a)→○H_B (A')→
b ↓⇨       H_b ⬇│          H_b (A)↓     ◎    ↓H_b (A')
B'○⇨       H_B'○└⇨      →H_B'(A)○─H_B'(a)→○H_B'(A')→
△△△
別記号体系での図式((西郷-道案内))
▽▽▽
{Ｃ}⇨{[Ｃ^op,Set]}┌{Ｃ^op}       ←A●←───a─○A'←
    └^-h          │                 ⇩       ⇩  ⇩
B ●⇨       ^B h●├⇨{Set} →^B h(A)●─^B h(a)→○^B h(A')→
b ↓⇨       ^b h⬇│          ^b h(A)↓     ◎    ↓^b h(A')
B'○⇨       ^B'h○└⇨      →^B'h(A)○─^B'h(a)→○^B'h(A')→
△△△
別記号体系での図式(独自、実験的、文章逆順合成記号∘から類推)
※補足説明:圏論標準での「b∘-」記号はこの図式の「b∘A」相当でも使用されるので、知らずにいると理解を妨げるかもしれない。
▽▽▽
{Ｃ}⇨{[Ｃ^op,Set]}┌{Ｃ^op}    ←A●←──a─○A'←
    └()∘-         │              ⇩    ⇩  ⇩
B ●⇨       B∘- ●├⇨{Set} →B ∘A●─B ∘a→○B∘A'→
b ↓⇨       b∘- ⬇│          b ∘A↓   ◎   ↓b∘A'
B'○⇨       B'∘-○└⇨      →B'∘A○─B'∘a→○B'∘A'→
△△△
別記号体系での図式(独自、実験的、文章順合成記号を使用)
▽▽▽
{Ｃ}⇨{[Ｃ^op,Set]}┌{Ｃ^op}    ←A●←a ──○A'←
    └-;()         │              ⇩    ⇩  ⇩
B ●⇨       -;B ●├⇨{Set} →A;B ●─a;B →○A';B→
b ↓⇨       -;b ⬇│          A;b ↓   ◎   ↓A';b
B'○⇨       -;B'○└⇨      →A;B'○─a;B'→○A';B'→
△△△
文章順合成記号による独自図式で、Set内の途中演算をかっこで示す。
▽▽▽
{Ｃ}⇨{[Ｃ^op,Set]}┌{Ｃ^op}        ←A●←a ───────○A'←
    └-;()         │                  ⇩  ⇩              ⇩
B ●⇨       -;B ●├⇨{Set} →A(;x);B ●─a(;A;x);B ──→○A'(;a;A;x);B→
b ↓⇨       -;b ⬇│        A(;x;B);b ↓   ◎             ↓A'(;a;A;x;B);b
B'○⇨       -;B'○└⇨  →A(;x;B;b);B'○─a(;A;x;B;b);B'→○A'(;a;A;x;B;b);B'→
△△△

前提: Ｃは局所小圏
前提: Ｋ:Ｃ⇨Setは関手
(D,φ)はＫの表現, representation :用語
定義:⇔ D∈Ｃ かつ φ:Ｃ(D,-) ≅ Ｋ
Ｋを表現可能関手, replasentable functorと呼ぶ :用語

前提: Ｃは局所小圏
前提: Ｋ:Ｃ^op⇨Setは関手
(D,φ)はＫの表現
定義:⇔ D∈Ｃ かつ φ:Ｃ(-,D) ≅ Ｋ
Dを表現対象, representing objectと呼ぶ :用語
Ｋを表現可能反変関手, replasentable contravariant functorと呼ぶ :用語
Ｋに表現が存在するとき、Ｋは表現可能, representableと呼ぶ :用語

Ｃ(-,D)は表現可能∵Ｃ(-,D) ≅ Ｃ(-,D) :性質
Ｃ(D,-)は表現可能∵Ｃ(D,-) ≅ Ｃ(D,-) :性質

前提: Ｃは(局所)小圏
前提: D∈Ｃ
前提: Ｋ     :Ｃ^op⇨Set ∈ [Ｃ^op,Set]_0 = Set^(Ｃ^op)
事実: Ｃ(-,D):Ｃ^op⇨Set ∈ [Ｃ^op,Set]_0 = Set^(Ｃ^op) :補足説明:hom関手で示した性質
[Ｃ^op,Set](Ｃ(-,D),Ｋ) ≅ ＫD【= D;Ｋ】
が、DとＫについて自然に成り立つ :性質「米田の補題」, The Yoneda Lemma :用語
証明:
次のyとYを定義し、必要事項を順次示す。
y: [Ｃ^op,Set](Ｃ(-,D),Ｋ)⇄ＫD :Y     【】
y: [Ｃ^op,Set](Ｃ(-,D), Ｋ) ∋   α:Ｃ(-,D)➡Ｋ |→ α_D(1_D) ∈ ＫD【】
        ∵ α_D:Ｃ(D,D)→ＫD, 1_D:D→D∈Ｃ(D,D) より α_D(1_D)∈ＫD【】
Y: [Ｃ^op,Set](Ｃ(-,D), Ｋ) ∋ Y(x):Ｃ(-,D)➡Ｋ ←|        x ∈ ＫD【】
┌                f       ∈Ｃ(B,D)
│             (Ｋf)_B     :   ＫD →ＫB【】∵Ｋ:Ｃ^op⇨Set
│                     x  ∈   ＫD      【】
│Y_(B,f)(x) = (Ｋf)_B(x) ∈         ＫB【】:各B∈Ｃと各f∈Ｃ(B,D)
│Y_ B   (x) = (Ｋ-)_B(x)  :Ｃ(B,D)→ＫB【】:各B∈Ｃ
└Y      (x) = (Ｋ-)_-(x)  :Ｃ(-,D)➡Ｋ 【】:定義
Y_BはB∈Ｃについて自然を示す。
∵以下が可換
▼▼▼
Ｃ(B ,D)○-Y_B (x)→○ＫB【=B;Ｋ】
Ｃ(g ,D)↓          ↓Ｋ(g)
Ｃ(B',D)○-Y_B'(x)→○ＫB'【=B';Ｋ】
▲▲▲
∵関手性より以下が可換
▼▼▼
  f◇|→◇  Ｋf_B(x)         【=x;(f_B;Ｋ)】
   ↓￣ ↓￣(Ｋg_B;Ｋf_B')(x)【=x;Ｋg_B;Ｋf_B'= Ｋf_B'(Ｋg_B(x))】
g;f◇|→◇  Ｋ(g;f)_B'(x)    【=x;Ｋ(g;f)_B'  = Ｋ(f∘g)_B'(x)】
▲▲▲
Y;y=1を示す。
∵ x;Y;y = (x;Y)_D(1_D) = x;(Ｋ(1_D))) = x;1_(ＫD) = x
【⇔ x;Y;y = (x;Y)_D(1_D) = x;(1_D;Ｋ)) = x;1_(D;Ｋ) = x
  ⇔ Y(y(x)) = (Yx)_D(1_D) = (Ｋ(1_D)))(x) = 1_(ＫD)(x) = x】:各x∈ＫD
y;Y=1を示す。
∵ 各B∈Ｃと各f∈Ｃ(B,D)について (1_D;α_D);(Ｋf)_B = f;α_B
                            【⇔ (1_D;α_D);(f;Ｋ)_B = f;α_B
                              ⇔ (Ｋf)_B∘(α_D∘1_D) = α_B∘f】:性質「米田の逆射性」
∵αの自然性より以下が可換
▼▼▼
Ｃ(D,D)○-α_D→○ＫD【= D;Ｋ】
Ｃ(f,D)↓      ↓Ｋf【= f;Ｋ】
Ｃ(B,D)○-α_B→○ＫB【= B;Ｋ】
▲▲▲
yはDについて自然を示す。
∵
▼▼▼
[Ｃ^op,Set](Ｃ(-,A),Ｋ)○-y→○ＫA【= A;Ｋ】
            Ｃ(-,f);-  ↓    ↓Ｋf【= f;Ｋ】
[Ｃ^op,Set](Ｃ(-,B),Ｋ)○-y→○ＫB【= B;Ｋ】
▲▲▲
∵
▼▼▼
        α_A◇|→◇1_A;α_A          【=α_A∘1_A】
Ｃ(-,f);-  ＿   ＿Ｋf               【=f;Ｋ】
           ↓   ↓(1_A;α_A);Ｋf    【=(1_A;α_A);(f;Ｋ) = Ｋf∘(α_A∘1_A)】
Ｃ(-,f);α_A◇|→◇1_A;(Ｃ(-,f);α_A)【=1_A;(Ｃ(-,f);α_A) = (α_A∘Ｃ(-,f))∘1_A】
【=α_A∘Ｃ(-,f)】
▲▲▲
  1_A;(Ｃ(-,f);α_A)【=1_A;(Ｃ(-,f);α_A) = (α_A∘Ｃ(-,f))∘1_A 】
= (1_A;Ｃ(-,f));α_A【=(1_A;Ｃ(-,f));α_A = α_A∘(Ｃ(-,f))∘1_A)】
= (1_A;f);α        【                   = α∘(f∘1_A)         】
= f;α              【                   = α∘f               】
= (1_A;α_A);Ｋf    【=(1_A;α_A);(f;Ｋ)  = Ｋf∘(α_A∘1_A)     】∵「米田の逆射性」
yはＫについて自然を示す。
∵
▼▼▼
[Ｃ^op,Set](Ｃ(-,A),Ｋ )○-y→○Ｋ A【= A;Ｋ 】
                     θ;-↓    ↓θ_A
[Ｃ^op,Set](Ｃ(-,A),Ｋ')○-y→○Ｋ'A【= A;Ｋ'】
▲▲▲
∵[Ｃ^op,Set]の合成の定義より可換は可換
▼▼▼
  α◇|→◇1_A;α_A      【= α_A∘1_A】
θ;-＿   ＿ θ_A
   ↓   ↓(1_A;α_A);θ_A【= θ_A∘(α_A∘1_A)】
α;θ◇|→◇1_A;(α;θ)_A  【= (θ∘α)_A∘1_A】
【=θ∘α】
▲▲▲
YはDとＫについて自然∵「自然変換の同型」
//

前提: Ｃは局所小圏
Ｃ(-,()):Ｃ➡[Ｃ^op,Set]は充満忠実 :性質「米田埋め込みの充満忠実性」((Leinster))p123
証明:
y(Ｃ(-,f)) = Ｃ(-,f)_A(1_A) = 1_A;f = f
また y:Ｃ(A,A')≅[Ｃ^op,Set](Ｃ(-,A), Ｃ(-,A')) は全単射∵「米田の補題」でＫ=Ｃ(-,A')とする
∴ y:Ｃ(A,A')∋f|→Ｃ(-,f)∈[Ｃ^op,Set](Ｃ(-,A), Ｃ(-,A')) はAとA'について全単射 //

前提: Ｃは局所小圏
前提: A,A'∈Ｃ
Ｃ(-,A)≅Ｃ(-,A') ⇔ A≅A' ⇔ Ｃ(A,-)≅Ｃ(A',-) :性質((Leinster))p125
証明: 米田埋め込みは充満忠実なので左の同値が成り立つ。右は双対性より //

コンマ圏

前提: Ａ,Ｂ,Ｃは圏
前提: Ｐ:Ａ⇨Ｃ⇦Ｂ:Ｑ は関手
(Ｐ⇒Ｑ)【= (Ｐ→Ｑ) = (Ｐ↓Ｑ)】はコンマ圏, comma category :表記 :用語
定義:⇔ Ｃ内で以下が可換
▼▼▼
{Ａ}  Ｐ  ⇨{Ｃ}⇦ Ｑ   {Ｂ}  {(Ｐ⇒Ｑ)}
A ○  ＰA ○-h →○ＱB  ○B   (Ｐ⇒Ｑ)_0∋○(A ,h ,B ) ∈(Ａ_0, Ｃ_1, Ｂ_0) :定義:圏の対象
f ↓  Ｐf ↓ ◎  ↓Ｑg  ↓g   (Ｐ⇒Ｑ)_1∋↓(f,    g ) ∈(Ａ_1,       Ｂ_1) :定義:圏の射
A'○  ＰA'○-h'→○ＱB' ○B'  (Ｐ⇒Ｑ)_0∋○(A',h',B') ∈(Ａ_0, Ｃ_1, Ｂ_0) :定義:圏の対象
▲▲▲
▽▽▽
{Ａ}     Ｐ⇨{Ｃ}⇦    Ｑ  {Ｂ}  {(Ｐ⇒Ｑ)}
A ○  A ;Ｐ○-h →○B ;Ｑ  ○B   (Ｐ⇒Ｑ)_0∋○(A ,h ,B ) ∈(Ａ_0, Ｃ_1, Ｂ_0) :定義:圏の対象
f ↓  f ;Ｐ↓ ◎  ↓g ;Ｑ  ↓g   (Ｐ⇒Ｑ)_1∋↓(f,    g ) ∈(Ａ_1,       Ｂ_1) :定義:圏の射
A'○  A';Ｐ○-h'→○B';Ｑ  ○B'  (Ｐ⇒Ｑ)_0∋○(A',h',B') ∈(Ａ_0, Ｃ_1, Ｂ_0) :定義:圏の対象
△△△

以降、特殊なコンマ圏を扱う箇所では、以下のように補足説明する。
上記のコンマ圏の汎用の図式をコピペし、実際にキーボードを操作し代入してみると理解が進むと思う。:表記、独自

補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)

▼▼▼
{Ｃ}
P0┌⇦○(Ｐ⇒Ｑ)⇨┐P1
Ａ○      ◎      ○Ｂ
Ｐ└⇨○Ｃ⇦───┘Ｑ
▲▲▲
ただし
P0 : (A, h:ＰA→ＱB, B) |→ A
【P0 : (A, h:A;Ｐ→B;Ｑ, B) |→ A】
P1 : (A, h:ＰA→ＱB, B) |→ B
【P1 : (A, h:A;Ｐ→B;Ｑ, B) |→ B】
のとき、以下のσは自然変換 :性質
▼▼▼
{Ｃ}
     ┌○(Ｐ⇒Ｑ)┐
P0;Ｐ⇩  ◎  σ➡ ⇩P1;Ｑ
     └○Ｃ───┘
▲▲▲
▽▽▽
     ┌○(Ｐ⇒Ｑ)┐
Ｐ∘P0⇩  ◎  σ➡ ⇩Ｑ∘P1
     └○Ｃ───┘
△△△

*【= 1】定義:= 1つの対象と恒等射のみの圏 :表記
! 定義:= 一意に決まる射、*からの射の場合は一意に決まる :表記
補足説明:「1」の記号は恒等射・圏の射集合・終対象で使用し使用し過ぎなので、本資料ではこの意味では「*」を使用し「1」を使用しない。

前提: Ａは圏
前提: B∈Ａ
ＡのB上のスライス圏, slice category :用語
⇔ Ａ/B :表記
定義:⇔ コンマ圏(1_Ａ⇒B)
⇔以下が可換 :性質
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>f>A'|Ａ>1>Ａ<!<*|B<1<B)
▼▼▼
{Ａ}          {Ａ/B} = {(1_Ａ⇒B)}
A ○-h →┐   Ａ/B_0∋○(A ,h )
f ↓ ◎  ○B  Ａ/B_1∋↓f 
A'○-h'→┘   Ａ/B_0∋○(A',h')
▲▲▲

前提: Ｂは圏
前提: A∈Ｂ
ＢのA上の余スライス圏, coslice category :用語
⇔ A/Ｂ :表記
定義:⇔ コンマ圏(A⇒1_Ｂ)
⇔以下が可換 :性質
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>1>A|*>!>Ｂ<1<Ｂ|B'<g<B)
▼▼▼
{Ｂ}         {A/Ｂ} = {(A⇒1_Ｂ)}
 ┌h →○B   A/Ｂ_0∋○(h ,B )
A○ ◎ ↓g   A/Ｂ_1∋↓g
 └h'→○B'  A/Ｂ_0∋○(h',B')
▲▲▲

CからＦへの普遍射, universal arrow :用語
定義:⇔ コンマ圏(C⇒Ｆ)の始対象
⇔以下が可換 :性質
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(C>1>C|*>!>Ｃ<Ｆ<Ｄ|D'<f<D)
▼▼▼
{Ｃ}   ⇦Ｆ   {Ｄ}  {(C⇒Ｆ)}
 ┌u →●ＦD  ●D   (C⇒Ｆ)_0∋●(D ,u ) = 0(始対象) ⇔ CからＦへの普遍射
C○ ◎ ↓Ｆf  ↓f   (C⇒Ｆ)_1∋↓∃!f   :fは唯一∵始対象から対象への射は一意
 └u'→○ＦD' ○D'  (C⇒Ｆ)_0∋○∀(D',u') ⇔ CからＦへの射のひとつ
▲▲▲
▽▽▽
{Ｃ}      ⇦Ｆ  {Ｄ}  {(C⇒Ｆ)}
 ┌u →●D ;Ｆ  ●D   (C⇒Ｆ)_0∋●  (D ,u ) = 0(始対象) ⇔ CからＦへの普遍射
C○ ◎ ↓f ;Ｆ  ↓f   (C⇒Ｆ)_1∋↓∃!f   :fは唯一∵始対象から対象への射は一意
 └u'→○D';Ｆ  ○D'  (C⇒Ｆ)_0∋○∀(D',u') CからＦへの射のひとつ
△△△

ＦからCへの普遍射, universal arrow :用語
定義:⇔ コンマ圏(Ｆ⇒C)の終対象
⇔以下が可換 :性質(上の命題の双対命題)
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(D'>f>D|Ｄ>Ｆ>Ｃ<!<*|C<1<C)
▼▼▼
{Ｄ}  Ｆ⇨{Ｃ}        {(Ｆ⇒C)}
D’○  ＦD'○-u'→┐   (Ｆ⇒C)_0∋○∀(D',u') ⇔ ＦからCへの射のひとつ
f ↓  Ｆf ↓ ◎  ○C  (Ｆ⇒C)_1∋↓∃!f   :fは唯一∵対象から終対象への射は一意
D ●  ＦD ●-u →┘   (Ｆ⇒C)_0∋●  (D ,u ) = 1(終対象) ⇔ ＦからCへの普遍射
▲▲▲
▽▽▽
{Ｄ}    Ｆ⇨{Ｃ}       {(Ｆ⇒C)}
D’○  D';Ｆ○-u'→┐   (Ｆ⇒C)_0∋○∀(D',u') ⇔ ＦからCへの射のひとつ
f ↓  f ;Ｆ↓ ◎  ○C  (Ｆ⇒C)_1∋↓∃!f   :fは唯一∵対象から終対象への射は一意
D ●  D ;Ｆ●-u →┘   (Ｆ⇒C)_0∋●  (D ,u ) = 1(終対象) ⇔ ＦからCへの普遍射
△△△

極限・余極限

前提: Ｃは圏
前提: Ｉは小圏
ＤはＩ型図式, diagram of shape【/type/index】Ｉ :用語
定義:⇔ Ｄ:Ｉ⇨Ｃ は関手、すなわち Ｄ:Ｉ⇨Ｃ ∈[Ｉ,Ｃ]【= Ｃ^Ｉ】
Ｉを固定し、Ｄ(Ｉ)⊂Ｃを改めてＤ⊂Ｃとすると次を満たすので、部分圏, subcategoryとも呼ぶ :用語と性質
i,j,k∈Ｉ_0, u:i→j,v:j→k∈Ｉ_1とすると
Di【=Ｄ(i)】∈Ｄ_0 :表記、独自
Dj, Dk ∈Ｄ_0
u【=Ｄ(u)】:Di→Dj∈Ｄ_1 :記号の再定義、独自
v          :Dj→Dk∈Ｄ_1
1_Di:Di→Di∈Ｄ_1
u;v【= v∘u】= Ｄ(u);Ｄ(v)【= Ｄ(v)∘Ｄ(u)】= Ｄ(u;v)【= Ｄ(v∘u)】∈Ｄ_1
Ｉ型図式のＩを、インデックス圏, 添字圏, index categoryと呼ぶ :用語
補足説明:添字集合, index setの一般化
▼▼▼
{Ｉ} →∀i○─∀u→○∀j→ ∈Ｉ型
⇩Ｄ      ⇩   ⇩  ⇩        Ｄ:Ｉ⇨Ｃ ∈[Ｉ,Ｃ]_0【= Ｃ^Ｉ】はＩ型図式
{Ｃ}  →Di○──u→○Dj→  ∈部分圏Ｄ
▲▲▲

対角関手, diagonal functor :用語
前提: Ｃは圏
前提: Ｉは小圏
Δ:Ｃ⇨[Ｉ,Ｃ] つまり関手を以下のように定める(自然性公理・関手の準同型などが成り立つように定める) :定義
各A∈Ｃ_0           について、ΔA       ∈[Ｉ,Ｃ]_0 :定関手, constant functor【, 定数関手】:用語と性質
各A∈Ｃ_0と各i∈Ｉ_0について、ΔA(i)=  A∈Ｃ_0
各A∈Ｃ_0と各u∈Ｉ_1について、ΔA(u)=1_A∈Ｃ_1
各f∈Ｃ_1           について、Δf       ∈[Ｉ,Ｃ](ΔA,ΔB)⊂[Ｉ,Ｃ]_1 つまり自然変換
各f∈Ｃ_1と各i∈Ｉ_0について、Δf(i)=  f∈Ｃ_1 :自然変換Δfのi成分
▼▼▼
{Ｃ}⇨{[Ｉ,Ｃ]}┌  {Ｉ} → ∀i    ●──∀u──→○   ∀j →
    └Δ        │                ⇩     ⇩       ⇩
A● ⇨     ΔA○├⇨{Ｃ} →ΔA(i)=A●─ΔA(u)=1_A→○A=ΔA(j)→
f↓ ⇨     Δf⬇│         Δf(i)=f↓      ◎      ↓f=Δf(j)
B○ ⇨     ΔB○└⇨     →ΔB(i)=B○─ΔB(u)=1_B→○B=ΔB(j)→
▲▲▲

Ｉが２つの対象からなる離散圏の場合、①の等式が成り立つと圏論のいくつかの本に記載されている。
②の等式が成り立つと筆者は誤解してしまったので、念の為注意喚起。
▼▼▼
(A,A)∈Ｃ×Ｃ
 ||    ||①
ΔA   ∈[Ｉ,Ｃ]
¬||   ¬||②
A×A ∈Ｃ
補足説明:A×Aは極限の一つで、コンマ圏(Δ⇒Ｉ)(Ｉは離散圏)の終対象として、Δも使用して改めて定義されるもの。
補足説明:①の等式この後明示的には使用しないため、忘れて構わない。
▲▲▲

前提: Ｃは圏
前提: Ｄ:Ｉ⇨ＣはＩ型図式
一時的定義: Ｄ~:*⇨[Ｉ,Ｃ]
事実:        Δ:Ｃ⇨[Ｉ,Ｃ]
(X,f)はＩ型図式Ｄの極限, limit 【, 逆極限, inverse limit, 射影的極限, projective limit, 普遍錐, universal cone, 極限錐, limiting cone】:用語
⇔ (X,f) = (limＤ,f) = limＤ【=lim_←Ｄ】:表記
定義:⇔ コンマ圏(Δ⇒Ｄ~)の終対象
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(Y>h>X|Ｃ>Δ>[Ｉ,Ｃ]<Ｄ~<*|*<1<*)
▼▼▼
{Ｃ}  Δ⇨{[Ｉ,Ｃ]}⇦Ｄ~   {*}  {(Δ⇒Ｄ~)}
Y ○  ΔY=Y○─g➡┐              (Δ⇒Ｄ~)_0∋○∀(Y,g) = Cone(Y,Ｄ)
h ↓  Δh=h⬇ ◎  ○Ｄ=Ｄ~*  ○*  (Δ⇒Ｄ~)_1∋↓∃!h   :hは唯一∵対象から終対象への射は一意:普遍性の条件
X ●  ΔX=X●─f➡┘              (Δ⇒Ｄ~)_0∋●  (X,f) = (limＤ,f) = limＤ = Cone(X,Ｄ) = 1(終対象)
▲▲▲
Cone(Y,Ｄ) = (Y,g) = (Y,{gi:Y→Ｄ(Ｉ)|i∈Ｉ}) ∈(Δ⇒Ｄ~)_0を、Yを頂点, vertexとするＤの錐, coneと呼ぶ。:用語
自然変換 g:ΔY➡Ｄ を詳しく表示する。
▼▼▼
{Ｉ}→∀i○─∀u→○∀j→   ∈Ｉ型
⇩Ｄ     ⇩   ⇩  ⇩       Ｄ∈[Ｉ,Ｃ]_0 つまり関手
{Ｃ} →Di○──u→○Dj→     ∈部分圏Ｄ
       gi↑   ◎   ↑gj      g∈[Ｉ,Ｃ](ΔY,Ｄ)⊂[Ｉ,Ｃ]_1 つまり自然変換 ∴Cone(Y,Ｄ)の内部は可換
      →Y○─1_Y→○Y→
⇧ΔY     ⇧   ⇧  ⇧       ΔY∈[Ｉ,Ｃ]_0 つまり関手
{Ｉ}→∀i○─∀u→○∀j→   ∈Ｉ型
▲▲▲
上の2つの図式を組み合わせて整理する。
▼▼▼
{Ｉ}→∀i○─∀u→○∀j→ ∈Ｉ型
⇩Ｄ     ⇩   ⇩  ⇩      Ｉ型図式
{Ｃ} →Di○──u→○Dj→  ∈部分圏Ｄ
   └  fi└←●X→┘fj  ┘(X,f) = (limＤ,f) = limＤ = Cone(X,Ｄ) すなわち fj = fi;u【⇔ fj = u∘fi】:錐の可換条件
             ↑∃!h        ∃!h, gi = h;fi, gj = h;fj【⇔ gi = fi∘h, gj = fj∘h】:普遍性とその可換条件、hは仲介射, mediating morphism :用語
   └  gi└←○Y→┘gj  ┘∀(Y,g) = Cone(Y,Ｄ) すなわち gj = gi;u【⇔ gj = u∘gi】:錐の可換条件
▲▲▲
補足説明:行内に、近い概念のオブジェクトが集中するように図式の配置を考慮している。
(X,f)のfiを極限の射影, 標準射影, 射影射, canonical projection, projection morphism と呼ぶ。:用語

   Ｃ(Y,limＤ) :補足説明:limＤへの射
≅ Cone(Y,Ｄ) ∵limＤの普遍性より
=  [Ｉ,Ｃ](ΔY,Ｄ) ∵定義
▼▼▼
┌ΔY⇨┐
Ｉ ⬇ Ｃ
└Ｄ⇨┘
▲▲▲
∴Δ⊣lim :性質、随伴は後出、自然性の証明は後日記載予定

前提: Ｃは局所小圏
前提: Ｄ:Ｉ⇨Ｃは図式
前提: X∈Ｃ
limＣ(c,Ｄ-) ≅ Set(c,limＤ) :性質「lim-hom交換」((MacLane))p154
証明:
Ｃ(c,Ｄ-):Ｉ⇨Set
λ:c→Ｄは錐 ⇔ λ:*⇨Ｃ(c,Ｄ-)は錐 ∵集合なので、全ての極限が存在する
∴ Cone(X,-) ≅ Set(X,Cone(*,-))
∴ Set(X,    limＣ(c,Ｄ-))
≅ Cone(X,      Ｃ(c,Ｄ-))  ∵Set(X,limＦ) ≅ Cone(X,Ｆ)
≅ Set(X,Cone(*,Ｃ(c,Ｄ-))) ∵Cone(X,Ｆ) ≅ Set(X,Cone(*,Ｆ)) (前で示したこと)
=  Set(X,     Cone(c,Ｄ))   ∵Cone(*,Ｃ(c,Ｄ-)) = Cone(c,Ｄ) (図式を辿って)
≅ Set(X,    Ｃ(c,limＤ))   ∵Cone(X,Ｆ) ≅ Ｃ(X,limＦ) //

前提: Ｃは圏
前提: Ｄ:Ｉ⇨Ｃは図式
一時的定義: Ｄ~:*⇨[Ｉ,Ｃ]
事実:        Δ:Ｃ⇨[Ｉ,Ｃ]
(X,f)はＤの余極限, colimit【, 順極限, direct limit, 帰納的極限, inductive limit】:用語(極限の命題の双対命題)
⇔ (X,f) = (colimＤ,f) = colimＤ【=lim_→Ｄ】:表記
定義:⇔ コンマ圏(Ｄ~⇒Δ)の始対象
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(*>1>*|*>Ｄ~>[Ｉ,Ｃ]<Δ<Ｃ|Y<h<X)
▼▼▼
{*}  Ｄ~⇨{[Ｉ,Ｃ]}⇦Δ  {Ｃ}  {(Ｄ~⇒Δ)}
           ┌─f➡●X=ΔX  ●X   (Ｄ~⇒Δ)_0∋●  (X,f) = (colimＤ,f) = colimＤ = Cocone(Ｄ,X) = 0(始対象)
*○ Ｄ~*=Ｄ○  ◎ ⬇h=Δh  ↓h   (Ｄ~⇒Δ)_1∋↓∃!h   :hは唯一∵始対象から対象への射は一意:普遍性の条件
           └─g➡○Y=ΔY  ○Y   (Ｄ~⇒Δ)_0∋○∀(Y,g) = Cocone(Ｄ,Y)
▲▲▲
Cocone(Ｄ,Y) = (Y,g) = (Y,{gi:Ｄ(Ｉ)→Y|i∈Ｉ}) ∈(Ｄ~⇒Δ)_0を、Yを頂点, vertexとするＤの余錐, coconeと呼ぶ。:用語
自然変換 g:Ｄ➡ΔY を詳しく表示する。
▼▼▼
{Ｉ}→∀i○─∀u→○∀j→   ∈Ｉ型
⇩Ｄ     ⇩   ⇩  ⇩      Ｄ∈[Ｉ,Ｃ]_0 つまり関手
{Ｃ} →Di○──u→○Dj→    ∈部分圏Ｄ
       gi↓   ◎   ↓gj     g∈[Ｉ,Ｃ](Ｄ,ΔY)⊂[Ｉ,Ｃ]_1 つまり自然変換 ∴Cocone(Ｄ,Y)の内部は可換
      →Y○─1_Y→○Y→
⇧ΔY     ⇧   ⇧  ⇧      ΔY∈[Ｉ,Ｃ]_0 つまり関手
{Ｉ}→∀i○─∀u→○∀j→   ∈Ｉ型
▲▲▲
上の2つの図式を組み合わせて整理する。
▼▼▼
{Ｉ}→∀i○─∀u→○∀j→ ∈Ｉ型
⇩Ｄ     ⇩   ⇩  ⇩      Ｉ型図式
{Ｃ} →Di○──u→○Dj→  ∈部分圏Ｄ
   └  fi└→●X←┘fj  ┘(X,f) = (colimＤ,f) = colimＤ = Cocone(Ｄ,X) ⇔ fi = u;fj【⇔ fi = u∘fj】:余錐の可換条件
             ↓∃!h        gi = fi;h, gj = fj;h【⇔ gi = h∘fi, gj = h∘fj】:普遍性とその可換条件、hは仲介射, mediating morphism :用語
   └  gi└→○Y←┘gj  ┘∀(Y,g) = Cocone(Ｄ,Y) ⇔ gi = u;gj【⇔ gi = u∘gj】:余錐の可換条件
▲▲▲
(X,f)のfiを余極限の余射影, 標準入射, coprojection, canonical injection と呼ぶ :用語

   Ｃ(colimＤ,Y) :補足説明:colimＤからの射
≅ Cocone(Ｄ,Y) ∵colimＤの普遍性より
=  [Ｉ,Ｃ](Ｄ,ΔY) ∵定義
▼▼▼
┌Ｄ⇨┐
Ｉ ⬇ Ｃ
└ΔY⇨┘
▲▲▲
∴colim⊣Δ :性質、随伴は後出、自然性の証明は後日記載予定

前提: Ｃは局所小圏
前提: Ｄ:Ｉ⇨Ｃは図式
前提: X∈Ｃ
limＣ(Ｄ-,X) ≅ Ｃ(colimＤ,X) :性質「colim-hom交換」
証明:
   Ｃ(colimＤ,X)
=  Ｃ^op(X,limＤ)
≅ limＣ^op(X,Ｄ-) ∵「lim-hom交換」
= limＣ(Ｄ-,X) //

1は圏Ｃの終対象, terminal object :用語:極限を用いて再定義する場合、「1」の記号は恒等射・圏の射集合・終対象で使用し文脈で意味を区別させる。
定義:⇔ Ｉ型=0=(φ,φ)(空(対象0個、射0個))としたlimＤ
⇔ 1∈Ｃ_0 かつ ∀Y∈Ｃ_0, ∃!h∈Ｃ(Y,1)
⇔ 1∈Ｃ_0 かつ ∀Y∈Ｃ_0, Ｃ(Y,1)が1元集合
⇔ 1∈Ｃ_0 かつ ∀Y∈Ｃ_0, |Ｃ(Y,1)|=1
▼▼▼
{Ｉ}   ∈Ｉ型(空(対象0個、射0個))
⇩Ｄ   Ｉ型図式
{Ｃ}   ∈部分圏Ｄ
●1    1 =limＤ=Cone(1,Ｄ)
↑∃!h :普遍性。可換条件なし∵Ｄの対象と射がない
○Y    ∀Y=Cone(Y,Ｄ)
▲▲▲

0は圏Ｃの始対象, initial object :用語:余極限を用いて再定義する場合(極限の命題の双対命題)
定義:⇔ Ｉ型=0=(φ,φ)(空(対象0個、射0個))としたcolimＤ
⇔ 0∈Ｃ_0 かつ ∀Y∈Ｃ_0, ∃!h∈Ｃ(0,Y)
⇔ 0∈Ｃ_0 かつ ∀Y∈Ｃ_0, Ｃ(0,Y)が1元集合
⇔ 0∈Ｃ_0 かつ ∀Y∈Ｃ_0, |Ｃ(0,Y)|=1
▼▼▼
{Ｉ}   ∈Ｉ型(空(対象0個、射0個))
⇩Ｄ   Ｉ型図式
{Ｃ}   ∈部分圏Ｄ
●0    0 =colimＤ=Cocone(Ｄ,0)
↓∃!h :普遍性。可換条件なし∵Ｄの対象と射がない
○Y    ∀Y=Cocone(Ｄ,Y)
▲▲▲

(X,p)=(D1×D2,p)はD1とD2の積, product :表記 :用語
定義:⇔ Ｉ型を、2つの対象を持つ離散圏としたlimＤ
定義:⇔ (X,p)=Cone(X,Ｄ)
 かつ ∀(Y,q)=Cone(Y,Ｄ),
 ∃!h:Y→X, q1 = h;p1, q2 = h;p2【⇔ q1 = p1∘h, q2 = p2∘h】
▼▼▼
{Ｉ}   ○       ○    ∈Ｉ型
⇩Ｄ   ⇩       ⇩    Ｉ型図式
{Ｃ} D1○       ○D2  ∈部分圏Ｄ(離散圏なのでDi間の射は無い)
     p1└←●X→┘p2  (X,p)= D1×D2 =limＤ=Cone(X,Ｄ) :錐の可換条件なし
           ↑∃!h     q1 = h;p1, q2 = h;p2【⇔ q1 = p1∘h, q2 = p2∘h】:普遍性とその可換条件
     q1└←○Y→┘q2  ∀(Y,q)=Cone(Y,Ｄ) :錐の可換条件なし
▲▲▲

(X,p)=(D1+D2,p)はD1とD2の余積, 双対積, coproduct, dual-product :表記 :用語(極限の命題の双対命題)
定義:⇔ Ｉ型を、2つの対象を持つ離散圏としたcolimＤ
定義:⇔ (X,p)=Cocone(Ｄ,X)
 かつ ∀(Y,q)=Cocone(Ｄ,Y),
 ∃!h:X→Y, q1 = p1;h, q2 = p2;h【⇔ q1 = h∘p1, q2 = h∘p2】
▼▼▼
{Ｉ}   ○       ○    ∈Ｉ型
⇩Ｄ   ⇩       ⇩    Ｉ型図式
{Ｃ} D1○       ○D2  ∈部分圏Ｄ(離散圏なのでDi間の射は無い)
     p1└→●X←┘p1   (X,p)= D1+D2 =colimＤ=Cocone(Ｄ,X) :余錐の可換条件なし
           ↓∃!h      q1 = p1;h, q2 = p2;h【⇔ q1 = h∘p1, q2 = h∘p2】:普遍性とその可換条件
     q1└→○Y←┘q2   ∀(Y,q)=Cocone(Ｄ,Y) :余錐の可換条件なし
▲▲▲

余積を持つ圏において、二つの射影的対象の余積は射影的 :性質
証明:
仮定: e:Y→Z epi f:X→Z
  pi;f【= f∘pi】
= qi;e【= e∘qi】∵D_iは射影的
= pi;h;e【= e∘h∘pi】∵Xは余積
∴f = h;e【= e∘h】∵k = pi;x【= x∘pi】を満たすxは余積の普遍性の性質より一意(同じもの)でないといけない
∴Xは射影的 //
▼▼▼
{Ｉ}   ○       ○    ∈Ｉ型
⇩Ｄ   ⇩       ⇩    Ｉ型図式
{Ｃ} D1○       ○D2  ∈部分圏Ｄ(Di間の射は無い)
     p1└→●X←┘p2    ┐↓f
           ↓∃!h       ○
     q1└→○Y←┘q2    ┘↑e:epi
▲▲▲

q1 または q2 はモノ ⇒ 積のh = <q1,q2>はモノ :性質
▼▼▼
{Ｉ}   ○       ○    ∈Ｉ型
⇩Ｄ   ⇩       ⇩    Ｉ型図式
{Ｃ} D1○       ○D2  ∈部分圏Ｄ(Di間の射は無い)
     p1└←●X→┘p2  (X,p)=limＤ=Cone(X,Ｄ)
           ↑∃!h
     q1└←○Y→┘q2  ∀(Y,q)=Cone(Y,Ｄ)
▲▲▲
証明:
仮定: x;h = y;h【⇔ h∘x = h∘y】
∴x;q1【= q1∘x】
= x;h;p1【= p1∘h∘x】∵h;p1【= p1∘h】= q1
= y;h;p1【= p1∘h∘y】∵仮定
= y;q1【= q1∘y】∵h;p1【= p1∘h】= q1
∴x = y ∵q1はモノ //

q1 または q2 はエピ ⇒ 余積のhはエピ :性質(極限の命題の双対命題)
▼▼▼
{Ｉ}   ○       ○    ∈Ｉ型○
⇩Ｄ   ⇩       ⇩    Ｉ型図式
{Ｃ} D1○       ○D2  ∈部分圏Ｄ(Di間の射は無い)
     p1└→●X←┘p2  (X,p)=colimＤ=Cocone(Ｄ,X)
           ↓∃!h
     q1└→○Y←┘q2  ∀(Y,q)=Cocone(Ｄ,Y)
▲▲▲
証明:
仮定: h;x = h;y【x∘h = y∘h】
∴q1;x【= x∘q1】
= p1;h;x【= x∘h∘p1】∵p1;h【= h∘p1】= q1
= p1;h;y【= y∘h∘p1】∵仮定
= q1;y【= y∘q1】∵p1;h【= h∘p1】= q1
∴x = y ∵q1はエピ //

(E,e)はf,gの等化子, equalizer :用語
定義:⇔ Ｉ型を以下としたlimＤ
定義:⇔ (E,e)=Cone(E,Ｄ) すなわち e;f = e;g【⇔ f∘e = g∘e】
 かつ ∀(Y,q)=Cone(Y,Ｄ) すなわち q;f = q;g【⇔ f∘q = g∘q】,
                          ∃!h:Y→E, q = h;e【⇔ q = e∘h】
▼▼▼
{Ｉ} ○=====⇉○    ∈Ｉ型
⇩Ｄ ⇩ ⇩⇩ ⇩    Ｉ型図式
{Ｃ}    f g
   D1○=====⇉○D2  ∈部分圏Ｄ
    e└←●E        (E,e)=limＤ=Cone(E,Ｄ) ⇔ e;f = e;g【⇔ f∘e = g∘e】:錐の可換条件 :可換性よりfjは冗長なので省略可能
         ↑∃!h     q=h;e :普遍性とその可換条件
    q└←○Y        ∀(Y,q)=Cone(Y,Ｄ) ⇔ q;f = q;g【⇔ f∘q = g∘q】:錐の可換条件 :可換性よりgjは冗長なので省略可能
▲▲▲
equalizerは多様体すなわち方程式による部分集合の一般化

(E,e)はf,gの等化子 ⇒ eはモノ :性質
証明:
仮定:       h;e   = k;e  【  e∘h =   e∘k】
前提:         e;f =   e;g【f∘e   = g∘e  】∵eは等化子
∴          h;e;f = h;e;g【f∘e∘h = g∘e∘h】∵前提
∴∃!f:Y→E,h;e   = f;e  【  e∘h =  e∘f】∵eは等化子
∴          k;e;f = k;e;g【f∘e∘k = g∘e∘k】∵前提
∴∃!g:Y→E,h;e   = g;e  【  e∘h =   e∘g】∵eは等化子
f = g = h = k は等化子の普遍性の性質より一意(同じもの)でないといけない //

(E,e)はf,gの余等化子, coequalizer :用語(極限の命題の双対命題)
定義:⇔ Ｉ型を以下としたcolimＤ
定義:⇔ (E,e)=Cocone(Ｄ,E) すなわち f;e = g;e【⇔ e∘f = e∘g】
 かつ ∀(Y,q)=Cocone(Ｄ,Y) すなわち f;q = g;q【⇔ q∘f = q∘g】,
                            ∃!h:E→Y, q = e;h【⇔ q = h∘e】
▼▼▼
{Ｉ} ○=====⇉○    ∈Ｉ型
⇩Ｄ ⇩ ⇩⇩ ⇩    Ｉ型図式
{Ｃ}    f g
   D1○=====⇉○D2  ∈部分圏Ｄ
         ●E←┘e   (E,e)=colimＤ=Cocone(Ｄ,E) ⇔ f;e = g;e【⇔ e∘f = e∘g】:余錐の可換条件 :可換性よりgiは冗長なので省略可能
         ↓∃!h     q = e;h【⇔ q = h∘e】:普遍性とその可換条件
         ○Y←┘q   ∀(Y,q)=Cocone(Ｄ,Y) ⇔ f;q = g;q【⇔ q∘f = q∘g】:余錐の可換条件 :可換性よりgiは冗長なので省略可能
▲▲▲
coequalizerは同値関係による商の一般化

(E,e)はf,gの余等化子 ⇒ eはエピ :性質(極限の命題の双対命題)
証明:
仮定:         e;h =   e;k【h∘e   = k∘e  】
前提:       f;e   = g;e  【  e∘f =   e∘g】∵eは余等化子
∴          f;e;h = g;e;h【h∘e∘f = h∘e∘g】∵前提
∴∃!f:Y→E,  e;h = e;f  【h∘e   = f∘e  】∵eは余等化子
∴          f;e;k = g;e;k【k∘e∘f = k∘e∘g】∵前提
∴∃!g:Y→E,  e;k =   e;g【k∘e   = f∘e    】∵eは余等化子
f = g = h = k は余等化子の普遍性の性質より性質より一意(同じもの)でないといけない //

(X,l) = (D1×_C D2,l)は引き戻し, p.b.【, ファイバー積, pullback, fiber product】:表記 :用語
定義:⇔ Ｉ型を以下としたlimＤ
定義:⇔ (X,l)=Cone(X,Ｄ) すなわち l1;d1 = l2;d2【⇔ d1∘l1 = d2∘l2】
 かつ ∀(Y,q)=Cone(Y,Ｄ) すなわち q1;d1 = q2;d2【⇔ d1∘q1 = d2∘q2】,
                   ∃!h:Y→X, q1 = h;l1, q2 = h;l2【⇔ q1 = l1∘h, q2 = l2∘h】
▼▼▼
{Ｉ} ○→○ ←○    ∈Ｉ型
⇩Ｄ ⇩⇩⇩ ⇩⇩    Ｉ型図式
{Ｃ}   d1   d2
   D1○→○C←○D2  ∈部分圏Ｄ
   l1└←●X→┘l2  (X,l)= D1×_C D2 =limＤ=Cone(X,Ｄ) ⇔ l1;d1 = l2;d2【⇔ d1∘l1 = d2∘l2】:錐の可換条件
         ↑∃!h     q1 = h;l1, q2 = h;l2【⇔ q1 = l1∘h, q2 = l2∘h】:普遍性とその可換条件
   q1└←○Y→┘q2  ∀(Y,q)=Cone(Y,Ｄ) ⇔ q1;d1 = q2;d2【⇔ d1∘q1 = d2∘q2】:錐の可換条件 :Cへの射は可換性より冗長のため省略可
▲▲▲
共通部分、逆像の一般化。

(X,l)=(D1+_C D2,l)は押し出し, p.o.【, pushout】:表記 :用語(極限の命題の双対命題)
定義:⇔ Ｉ型を以下としたcolimＤ
定義:⇔ (X,l)=Cocone(Ｄ,X) すなわち d1;l1 = d2;l2【⇔ l1∘d1 = l2∘d2】
 かつ ∀(Y,q)=Cocone(Ｄ,Y) すなわち d1;q1 = d2;q2【⇔ q1∘d1 = q2∘d2】,
                     ∃!h:Y→X, q1 = h∘l1, q2 = h∘l2【⇔ q1 = h∘l1, q2 = h∘l2】
▼▼▼
{Ｉ} ○←○ →○    ∈Ｉ型
⇩Ｄ ⇩⇩⇩ ⇩⇩    Ｉ型図式
{Ｃ}   d1   d2
   D1○←○C→○D2  ∈部分圏Ｄ
   l1└→●X←┘l2  (X,l)= D1+_C D2 =colimＤ=Cocone(Ｄ,X) ⇔ d1;l1 = d2;l2【⇔ l1∘d1 = l2∘d2】:余錐の可換条件
         ↓∃!h     q1 = h∘l1, q2 = h∘l2【⇔ q1 = h∘l1, q2 = h∘l2】:普遍性とその可換条件
   q1└→○Y←┘q2  ∀(Y,q)=Cocone(Ｄ,Y) ⇔ d1;q1 = d2;q2【⇔ q1∘d1 = q2∘d2】:余錐の可換条件 :Cへの射は可換性より冗長のため省略可
▲▲▲

(D,f,g)は引き戻し かつ fはモノ ⇒ f'はモノ :性質
▼▼▼
{Ｃ}f<m>  g
 A○→○C←○B     ∈部分圏Ｄ
g'└←●D→┘f'<m> Ｄの引き戻し
▲▲▲
証明:
▼▼▼
{Ｃ}f<m> g
 A○→○C←○B      ∈部分圏Ｄ
g'└←●D→┘f'<m?> (D,f',g')=colimＤ(Ｄの余錐のひとつ)
      _⇈h k
l2└←○E→┘l1     ∀(E,l)Ｄの錐
▲▲▲
仮定:l1= h;f' = k;f'【f'∘h = f'∘k】
∴(h;g');f【= f∘(g' ∘h)】
= h;(g';f)【= (f∘ g')∘h】
= h;(f';g)【= (g∘ f')∘h】∵引き戻し
= (h;f');g【= g∘(f' ∘h)】
= (k;f');g【= g∘(f' ∘k)】∵仮定
= k;(f';g)【= (g∘ f')∘k】
= k;(g';f)【= (f∘ g')∘k】∵引き戻し
= (k;g');f【= f∘(g' ∘k)】
∴h;g' = k;g'【g'∘h = g'∘k】∵fはモノ
仮定: l2 = h;g' = k;g'【= g'∘h = g'∘k】
∴l2;f【= f∘ l2】
= (h;g');f【= f∘(g' ∘h)】∵仮定
= h;(g';f)【= (f∘ g')∘h】
= h;(f';g)【= (g∘ f')∘h】∵引き戻し
= (h;f');g【= g∘(f' ∘h)】
= l2;g【= g∘ l1】∵仮定
∴∃!l3:E→D, l3;f' = l1 = h;f' = k;f'【f'∘l3 = l1 = f'∘h = f'∘k】
         かつ l3;g' = l2 = h;g' = k;g'【g'∘l3 = l2 = g'∘h = g'∘k】∵引き戻し
l3 = h = k は引き戻しの普遍性の性質より一意(同じもの)でないといけない //

(D,f,g)は押し出し かつ fはエピ ⇒ f'はエピ :性質(極限の命題の双対命題)
▼▼▼
{Ｃ}f<e>  g
 A○←○C→○B     ∈部分圏Ｄ
g'└→●D←┘f'<e> Ｄの押し出し
▲▲▲
証明:
▼▼▼
{Ｃ}f<e>  g
 A○←○C→○B     ∈ 部分圏Ｄ
g'└→●D←┘f'<e?> Ｄの押し出し
     _⇊∃!h
l1└→○E←┘l2     ∀Ｄの余錐
▲▲▲
仮定: l1 = f';h = f';k【h∘f' = k∘f'】
∴f;(g';h)【= (h∘ g')∘f】
= (f;g');h【= h∘(g' ∘f)】
= (g;f');h【= h∘(f' ∘g)】∵押し出し
= g;(f';h)【= (h∘ f')∘g】
= g;(f';k)【= (k∘ f')∘g】∵仮定
= (g;f');k【= k∘(f' ∘g)】
= (f;g');k【= k∘(g' ∘f)】∵押し出し
= f;(g';k)【= (k∘ g')∘f】
∴g';h = g';k【h∘g'=k∘g'】∵fはエピ
仮定: l2 = g';h = g';k【= h∘g' = k∘g'】
∴f;l2【= l2∘f】
= f;(g';h)【= (h∘ g')∘f】∵仮定
= (f;g');h【= h∘(g' ∘f)】
= (g;f');h【= h∘(f' ∘g)】∵押し出し
= g;(f';h)【= (h∘ f')∘g】
= g;l1【= l1∘g】∵仮定
∴∃!l3:D→E, f';l3 = l1 = f';h = f';k【l3∘f' = l1 = h∘f' = k∘f'】
         かつ g';l3 = l2 = g';h = g';k【l3∘g' = l2 = h∘g' = k∘g'】∵p.o.
l3 = h = k は押し出しの普遍性の性質より一意(同じもの)でないといけない //

(1)右の四角形がp.b.,外枠の四角形がp.b. ⇒ 左の四角形がp.b.
(2)左右の四角形がp.b. ⇒ 外枠の四角形がp.b. :性質
▼▼▼
○→○→○
↓  ↓  ↓
○→○→○
▲▲▲
証明:
(1)
∃!l1, 次が可換 ∵右の四角形がp.b.
▼▼▼
{Ｃ}
○─────┐
│   ↘l1   ↓
│  ○→○→○
│  ↓  ↓  ↓
└→○→○→○
▲▲▲
∃!l2, 次が可換 ∵外枠の四角形がp.b.
▼▼▼
{Ｃ}
○─────┐
│↘l2      ↓
│  ○→○→○
│  ↓  ↓  ↓
└→○→○→○
▲▲▲
よって以下の可換性とl2の一意性より、左の四角形がp.b.である。
▼▼▼
{Ｃ}
○─────┐
│↘l2 ↘l1 ↓
│  ○→○→○
│  ↓  ↓  ↓
└→○→○→○ //
▲▲▲
(2)
∃!l1, 次が可換 ∵右の四角形がp.b.
▼▼▼
{Ｃ}
○─────┐
│   ↘l1   ↓
│  ○→○→○
│  ↓  ↓  ↓
└→○→○→○
▲▲▲
∃!l2, 次が可換 ∵左の四角形がp.b.
▼▼▼>{Ｃ}
○─────┐
│↘l2      ↓
│  ○→○→○
│  ↓  ↓  ↓
└→○→○→○
▲▲▲
よって以下の可換性とl2の一意性より、外枠の四角形がp.b.である。
▼▼▼
{Ｃ}
○─────┐
│↘l2 ↘l1 ↓
│  ○→○→○
│  ↓  ↓  ↓
└→○→○→○ //
▲▲▲

任意の2対象について積が存在し、任意の2つの矢についてequalizerが存在
⇒ 任意の○→○←○についてp.b.が存在する :性質
証明:
仮定: eはp1;f, p2;g【f∘p1, g∘p2】のequalizer
▼▼▼
{Ｃ} f    g
 A○→○C←○B
p1└←●E→┘p2
      ↑eはequalizer
      ○P
▲▲▲
∴
▼▼▼
{Ｃ}  f    g
   A○→○C←○B
e;p1└←●P→┘e;p2
        ↑l           ∃!l ∵eはequalizer
   h└←○Q→┘k      ∃!l=<h,k> ∵ＣはPの積を持つ
▲▲▲
∴これはp.b.
▼▼▼
{Ｃ}  f    g
   A○→○C←○B
e;p1└←●P→┘e;p2 //
▲▲▲

随伴

前提: Ａ,Ｂは圏
前提: Ｆ:Ａ⇄Ｂ:Ｇは関手
Ｆ,Ｇは随伴, adjunction :用語
⇔ Ｆ⊣Ｇ :表記
⇔ Ｆ⊣Ｇ:Ａ⇄Ｂ :表記、独自
定義:⇔ ∀A∈Ａ, ∀B∈Ｂ,
φ_A,B:Ｂ(ＦA,B)≅Ａ(A,ＧB):Ψ_A,B
   【φ_A,B:Ｂ(A;Ｆ,B)≅Ａ(A,B;Ｇ):Ψ_A,B】かつ A,Bについて自然(詳細は後述)
ＦはＧの左随伴, left-adjoint :用語
ＧはＦの右随伴, right-adjoint :用語

前提:Ｆ⊣Ｇ:Ａ⇄Ｂ
▼▼▼
{Ｂ}  {Ａ} 【{Ａ}   {Ｂ}  】
○ＦA ○A  【○A;Ｆ ○A   】
↓f   ↓g  【↓f    ↓g   】
○B   ○ＧB【○B    ○B;Ｇ】
     ↔            ↔ :表記、独自:左右のそれぞれの対象と射が、φ・Ψ・転置によって自然に・自然同型として対応していることを表す。
▲▲▲
⇔ f~ = φf = g :性質と表記、f~は独自
⇔ f = Ψg = g~ :性質と表記、g~は独自
g,fをそれぞれf,gの転置, transposeと呼びf~,g~で表す。φとΨは自然同型なので、f~=f,g~=gである。:性質と表記、独自
補足説明: 圏論の標準では図式を縦横転置し、かつ横線で区切って表示し、二方向規則, two-way ruleと呼ぶ。:用語
補足説明: f~は圏論標準ではfの上にバーを引くことで表す。バーをかぶせる範囲により作用範囲を表現する。

随伴の自然性
φ_A,BがA,Bについて自然 :用語((雪田))p149((Leinster))p59
定義:⇔ Ｆp;g;q ↔ p;f;Ｇq【⇔ (p;Ｆ);g;q ↔ p;f;(q;Ｇ) ⇔ q∘g∘Ｆp ↔ Ｇq∘f∘p】
表記:⇔
▼▼▼
{Ｂ}   {Ａ}   {Ｂ}     {Ａ}
○ＦA' ○A'  【○A';Ｆ ○A'   】┐
↓Ｆp  ↓p   【↓p;Ｆ  ↓p    】│Aについて自然 :用語
○ＦA  ○A   【○A;Ｆ  ○A    】│┐
↓g    ↓f   【↓g     ↓f    】││
○B    ○ＧB 【○B     ○B;Ｇ 】┘│
↓q    ↓Ｇq 【↓q     ↓q;Ｇ 】  │Bについて自然 :用語
○B'   ○ＧB'【○B'    ○B';Ｇ】  ┘
      ↔              ↔
▲▲▲

随伴の自然性公理は、射の配列
A0→...→An, An;Ｆ→B0, B0→...→Bm
【A0→...→An, ＦAn→B0, B0→...→Bm】
から、ちょうど一つの射
A0→ＧBm【A0→Bm;Ｇ】
を構成することを可能にする。((Leinster))p50

前提: Ａ,Ｂは圏
前提: Ｆ⊣Ｇ:Ａ⇄Ｂ
前提: ∀A∈Ａ, ∀B∈Ｂ,
▼▼▼
┌          ┬BにＦAを代入   ┬AにＧBを代入    ┐
○ＦA ○A    ○ＦA   ○A      ○ＦＧB ○ＧB
↓g   ↓f    ↓1_ＦA ↓η_A    ↓ε_B   ↓1_ＧB  :ηとεの定義
○B   ○ＧB  ○ＦA   ○ＧＦA  ○B     ○ＧB
└    ↔    ┴       ↔       ┴       ↔       ┘
▲▲▲
▽▽▽
┌            ┬BにA;Ｆを代入       ┬AにB;Ｇを代入    ┐
○A;Ｆ ○A     ○A;Ｆ      ○A        ○B;Ｇ;Ｆ ○B;Ｇ
↓g    ↓f     ↓1_(A;Ｆ) ↓η_A      ↓ε_B     ↓1_(B;Ｇ)  :ηとεの定義
○B    ○B;Ｇ  ○A;Ｆ      ○A;Ｆ;Ｇ  ○B       ○B;Ｇ
└    ↔      ┴         ↔          ┴        ↔      ┘
△△△
⇔ (η_A)~ = 1_ＦA, (ε_B)~ = 1_ＧB :性質
η_Aは  単位,   unit、η:1_Ａ➡ＧＦ【η:1_Ａ➡Ｆ;Ｇ】:用語
ε_Bは余単位, counit、ε:ＦＧ➡1_Ｂ【ε:Ｇ;Ｆ➡1_Ｂ】:用語
このとき、ηとεは自然変換になっている :性質((雪田))p150
証明:
▼▼▼
{Ａ}     {Ｂ}              {Ａ}     ┌補足説明
○A1     ○ＦA1   ○ＦA1   ○A1      →Ｆ追加→変更無→Ｆ除去
↓f      ↓Ｆf    ↓1_ＦA1 ↓η_A1
○A2     ○ＦA2   ○ＦA1   ○ＧＦA1  →Ｆ追加→対象変→Ｇ追加
↓η_A2   ↓1_ＦA2 ↓Ｆf    ↓ＧＦf
○ＧＦA2 ○ＦA2   ○ＦA2   ○ＧＦA2  →Ｇ除去→変更無→Ｇ追加
         ↔1     ◎2      ↔3
▲▲▲
▽▽▽
{Ａ}       {Ｂ}                     {Ａ}       ┌補足説明
○A1       ○A1;Ｆ     ○A1;Ｆ     ○A1         →Ｆ追加→変更無→Ｆ除去
↓f        ↓ f;Ｆ     ↓1_(A1;Ｆ) ↓η_A1
○A2       ○A2;Ｆ     ○A1;Ｆ     ○A1;Ｆ;Ｇ   →Ｆ追加→対象変→Ｇ追加
↓η_A2     ↓1_(A2;Ｆ) ↓ f;Ｆ     ↓ f;Ｆ;Ｇ
○A2;Ｆ;Ｇ ○A2;Ｆ     ○A2;Ｆ     ○A2;Ｆ;Ｇ  →Ｇ除去→変更無→Ｇ追加
          ↔1         ◎2         ↔3
△△△
∵↔1は自然性とηの定義
∵◎2は共にＦfに等しい
∵↔3は自然性とη定義
∴
▼▼▼
    η_A1
A1○→○ＧＦA1
 f↓◎↓ＧＦf
A2○→○ＧＦA2
    η_A2
▲▲▲
▽▽▽
    η_A1
A1○→○A1;Ｆ;Ｇ
 f↓◎↓ f;Ｆ;Ｇ
A2○→○A2;Ｆ;Ｇ
    η_A2
△△△
∴ηは自然変換
▼▼▼
{Ｂ}     {Ａ}                {Ｂ}    ┌補足説明
○ＦＧB1 ○ＧB1    ○ＧB1    ○ＦＧB1 →Ｆ除去→変更無→Ｆ追加
↓ＦＧg  ↓Ｇg     ↓1_ＧB1  ↓ε_B1
○ＦＧB2 ○ＧB2    ○ＧB1    ○B1     →Ｆ除去→対象変→Ｇ除去
↓ε_B2   ↓1_ＧB2  ↓Ｇg     ↓g
○B2     ○ＧB2    ○ＧB2    ○B2     →Ｇ追加→変更無→Ｇ除去
        ↔1       ◎2       ↔3
▲▲▲
▽▽▽
{Ｂ}       {Ａ}                      {Ｂ}
○B1;Ｇ;Ｆ ○B1;Ｇ      ○B1;Ｇ      ○B1;Ｇ;Ｆ
↓ g;Ｇ;Ｆ ↓ g;Ｇ      ↓1_(B1;Ｇ)  ↓ε_B1
○B2;Ｇ;Ｆ ○B2;Ｇ      ○B1;Ｇ      ○B1
↓ε_B2     ↓1_(B2;Ｇ)  ↓ g;Ｇ      ↓g
○B2       ○B2;Ｇ      ○B2;Ｇ      ○B2
          ↔1          ◎2           ↔3
△△△
∵↔1は自然性とεの定義
∵◎2は共にＧgに等しい
∵↔3は自然性とε定義
∴
▼▼▼
{Ｂ}    ε_B1
ＦＧB1○→○B1
ＦＧg ↓◎↓g
ＦＧB2○→○B2
        ε_B2
▲▲▲
▽▽▽
          ε_B1
B1;Ｇ;Ｆ○→○B1
 g;Ｇ;Ｆ↓◎↓ g
B2;Ｇ;Ｆ○→○B2
          ε_B2
△△△
∴εは自然変換 //

前提: Ａ,Ｂは圏
前提: Ｆ ⊣Ｇ :Ａ⇄Ｂ
前提: Ｆ'⊣Ｇ':Ｂ⇄Ｃ
Ｆ'Ｆ⊣ＧＧ':Ａ⇄Ｃ :性質((Leinster))p58
証明: Ｃ(Ｆ'ＦA,C)≅Ｂ(ＦA,Ｇ'C)≅Ｂ(A,ＧＧ'C) が自然に成り立つ //

前提: Ａ,Ｂは圏
前提: Ｆ⊣Ｇ:Ａ⇄Ｂ
このとき、以下が可換 :性質「三角等式」, ジグザグ等式, triangle identity, zig-zag identity :用語((Leinster))p61((雪田))p153p157
▼▼▼
{[Ａ,Ｂ]}     ┌{Ｂ} すなわち
┌──○Ｆ     ┌──○ＦA
│    ↓Ｆη    │    ↓Ｆη_A
│1   ○ＦＧＦ │1   ○ＦＧＦA
↓◎  ↓εＦ    ↓◎  ↓ε_ＦA
└──○Ｆ     └──○ＦA
▲▲▲
▽▽▽
{[Ａ,Ｂ]}     ┌{Ｂ} すなわち
┌──○Ｆ       ┌──○A;Ｆ
│    ↓η;Ｆ     │    ↓η_A;Ｆ
│1   ○Ｆ;Ｇ;Ｆ │1   ○Ｆ;Ｇ;Ｆ
↓◎  ↓Ｆ;ε     ↓◎  ↓ε_(A;Ｆ)
└──○Ｆ       └──○A;Ｆ
△△△
▼▼▼
{[Ｂ,Ａ]}     ┌{Ａ} すなわち
┌──○Ｇ     ┌──○ＧB
│    ↓ηＧ    │    ↓η_ＧB
│1   ○ＧＦＧ │1   ○ＧＦＧB
↓◎  ↓Ｇε    ↓◎  ↓Ｇε_B
└──○Ｇ     └──○ＧB
▲▲▲
▽▽▽
{[Ｂ,Ａ]}       ┌{Ａ} すなわち
┌──○Ｇ       ┌──○B;Ｇ
│    ↓Ｇ;η     │    ↓η_(B;Ｇ)
│1   ○Ｇ;Ｆ;Ｇ │1   ○B;Ｇ;Ｆ;Ｇ
↓◎  ↓ε;Ｇ     ↓◎  ↓ε_B;Ｇ
└──○Ｇ       └──○B;Ｇ
△△△
証明:
以下、↔1は自然性とεの定義、↔2は自然性とηの定義より成り立つ。
▼▼▼
{Ｂ}      {Ａ}        {Ｂ}
○ＦA     ○A         ○ＦA
↓η_ＦA   ↓η_A      ↓1_ＦA
○ＦＧＦA ○ＧＦA    ○ＦA
↓ε_ＦA   ↓1_ＧＦA  ↓1_ＦA
○ＦA     ○ＧＦA    ○ＦA
          ↔1        ↔2
▲▲▲
▽▽▽
{Ｂ}         {Ａ}            {Ｂ}
○A;Ｆ       ○A             ○A;Ｆ
↓η_A;Ｆ     ↓η_A          ↓1_(A;Ｆ)
○A;Ｆ;Ｇ;Ｆ ○A;Ｆ;Ｇ      ○A;Ｆ
↓ε_(A;Ｆ)   ↓1_(A;Ｆ;Ｇ)  ↓1_(A;Ｆ)
○A;Ｆ       ○A;Ｆ;Ｇ      ○A;Ｆ
            ↔1             ↔2
△△△
以下、↔1は自然性とηの定義、↔2は自然性とεの定義よりなりたつ。
▼▼▼
{Ａ}      {Ｂ}       {Ａ}
○ＧB     ○ＦＧB    ○ＧB
↓η_ＧB   ↓1_ＦＧB  ↓1_ＧB
○ＧＦＧB ○ＦＧB    ○ＧB
↓ε_ＧB   ↓ε_B      ↓1_ＧB
○ＧB     ○B        ○ＧB
          ↔1        ↔2
▲▲▲
▽▽▽
{Ａ}         {Ｂ}           {Ａ}
○B;Ｇ       ○B;Ｇ;Ｆ      ○B;Ｇ
↓η_(B;Ｇ)   ↓1_(B;Ｇ;Ｆ)  ↓1_(B;Ｇ)
○B;Ｇ;Ｆ;Ｇ ○B;Ｇ;Ｆ      ○B;Ｇ
↓ε_B;Ｇ     ↓ε_B           ↓1_(B;Ｇ)
○B;Ｇ       ○B             ○B;Ｇ
            ↔1             ↔2
△△△ //

前提: Ｆ⊣Ｇ:Ａ⇄Ｂ
∀g:ＦA→B, g~ = η_A;Ｇg
∀f:A→ＧB, f~ = Ｆf;ε_B :性質「三角等式を満たす随伴の一意性」
証明:
▼▼▼
○ＦA ○ＦA ○A
│    ↓1   ↓η_A   ∵(η_A)~ = 1_ＦA
│    ○ＦA ○ＧＦA
↓g   ↓g   ↓Ｇg
○B   ○B   ○ＧB
     =     ↔
▲▲▲
▽▽▽
△△△
▼▼▼
○A   ○A   ○ＦA
│    ↓f   ↓Ｆf
│    ○ＧB ○ＦＧB
↓f   ↓1   ↓ε_B   ∵(ε_B)~ = 1_ＧB
○ＧB ○ＧB ○B
     =     ↔
▲▲▲
▽▽▽
△△△ //

前提: Ａ,Ｂは圏
前提: Ｆ:Ａ⇄Ｂ:Ｇは関手
(1) Ｆ⊣Ｇ
1:1対応⇔ (2) 三角等式を満たす自然変換の組(η:1_Ａ→ＧＦ, ε:ＦＧ→1_Ｂ) :性質((Leinster))p62((雪田))p157
証明:
(1)⇒(2)は「三角等式」。
この対応が全単射であることを示す。そうすれば(2)⇒(1)が言える。
仮定: (η,ε)は三角等式を満たす自然変換の組
一意性は「三角等式を満たす随伴の一意性」。
仮定: g           ∈Ｂ(ＦA,B)
定義: g~ = η_A;Ｇg∈Ａ(A,ＧB) :この証明だけでの定義だが、証明が進むうちに、随伴における定義と同一であることがわかる。
仮定: f           ∈Ａ(A,ＧB)
定義: f~ = Ｆg;ε_B∈Ｂ(ＦA,B) :この証明だけでの定義だが、証明が進むうちに、随伴における定義と同一であることがわかる。
▼▼▼
{Ｂ}
┌──○ＦA
│    ↓η_A;Ｆ   
│1   ○ＦＧＦA─ＦＧg→○ＦＧB
↓    ↓ε_ＦA            ↓ε_B
└──○ＦA─────g→○B
▲▲▲
∴
g
= 1;g
= η_A;(Ｇg;Ｆ);ε_B ∵図式が可換なので
= g~;Ｆ;ε_B ∵~の定義
= g~~ ∵~の定義
▼▼▼
{Ａ}
┌──○ＧB   ←f───○A
│    ↓η_ＧB           ↓η_A
│1  ○ＧＦＧB←ＦＧf─○ＧＦA
↓    ↓Ｇε_B
└──○ＧB
▲▲▲
f
= f;1
= η_A;(Ｇf;Ｆ);Ｇε_B ∵図式が可換なので
= f~;Ｆ;Ｇε_B ∵~の定義
= f~~ ∵~の定義
∴~は随伴の転置になっている。
自然性を示す。
(ＦA─g→B─q→B')~
= (g;q)~
= η_A;Ｇ(g;q) ∵~の定義
= η_A;Ｇg;Ｇq
= g~;Ｇq ∵~の定義
= A─g~→ＧB─Ｇq→ＧB'
(A'─p→A─f→ＧB)~
= (p;f)~
= Ｆ(p;f);ε_B ∵~の定義
= Ｆp;Ｆf;ε_B
= Ｆp;f~ ∵~の定義
= ＦA'─Ｆp→ＦA─f~→B
∴(1)Ｆ⊣Ｇ
この随伴の単位はη、余単位はε。
∵(1_ＦA)~=η_A;Ｇ(1_ＦA) = η_A;1 = η_A
  (1_ＧB)~=Ｆ(1_ＧB);ε_B = 1;ε_B = ε_B

前提: Ａ,Ｂは圏
前提: Ｆ⊣Ｇ:Ａ⇄Ｂ
単位η_A:A→ＧＦA【η_A:A→A;Ｆ;Ｇ】はコンマ圏(A⇒Ｇ)の始対象 :性質「随伴の単位ηはコンマ圏(A⇒Ｇ)の始対象」((Leinster))p71
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>1>A|*>!>Ａ<Ｇ<Ｂ|B<q<ＦA)
証明:
▼▼▼
{Ａ}                {Ｂ}   {(A⇒Ｇ)}
 ┌─η_A→●ＧＦA  ●ＦA  (A⇒Ｇ)_0∋●(ＦA,η_A) ?= 0(始対象)
A○       ↓Ｇq     ↓q    (A⇒Ｇ)_1∋↓q:ＦA→B
 └──f→○ＧB     ○B    (A⇒Ｇ)_0∋○(B,f)
▲▲▲
Ｆ⊣Ｇ
⇔ 三角等式
⇒ 図式が可換
⇔ f = η_A;Ｇq
⇔ f = q~ ∵q~ = η_A;Ｇq
⇔ q = f~
∴ qは唯一、∴(ＦA,η_A)∈(A⇒Ｇ)は始対象 //

前提: Ａ,Ｂは圏
前提: Ｆ⊣Ｇ:Ａ⇄Ｂ
余単位ε_B:ＦＧB➡B【ε_B:B;Ｇ;Ｆ➡B】はコンマ圏(Ｆ⇒B)の終対象 :性質「随伴の余単位εはコンマ圏(Ｆ⇒B)の終対象」(上の命題の双対命題)
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>q>ＧB|Ａ>Ｆ>Ｂ<!<*|B<1<B)
証明:
▼▼▼
{Ａ}  {Ｂ}                 {(Ｆ⇒B)}
  A○ ＦA  ○──g→┐    (Ｆ⇒B)_0∋○(A,g)
  q↓ Ｆq  ↓       ○B   (Ｆ⇒B)_1∋↓q:A→ＧB
ＧB● ＦＧB●─ε_B→┘    (Ｆ⇒B)_0∋●(ＧB,ε_B) ?= 1(終対象)
▲▲▲
Ｆ⊣Ｇ
⇔ 三角等式
⇒ 図式が可換
⇔ g = Ｆq;ε_B
⇔ g = q~ ∵q~ = Ｆq;ε_B
⇔ q = g~
∴ qは唯一、∴(ＧB,ε_B)∈(Ｆ⇒B)は終対象 //

前提: Ａ,Ｂは圏
前提: Ｆ:Ａ⇄Ｂ:Ｇは関手
(1) Ｆ⊣Ｇ
1:1対応⇔ (2) ∀A∈Ａ, η_A:A→ＧＦAがコンマ圏(A⇒Ｇ)の始対象であるような自然変換η:1_Ａ→ＧＦ :性質「随伴の単位ηとコンマ圏(A⇒Ｇ)の始対象は1:1対応」((Leinster))p62
証明:
(1)⇒(2)は「随伴の単位ηはコンマ圏(A⇒Ｇ)の始対象」より。
仮定: η:1_Ａ→ＧＦは自然変換で、次を満たす「∀A∈Ａ, η_A:A→ＧＦAがコンマ圏(A⇒Ｇ)の始対象」
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(ＧB>1>ＧB|*>!>Ａ<Ｇ<Ｂ|B<ε_B<ＦＧB)
▼▼▼
{Ａ}                      {Ｂ}      {(ＧB⇒Ｇ)}
   ┌─η_ＧB→●ＧＦＧB  ●ＦＧB   (ＧB⇒Ｇ)_0∋●(ＦＧB,η_ＧB) = 0(始対象) ∴ηは始対象∵仮定
ＧB○   ◎     ↓Ｇε_B    ↓ε_B     (ＧB⇒Ｇ)_1∋↓ε_B:ＦＧB→B  ∴可換∵仮定、∴ε_Bは存在∵仮定、∴ε_Bは唯一∵ηは始対象⇒∴εを一意なものとして定義できる
   └───1→○ＧB      ○B       (ＧB⇒Ｇ)_0∋○(B,1)
▲▲▲
三角等式の一つは可換になる。
自然性を示す。
▼▼▼
ＧB○─η_ＧB→○ＧＦＧB
   │          ↓Ｇε_B
   ├───1→○ＧB
   │          ↓Ｇq
   └──Ｇq→○ＧB'
┌ＧB ○─η_ＧB →○ＧＦＧB
│Ｇq ↓           ↓ＧＦＧq
│ＧB'○─η_ＧB'→○ＧＦＧB'
│    │1          ↓Ｇε_B'
└Ｇq ┴=========⇉○ＧB'
▲▲▲
ε_B;qとＦＧq;ε_B'はともにコンマ圏(ＧB⇒Ｇ)の射
(ＧB,η)は始対象なので2つは等しい。
∴εは自然変換
▼▼▼
A○─η_A→○ＧＦA
 │       ↓Ｇ(1_ＦA)
 └─η_A→○ＧＦA
    A○───η_A→○ＧＦA
  η_A↓            ↓ＧＦη_A
ＧＦA○─η_ＧＦA→○ＧＦＧＦA
     │            ↓Ｇ(ε_ＦA)
     └────1→○ＧＦA
▲▲▲
Ｆη_A;ε_ＦA = 1_ＦA ∵(A,η)はコンマ圏(A⇒Ｇ)の始対象
∴三角等式のもう一つは可換になる。

前提: Ａ,Ｂは圏
前提: Ｆ:Ａ⇄Ｂ:Ｇは関手
(1) Ｆ⊣Ｇ
1:1対応⇔ (2) ∀B∈Ｂ, ε_B:ＦＧB→Bがコンマ圏(Ｆ⇒B)の終対象であるような自然変換ε:1_Ａ→ＦＧ :性質「随伴の余単位εとコンマ圏(Ｆ⇒B)の終対象は1:1対応」(上の命題の双対命題)
証明:
(1)⇒(2)は「随伴の余単位εはコンマ圏(Ｆ⇒B)の終対象」より。
仮定: ε:1_Ｂ→ＦＧは自然変換で、次を満たす「∀B∈Ｂ, ε_B:ＦＧB→Bがコンマ圏(Ｆ⇒B)の終対象」
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>η_A>ＧＦA|Ａ>Ｆ>Ｂ<!<*|ＦA<1<ＦA)
▼▼▼
{Ａ}     {Ｂ}                       {(ＦA⇒Ｆ)}
     A○ Ｆ     A○ ──1→┐      (ＦA⇒Ｆ)_0∋○(A,1)
  η_A↓  Ｆ  η_A↓   ◎    ○ＦA   (ＦA⇒Ｆ)_1∋↓η_A:A→ＧＦA ∴可換∵仮定、∴η_Bは存在∵仮定、∴η_Bは唯一∵εは終対象⇒∴ηを一意なものとして定義できる
ＧＦA●  ＦＧＦA●─ε_ＦA→┘      (ＦA⇒Ｆ)_0∋●(ＧＦA,ε_A) = 1(終対象)  ∴εは終対象∵仮定
▲▲▲
三角等式の一つは可換になる。
自然性を示す。
▼▼▼
   ＦA'○ ────┐
    Ｆq↓          ↓Ｆq
   ＦA ○───1→┤
  Ｆη_A↓         │
ＦＧＦA○─ε_ＦA→○ＦA
    ＦA'○==========┬──┐
  Ｆη_A'↓          ↓1   │
ＦＧＦA'○───1→○ＦA'│
ＦＧＦq ↓         │Ｆq  │Ｆq
ＦＧＦA ○─ε_ＦA→○ＦA←┘
▲▲▲
q;η_Aとη_A';ＧＦqはともにコンマ圏(ＦA⇒Ｆ)の射
(ＦA,ε)は終対象なので2つは等しい。
∴ηは自然変換
▼▼▼
Ｆ   ＧB ○─ε_B─┐
Ｆ(1_ＧB)↓       ↓
Ｆ   ＧB ○─ε_B→○B
Ｆ    ＧB○─────┐
Ｆ(η_ＧB)↓           ↓1
ＦＧＦＧB○─ε_ＦＧB→○ＦＧB
ε_  ＦＧB↓            │ε_B
ＦＧ   B ○───ε_B→○B
▲▲▲
Ｆ(η_ＧB);ε_ＦＧB = 1_ＧB ∵(B,ε)はコンマ圏(Ｇ⇒B)の終対象
∴三角等式のもう一つは可換になる。

前提: Ａ,Ｂは圏
前提: Ａ←Ｂ:Ｇは関手
Ｇが左随伴を持つ
⇔∀A∈Ａ, コンマ圏(A⇒Ｇ)が始対象を持つ :性質((Leinster))p74
証明:
⇒は「随伴の単位ηはコンマ圏(A⇒Ｇ)の始対象」。
⇐を示す。
仮定: ∀A∈Ａ, コンマ圏(A⇒Ｇ)の始対象を(Ｆ(A),η:A→ＧＦA)とする。:この証明だけでの定義だが、証明が進むうちに、随伴における定義と同一であることがわかる。
仮定: f:A→A'
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(A>f>A'|Ａ>1>Ａ<Ｇ<Ｂ|Ｆ(A')<Ｆ(f)<Ｆ(A))
▼▼▼
{Ａ}                       {Ｂ}
A ○─η_A →○Ｇ(Ｆ(A ))  ○Ｆ(A )
f ↓         ↓Ｇ(Ｆ(f ))  ↓Ｆ(f ) :定義
A'○─η_A'→○Ｇ(Ｆ(A'))  ○Ｆ(A')
▲▲▲
∴このＦは関手になっている。(省略)
図式よりηは自然変換1→ＧＦだといえる。
「随伴の単位ηとコンマ圏(A⇒Ｇ)の始対象は1:1対応」より、ＦはＧの左随伴である。 //

前提: Ａ,Ｂは圏
前提: Ｆ:Ａ←Ｂは関手
Ｆが右随伴を持つ
⇔∀B∈Ｂ, コンマ圏(Ｆ⇒B)が終対象を持つ :(上の命題の双対命題)
証明:
⇒は「随伴の余単位εはコンマ圏(Ｆ⇒B)の終対象」。
⇐を示す。
仮定: ∀B∈Ｂ, コンマ圏(Ｆ⇒B)の終対象を(Ｇ(B),ε:ＦＧB→B)とする。:この証明だけでの定義だが、証明が進むうちに、随伴における定義と同一であることがわかる。
仮定: g:B'→B
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(Ｇ(B')>Ｇ(f)>Ｇ(B)|Ａ>Ｆ>Ｂ<1<Ｂ|B<f<B')
▼▼▼
{Ａ}      {Ｂ}
Ｇ(B')○  Ｆ(Ｇ(B'))○─ε_B'→○B'
Ｇ(f )↓  Ｆ(Ｇ(f ))↓         ↓f  Ｇ(f ):定義
Ｇ(B )○  Ｆ(Ｇ(B ))○─ε_B →○B
▲▲▲
∴このＧは関手になっている。(省略)
図式よりεは自然変換ＦＧ→1だといえる。
「随伴の余単位εとコンマ圏(Ｆ⇒B)の終対象は1:1対応」より、ＧはＦの右随伴である。 //

▼▼▼
{Ｃ}
!C○ ○C
 !↓ ↓h    ∴hは唯一∵!が唯一なので
 *○ ○Ｕ*  ∴Ｕ*は終対象
   ↔
▲▲▲
▼▼▼
{Ｃ}
 *○ ○Ｆ*  ∴Ｆ*は始対象
 !↓ ↓h    ∴hは唯一∵!が唯一なので
!C○ ○C
   ↔
▲▲▲
∴始対象 ⊣ ! ⊣ 終対象 :性質((Awodey))p224

巾

矢の積, product of arrows :用語
f×g 定義:= <f∘p1, g∘p2>:A×C→B×D
▼▼▼
{Ｃ}
   A○──f→○B
  p1↑       ↑p1
A×C○-f×g→○B×D
  p2↓       ↓p2
   C○──g→○D   //
▲▲▲

前提: Ｃは二項積を持つ圏
積関手: -×A:Ｃ⇨Ｃ
(-×A)(X) = X×A :定義:積関手の対象の対応
(-×A)(f:X→Y) = f×1_A:X×A→Y×A :定義:積関手の射の対応
コンマ圏(-×A⇒B)に終対象が存在するとき、終対象をB^Aと記し、巾関手を定義することができる。 :性質
巾関手: -^A:Ｃ⇨Ｃ
(-^A)(Y) = Y^A :定義:巾関手の対象の対応
(-^A)(g:Y→Z) = g^A:X^A→Z^A :定義:巾関手の射の対応
補足説明: コンマ圏の図式で以下代入する。(A>f>A'|Ａ>Ｐ>Ｃ<Ｑ<Ｂ|B'<g<B)←(X>f'>B^A|Ｃ>-×A>Ｃ<!<*|B<1<B)
▼▼▼
{Ｃ}                      {(-×A⇒B)}
X  ○    X×  A○- f→┐  (-×A⇒B)_0∋○∀(X  ,f:X×A→B)
f' ↓   f'×1_A↓ ◎  ○B (-×A⇒B)_1∋↓∃!f':X→B^A, f = f'×1_A;ev ∵(B^A,ev)は終対象 :補足説明:この条件は圏論界での巾の普遍性の性質そのもの。
B^A●  B^A×  A●-ev→┘  (-×A⇒B)_0∋●  (B^A,ev:B^A×A→B) = 1(終対象)
▲▲▲
∴ -×A ⊣ -^A
巾, 冪, exponentiation :用語、はば・きれでIME変換
evを評価, 値づけ, evaluationと呼ぶ :用語

その他

前提: Ｃはデカルト閉圏
(A^B)^C≅A^(B×C) :性質「指数法則」((Awodey))p218
証明:Ｃ(X,(A^B)^C)≅Ｃ(X×C,(A^B))≅Ｃ((X×C)×B,A)≅Ｃ(X×(B×C),A)≅Ｃ(X,A^(B×C)), 自然性は省略 //

前提: Ｃは局所小デカルト閉圏
A^C×B^C≅(A×B)^C:性質((Awodey))p230
証明:Ｃ(X,A^C×B^C)≅Ｃ(X,A^C)×Ｃ(X,B^C)≅Ｃ(X×C,A)×Ｃ(X×C,B)≅Ｃ(X×C,A×B)≅Ｃ(X,(A×B)^C), 自然性は省略 //

前提: Ｃは局所小デカルト閉圏
A^B×A^C≅A^(B+C):性質((Awodey))p230
証明:Ｃ(X,A^B×A^C)≅Ｃ(X,A^B)×Ｃ(X,A^C)≅Ｃ(X×B,A)×Ｃ(X×C,A)≅Ｃ((X×B)+(X×C),A)≅Ｃ(X×(B+C),A)≅Ｃ(X,A^(B+C)), 自然性は省略 //

前提: Ｃはデカルト閉圏で余積を持つ
(A×B)+(A×C)≅A×(B+C):性質「分配律」((Awodey))p219
証明:Ｃ(A×(B+C),X)≅Ｃ(B+C,X^A)≅Ｃ(B,X^A)×Ｃ(C,X^A)≅Ｃ(A×B,X)×Ｃ(A×C,X)≅Ｃ((A×B)+(A×C),X), 自然性は省略 //

X×1≅X :性質
証明:Ｃ(X×1,Y)≅Ｃ(X,Y^1)≅Ｃ(X,Y) //

X+0≅X :性質
証明:Ｃ(X+0,Y)≅Ｃ(X,Y)×C(0,Y)≅Ｃ(X,Y)×1≅Ｃ(X,Y) //

前提 Ｆ⊣Ｇ:Ａ⇄Ｂ
Ｆは余極限を保存する、Ｇは極限を保存する:性質((Leinster))p188
証明:
前提: Ｄ:Ｉ⇨Ｂは極限の図式
Ａ(A,ＧlimＤ)≅Ｂ(ＦA,limＤ)≅limＢ(ＦA,Ｄ)≅limＢ(A,Ｇ∘Ｄ)≅Cone(A,Ｇ∘Ｄ)≅Ａ(A,lim(Ｇ∘Ｄ))
∴Ｇは極限を保存する
∴Ｆは余極限を保存する∵双対性
自然性は省略 //

反変巾集合関手Ｐ:Set^op→Setは自己随伴:性質((Awodey))p338
証明:Set(A,ＰB)≅Set(A,2^B)≅Set(B,2^A)≅Set(B,ＰA)≅Set^op(Ｐ^opA,B), 自然性は省略 //

概念の依存関係

将来はオントロジーログにしたい。

終対象1は!:Ｃ→*の右随伴
極限は対角関手の右随伴
始対象0は!:Ｃ→*の左随伴
余極限は対角関手の左随伴
極限はコンマ圏(Δ⇒Ｄ)の終対象
随伴の余単位ε_Bはコンマ圏(Ｆ⇒B)の終対象
余極限はコンマ圏(Ｄ⇒Δ)の始対象
余極限は余錐の圏の始対象
随伴の単位η_Aはコンマ圏(A⇒Ｇ)の始対象
終対象は「空圏」型図式の極限
始対象は「空圏」型図式の余極限

更新履歴

2024/05/08a 新規公開
2024/05/09a hom関手のミス修正、整形、成分の解説を追加、更新履歴を追加、フォント指定を注意に移動、性質の証明を追加、
2024/05/10a 一部の対象を強調、関手・自然変換の矢印を変更、文言を調整、
2024/05/12a hom関手・対角関手の一部ミス修正、hom関手に実験情報追加、
2024/05/16a hom関手の向き変更、対角関手の落とし穴情報を追加、記号の編集ミスを修正、文言を調整、

参考文献

((記号)) 情報
((MacLane)) S.マックレーン著, 三好博之, 高木理訳, 圏論の基礎, 丸善出版, 2012.
((Awodey)) S.アウディ著, 前原和寿訳圏論原著第2版, 共立出版, 2015.
((Leinster)) T.レンスター著, 斎藤恭司監修, 土岡俊介訳, ベーシック圏論, 丸善出版, 2017
((雪田)) 雪田修一著, 圏論入門 Haskellで計算する具体例から, 日本評論社, 2020
((西郷-道案内)) 西郷甲矢人, 能美十三著, 圏論の道案内, 技術評論社, 2019
((Fong-Spivak)) B.Fong, D.Spivak著, 川辺治之訳, 活躍する圏論, 共立出版, 2023
((Spivak)) D.Spivak著, 川辺治之訳, みんなの圏論, 共立出版, 2021
((清水-高階)) 清水義夫著, 圏論による論理学高階論理とトポス, 東京大学出版会 2007
((清水-記号)) 清水義夫著, 記号論理学講義基礎理論束論と圏論知識論, 東京大学出版会 2013
((田中)) 田中久美子著, 記号と再帰, 東京大学出版会 2010
((MacLane-数学)) S.マックレーン著, 彌永昌吉監修, 赤尾和男, 岡本周一訳, 数学その形式と機能, 1992
((西郷-田口)) 西郷甲矢人, 田口茂著, 現実とは何か, 筑摩書房, 2019
((西郷-集合)) 西郷甲矢人, 能美十三著, 圏論的集合論集合圏とトポス, 現代数学社, 2021
((前原)) 前原和壽著, 圏論入門, 共立出版, 2018
((斎藤) 斎藤毅著抽象数学の手ざわり, 岩波書店, 2021
((Bradley)) T.Bradley, T.Bryson, J Terilla著, 小森洋平訳, 圏論によるトポロジー, 森北出版, 2023
((中岡)) 中岡宏行著, 圏論の技法, 日本評論社, 2015
((西郷-委員会)) 圏論の歩き方委員会, 圏論の歩き方, 日本評論社, 2015
((西郷-地平線)) 西郷甲矢人著, 圏論の地平線, 技術評論社, 2022
写像の合成 https://ja.wikipedia.org/wiki/%E5%86%99%E5%83%8F%E3%81%AE%E5%90%88%E6%88%90
逆ポーランド記法 https://ja.wikipedia.org/wiki/%E9%80%86%E3%83%9D%E3%83%BC%E3%83%A9%E3%83%B3%E3%83%89%E8%A8%98%E6%B3%95
Z言語 https://ja.wikipedia.org/wiki/Z%E8%A8%80%E8%AA%9E
https://en.wikipedia.org/wiki/Composition_of_relations
https://math.stackexchange.com/questions/314794/diagrammatic-postfix-composition-of-functions
https://rosettacode.org/wiki/Function_composition
https://qiita.com/norkron/items/f90d851daf05a2efa567