第7部　圏論と普遍性

始対象Iについて、各Xへの射と、その射型が一要素である証明を組にします。

始性は ∀X, ∃! f:I⟶X, True、すなわち各hom型 I⟶X が可縮であることです。データとして中心射 desc X : I⟶X と、任意の f:I⟶X に対する f=desc X を持ちます。単なる射の存在だけでは普遍性にならず、 一意性が異なる選択を同じにします。Leanでは Unique (I ⟶ X) または IsInitial I の射と一意性フィールドとして 読めます。

自由対象では「生成元写像を延長する射」の型が一要素であるという相対的な始性へ一般化します。

二つの始対象I,Jの普遍射 f:I⟶J と g:J⟶I を取り、合成を恒等射と比較します。

始性からfとgが一意に存在します。g≫f:I⟶I と 𝟙 I は同じhom型の射なので始性の一意性から等しく、同様に f≫g=𝟙 J です。従ってfは同型です。さらにIからJへの射自体が一意なので、この同型も一意です。「等しい」ではなく 圏内で同型というのが一般の結論であり、骨格化や一価性がある場合にだけ対象等式へ強められます。

極限、自由対象、表現対象の一意性も、普遍射を往復させる同じ証明雛形で得られます。

Cの終対象は反対圏Cᵒᵖの始対象です。

終対象Tは各XからTへの一意な射 X⟶T を持ちます。反対圏ではこれは op T⟶op X となり、op Tから任意対象への 一意な射なので始対象です。始対象一意性の証明を反対圏へ適用すれば、二つの終対象の間の一意な同型も得られます。 双対化では対象は同じでも、合成順 f≫g が反対圏で逆になることを型が管理します。

モノ射とエピ射、積と余積、極限と余極限も、定義を反対圏へ移して体系的に双対化します。

f:X⟶A と g:X⟶B から対射 ⟨f,g⟩:X⟶A×B を作ります。

積Pには射影 π₁:P⟶A、π₂:P⟶B があります。任意の錐f,gに対し媒介射uを作り、 u≫π₁=f と u≫π₂=g を要求します。Type では u x=(f x,g x) です。別のvが同じ二式を満たせば、各xで 第一・第二成分が一致し、積外延性からv=uです。存在と一意性を合わせてPが離散二点図式の極限になります。

複数の観察を一つの対象へ束ねるAPIを、積への媒介射として設計できます。

Hom(X,P)→Hom(X,A)×Hom(X,B) を射影との合成で定義します。

写像 Φ_X(u)=(u≫π₁,u≫π₂) の逆を Ψ_X(f,g)=⟨f,g⟩ とします。β則で Φ_X∘Ψ_X=id、η則で Ψ_X∘Φ_X=id なので全単射です。さらに k:Y⟶X による前合成と可換し、Xについて自然です。この自然性を含む Hom(-,P)≅Hom(-,A)×Hom(-,B) が、積を表現対象として特徴づけます。

普遍対象をhom関手の自然同型として表すと、米田の補題から一意性を統一的に導けます。

空添字族への錐は脚を一つも持たず、任意のXから頂点Pへの一意な射だけが残ります。

零項積Pの普遍性は、各XからPへの媒介射が一意に存在することです。従ってPは終対象です。脚がないため可換条件は 空虚ですが、一意な媒介射の条件は消えません。集合の空積が一要素集合になるのも、空の選択関数がただ一つあるためです。 「要素がない積」を空集合と考えると、積の普遍性ではなく和の直観を混ぜています。

零項演算を含めると、有限積を持つ圏には終対象も含まれるという定義上の慣例を正確に読めます。

f:A⟶X と g:B⟶X を場合分けする射 [f,g]:A+B⟶X にまとめます。

余積Qには注入 ι₁:A⟶Q、ι₂:B⟶Q があり、任意の余錐f,gへ一意なuを与えて ι₁≫u=f、ι₂≫u=g とします。Type ではuは和型の二構成子をfとgで場合分けします。別のvも同じ式を満たせば、 和型の各構成子の場合にuとvが一致するので関数外延性で等しいです。

異なる入力形式を一つの処理へ統合する設計を、余積からの一意な射として捉えられます。

余積から出る射を二つの注入との前合成へ送ります。

Hom(Q,X)≅Hom(A,X)×Hom(B,X) を u↦(ι₁≫u,ι₂≫u) と [f,g] で構成します。β・η則が逆法則を与え、 XからYへの射による後合成について自然です。積の式では可変対象Xがhomの第一引数にあり反変でしたが、余積では 第二引数にあり共変です。射の向きが自然性の向きも決めます。

表現可能関手と余表現可能関手を見分ける際、homの変数位置を最初に確認します。

積の対象・射・等式を反対圏へ移し、op/unop後の向きを一行ずつ戻します。

CᵒᵖでA,Bの積Qを取ると、射影 Q⟶op A はCで注入 A⟶unop Q になります。Cᵒᵖの錐 op X⟶Q はCの余錐 unop Q⟶X へ反転し、媒介射の存在一意性もCで余積の条件になります。従って反対圏の積は 元の圏の余積です。式を左右の語の置換だけでなく、各射の型へ戻すことで合成順の誤りを防げます。

新しい双対定理を述べるときは、反対圏で既存定理を適用してから記法を翻訳します。

結合律の三射に対象を四つ付け、両辺の始域と終域を確認します。

f:X⟶Y、g:Y⟶Z、h:Z⟶W なら (f≫g)≫h と f≫(g≫h) はともにXからWへの射です。単位律は 𝟙 X≫f=f と f≫𝟙 Y=f。型が合うだけでは等式は従わず、圏構造の法則として必要です。homが異なる宇宙に 属しても合成の入出力は一致しなければならず、対象宇宙と射宇宙を別に持つことで大きな圏も扱えます。

型付きAPIでは圏の型付けが接続不能な操作を排除し、法則が再括弧付けの意味保存を保証します。

対象を一つにし、自己射をモノイド要素、合成をモノイド演算にします。

文字列と連結から一対象圏を作ります。唯一の対象を★、Hom(★,★)=String、恒等射を空文字列、合成を連結とします。 連結の結合律と空文字列の単位律が圏法則です。自然数加法なら恒等射0、合成+の別例になります。非可換モノイドでは 合成順が観察できるため、どちらの文字列を先に連結するかを圏の ≫ の規約と一致させます。

一対象圏の関手はモノイド準同型、自然変換は適切な交換条件を満たす要素として読めます。

「左逆を持つ射はモノ射」を反対圏へ適用します。

Cでfが右逆gを持ち f≫g=𝟙 とします。反対圏では f.op は左逆 g.op を持つためモノ射です。反対圏のモノ射は Cのエピ射なので、右逆を持つ射はエピ射と分かります。直接には u≫f=v≫f の両辺へgを後合成し、結合律と 右逆式でu=vを得ます。双対化した結論を直接証明すれば、向きの誤りを発見できます。

分裂モノ射と分裂エピ射、核と余核なども同じ方法で双対定理を生成します。

一対象圏の関手が自己射に与える写像を取り出します。

モノイドM,Nを一対象圏と見ると、関手Fは唯一の対象を唯一の対象へ送り、射写像 φ:M→N を与えます。恒等射保存 F(𝟙)=𝟙 は φ(e_M)=e_N、合成保存 F(f≫g)=F f≫F g は φ(m·n)=φ(m)·φ(n) です。従って関手法則は モノイド準同型の単位・積保存則そのものです。対象写像が自明でも射と法則が情報を持ちます。

群・環を一対象または構造付き圏として見ると、構造保存写像を関手の特殊例として比較できます。

(F⋙G).map f=G.map(F.map f) を二つの保存則で順に書き換えます。

恒等射について G.map(F.map(𝟙 X))=G.map(𝟙(FX))=𝟙(G(FX))。合成について G.map(F.map(f≫g))=G.map(F.map f≫F.map g)=G.map(F.map f)≫G.map(F.map g) です。各等号の一段目はF、二段目はGの 関手法則です。対象写像の合成だけ定めても射写像とこれらの証明がなければ関手になりません。

関手合成の結合性が定義的か自然同型までかを、実装上のレコード表現と区別して確認します。

反変関手を Cᵒᵖ⥤D とし、Cの射 f:X⟶Y をopしてmapします。

f:X⟶Y は反対圏で f.op:op Y⟶op X なので、Fは F(op Y)⟶F(op X) を返します。合成 f≫g のopは g.op≫f.op となり、F.mapはこの順序の合成を保存します。したがって「反変関手が合成を逆にする」 という別法則を追加せず、通常の関手法則と反対圏の合成で表現できます。

前層、homの第一変数、双対空間を反対圏からの通常の関手として統一します。

η:F⟶G の成分と f:X⟶Y に対し、FXからGYへ至る二経路を書きます。

成分は η_X:F X⟶G X です。二経路は F.map f≫η_Y と η_X≫G.map f で、ともにFXからGYへ行きます。 自然性は両者の等式です。対象ごとの射を集めただけではこの整合条件がなく、圏の射に沿って選択が一様とは限りません。 正方形は記憶用の図ではなく、型が許す二つの合成を比較したものです。

多相関数の自然性やデータ構造mapとの可換性を、関手間の自然変換として表せます。

モノイド準同型φ,ψの間の成分はNの一要素nで、自然性を全mについて書きます。

一対象圏の関手F,Gは準同型 φ,ψ:M→N です。自然変換の唯一の対象成分は a∈N。自然性は全mについて φ(m)·a=a·ψ(m) です。Nが可換でφ=ψなら任意のaが自然変換になります。一般にはこの交換子条件を満たすaだけです。 従って対象成分の型が存在しても、自然性方程式に解があるとは限りません。

表現間のintertwinerや加群準同型も、作用と交換する自然変換として読めます。

恒等自然変換と垂直合成を対象ごとの恒等射・合成で定義します。

(𝟙 F)_X=𝟙(FX)、(η≫θ)_X=η_X≫θ_X と定めます。合成の自然性はηとθの自然性を順に使い、結合律で括弧を 整えます。左右単位律と結合律は各XでDの圏法則へ還元し、自然変換の外延性から全体の等式になります。したがって 関手を対象、自然変換を射とする関手圏が得られます。

修飾や水平合成も成分計算へ下ろし、2圏的な交換則の準備にします。

包含とレトラクションで左逆だけ、全射と切断で右逆だけの例を作ります。

包含 i:{0}→{0,1} は定値レトラクションrを持ち r∘i=id ですが i∘r≠id なので同型ではありません。逆に 射影 p:{0,1}→{0} は切断を持つ右可逆射ですが単射でなく同型ではありません。同型には同じ逆射が左右両方の 逆法則を満たす必要があります。左逆からmono、右逆からepiは従いますが、一般圏でmonoかつepiでも同型とは限りません。

圏同値でも完全忠実性と本質的全射性を別々に検査し、片方向の情報だけで同値としないようにします。

ηの自然性式の左右へ成分逆を合成して、逆成分の自然性へ変形します。

F f≫η_Y=η_X≫G f に左から η_X⁻¹、右から η_Y⁻¹ を合成します。結合律と逆法則で整理すると G f≫η_Y⁻¹=η_X⁻¹≫F f となり、逆成分族の自然性です。対象ごとの同型を逆にするだけでなく、元の自然性を 使って成分族が自然変換になることを示す必要があります。

自然同型の合成・水平合成でも、成分同型と自然性を別の証明義務として管理します。

擬逆と単位・余単位から完全忠実性・本質的全射性を示し、逆向きは対象の原像を選びます。

同値 F:C⥤D に擬逆Gと自然同型 GF≅Id、FG≅Id があれば、hom写像の逆をGと同型成分で構成してFは完全忠実です。 任意のdは F(Gd)≅d なので本質的全射です。逆に完全忠実かつ本質的全射なら、各dに原像Gdと同型を選びます。 射へのGはFのhom全単射で持ち上げ、法則と自然同型を一意性から示します。後者の構成には対象ごとの選択が現れます。

具体的圏の同値を示す際、擬逆を直接作る方法と完全忠実・本質的全射を示す方法を比較します。

添字圏Jに二対象だけを置き、恒等射以外の射を持たせません。

図式Dは二対象をA,Bへ送ります。Xを頂点とする錐は脚 f:X⟶A、g:X⟶B だけで、非自明な自然性条件はありません。 終錐は任意のf,gから一意な媒介射を持つので、まさに積の普遍性です。離散一対象なら極限はその対象、空図式なら 終対象になります。添字圏の射が増えると、脚の間に可換条件が加わります。

等化子・引戻しも添字圏の形を変えた極限として、個別定義を一つの概念へ統合できます。

各極限錐を、もう一方の終錐性へ入力して頂点間の射を得ます。

極限錐LとMがあれば、Mの錐からLの終性で u:M.pt⟶L.pt、Lの錐からMの終性で v:L.pt⟶M.pt を得ます。 合成 v≫u と恒等射はLの各脚との合成が等しいため、媒介射の一意性から一致します。逆合成も同様です。さらにuは 各脚と可換する唯一の同型で、単なる対象同型より図式に対する整合性が強いです。

極限の異なる具体構成を交換するとき、この標準同型が後続の射と自然に可換することを利用します。

共通終域への二射を反対圏で共通始域からの二射として読み替えます。

f:X⟶Z、g:Y⟶Z の引戻しPは射 P⟶X,P⟶Y を持ち、Zへの合成が一致する普遍錐です。反対圏では f.op:op Z⟶op X、g.op:op Z⟶op Y の押出しとなり、元の圏では注入 X⟶Q,Y⟶Q と共通射への一意な媒介射を 持ちます。可換式も合成順を反転して押出しの式になります。

base changeとcobase changeの定理を反対圏で対応させ、片側だけの直観に依存しないようにします。

共変hom関手 Hom(A,-) は射fへ後合成、反変hom関手 Hom(-,A) は前合成を割り当てます。

Hom(A,-) は f:X⟶Y に h↦h≫f を割り当てます。恒等保存は右単位律、合成保存は結合律です。 Hom(-,A) はfに k↦f≫k を反対向きに割り当て、同じ二法則で関手になります。homの二変数を同時に扱う Hom:Cᵒᵖ×C→Type では射対 (f,g) が h↦f≫h≫g を与えます。

表現可能性を読む前に、どちらのhom変数を固定した関手かを必ず特定します。

関手Fと元 u∈F R から、射 f:R⟶X を F f(u) へ送ります。

普遍元 (R,u) は各Xで Φ_X:Hom(R,X)→F X, f↦F(f)(u) が全単射になるものです。逆写像は各 x∈F X に 一意な射 f:R⟶X を対応させます。g:X⟶Y に対し F g(Φ_X f)=F(g)(F(f)u)=F(f≫g)u=Φ_Y(f≫g) なのでΦは 自然です。普遍元はRでの一要素から全対象のF要素を一意に生成します。

自由群の普遍元を生成元写像として読み、準同型全体との自然な対応を構成します。

関手 X↦Hom(X,A)×Hom(X,B) を、どの対象の反変hom関手が表現するか考えます。

積Pと射影から Hom(X,P)≅Hom(X,A)×Hom(X,B) がXについて自然に得られます。従って反変関手 Hom(-,A)×Hom(-,B) はPにより表現されます。普遍元はX=Pで恒等射に対応する対 (π₁,π₂) です。逆にこの関手の 表現対象Rと普遍元を取れば、その二成分を射影とし、自然全単射から積の媒介射と一意性を回収できます。

極限一般を「錐の関手」の表現対象として捉えると、普遍性と表現可能性が同じ構造になります。