第7部 圏論と普遍性

問題1制限の合成則を二つの記法で導く

Problem

問題

射 X→Y→Z と前層 P を取り、P(Z)→P(Y)→P(X) の各写像の始域と終域を書いてください。反対圏で (f≫g)ᵒᵖ=gᵒᵖ≫fᵒᵖ となることから、関手法則を制限写像の合成則へ翻訳します。 Leanで P.map_comp g.op f.op を使って同じ式を証明し、式の順序を逆にした候補が型検査を通らない理由まで説明できれば完了です。

ヒント

前層Pを Cᵒᵖ⥤Type と書く記法と、制限写像 s↦s|_f の記法を並べます。

解答

f:U⟶V、g:V⟶W に対し反変性から P(g≫f)=P(f)∘P(g) です。切断記法では (s|_g)|_f=s|_{g≫f}。恒等射について s|_{𝟙}=s です。関手記法では通常の合成保存則ですが、opにより元の圏の射順が反転します。二記法を対応させると、制限を二回行う領域の順序を誤りにくくなります。

座標変換、環の局所化、文脈への再添字付けも同じ反変合成則で追跡できます。

Lean検査済みL407–416

open _root_.CategoryTheory

universe u

variable {C : Type u} [Category.{u} C]

theorem restrictionComposition (P : Cᵒᵖ ⥤ Type u)
    {U V W : C} (f : U ⟶ V) (g : V ⟶ W) :
    P.map (f ≫ g).op = P.map g.op ≫ P.map f.op := by
  simp

問題2対象ごとの写像を自然変換へ昇格する

Problem

問題

二つの集合値前層 P,Q と関数族 η_X:P(X)→Q(X) を考えます。自然変換にするための可換式を全ての f:X→Y について書き、定値前層間では一つの関数 a→b がその条件を満たすことを証明してください。次に対象ごとに異なる関数を選び、自然性が破れる小さな圏の例を構成します。データと法則の両方を NatTrans のフィールドへ対応させられれば完了です。

ヒント

η_U:P(U)→Q(U) がすべての制限写像と可換する条件を書きます。

解答

各Uの写像η_Uに対し、f:V⟶U について Q(f)(η_U s)=η_V(P(f)s) が必要です。左辺は変換後に制限し、右辺は制限後に変換します。この式が全f,sで成り立てばηは前層間の自然変換です。例えば連続関数を値ごとに二乗する操作は制限と可換し、「定義域全体で積分する」操作は一般に制限と可換しないため前層射になりません。

局所的なデータ変換をAPI化するとき、領域縮小との可換性を合成可能性の条件にします。

問題3定値前層が層にならない状況を分析する

Problem

問題

二つの互いに交わらない非空開集合からなる空間を考え、二点以上を持つ集合 A の定値前層を置きます。二領域に異なる値を選んだ局所データが交わり上で一致することと、全体上の定数へ貼り合わさらないことを示してください。どの段階までは前層法則だけで成立し、どの段階で貼り合わせの存在が失敗したかを区別します。同じ例を局所定値関数の層と比較し、定値前層と定値層を識別できれば完了です。

ヒント

非連結な開集合を二つの互いに素な開集合で被覆し、異なる定数を各成分に置きます。

解答

集合Aをすべての非空開集合へ割り当て、制限を恒等とする定値前層を考えます。U=U₁⊔U₂ が非連結なら、U₁にa、 U₂にb≠aを置いた局所切断は交わりが空なので整合します。しかしU上の定値切断は一つの値しか取れず、両方へ貼り合いません。従ってAが一要素でない限り層条件に失敗します。局所定値関数の層は成分ごとに値を選べるため、この欠陥を修正します。

層条件は局所的一致だけでなく、位相の連結性に応じた大域データの柔軟性も要求します。

第59章

篩・Grothendieck位相・サイト

問題1主篩の普遍性を証明する

Problem

問題

射 f:Y→X が生成する主篩を、h:Z→X がある g:Z→Y によって h=g;f と書けるという条件で記述してください。この集まりが前合成で閉じることを結合律から証明します。さらに f を含む任意の篩 S が主篩を含むことを示し、Sieve.generate_le_iff の特殊例へ対応させてください。包含の向きを言葉でも説明できれば完了です。

ヒント

射f:Y→Xが生成する主篩を、fを経由するXへの射全体として定めます。

解答

⟨f⟩={g:Z→X | ∃h:Z→Y,h≫f=g} とします。これは前合成で閉じるので篩です。fを含む任意の篩Sは前合成閉性から fを経由するすべてのgを含むため ⟨f⟩⊆S。従って主篩はfを含む最小の篩です。米田前層 yX の部分前層としては、 fの像部分前層に一致します。

位相空間の開包含では主篩が一つの被覆片以下の開集合全体を表します。

問題2引戻し公理の合成安定性を証明する

Problem

問題

篩 S と射 Z→Y→X に対し、合成に沿う一回の引戻しと二回の引戻しが同じ射を含むことを両方向に示してください。定義を展開すると双方が S(h;g;f) へ帰着することを結合律で確認します。続いて S∈J(X) から二通りに Z 上の被覆を得て、Grothendieck位相の安定性がこの等式と両立することを説明できれば完了です。

ヒント

篩Sのfに沿う引戻しを f* S={g | g≫f∈S} とし、二射で計算します。

解答

f:Y→X、g:Z→Y なら g*(f*S)=(f≫g)*S です。実際hが左辺に属すことは h≫g∈f*S、すなわち (h≫g)≫f∈S で、結合律によりhが右辺に属すことと同値です。従ってSがXを被覆し、被覆篩が任意射の引戻しで被覆なら、二段の基底変換も一段の基底変換として被覆になります。

局所性を再添字付けに安定な条件として設計すると、ファイブレーション上の被覆へ一般化できます。

問題3三公理から上方閉性を導く

Problem

問題

被覆篩 S と包含 S≤R を仮定します。推移性を S と R へ適用し、各 f∈S について f*R=⊤ となることを示して R の被覆性を導いてください。どこで包含を使い、どこで篩の下方閉性を使ったかを分離します。最後に二被覆の共通部分が被覆である証明を組み立て、追加公理ではなく導出定理であることを確認できれば完了です。

ヒント

被覆篩S⊆Rに対し、局所性公理をRへ適用し、Sに属する各射上でRの引戻しが最大篩になることを示します。

解答

SがXの被覆でS⊆Rとします。任意の f:Y→X がSに属すれば、恒等射を含め任意のgとの合成g≫fはS、従ってRに属します。よって f*R はY上の最大篩で被覆です。局所性公理を被覆Sに沿ってRへ適用するとRもXの被覆です。最大篩公理、引戻し安定性、局所性から被覆篩族の上方閉性が導かれます。

基底を被覆族で与える場合も、生成される篩位相で上方閉性が自動的に満たされることを確認します。

第60章

層条件・貼り合わせ・層化

問題1整合族と貼り合わせを定義から判定する

Problem

問題

被覆篩 S、前層 P、大域要素 t∈P(X) を取り、x_f=P(f)(t) と定めてください。二つの合成 g₁;f₁=g₂;f₂ に沿う制限が一致することを、前層の合成保存則から証明します。さらに t が x の貼り合わせであることを示し、Leanの is_compatible_of_exists_amalgamation と各定義へ対応させてください。どの推論が層条件を使わず全前層で成立するかを指摘できれば完了です。

ヒント

被覆 U=⋃Uᵢ 上の切断sᵢが交叉上で一致し、大域切断sが各sᵢへ制限されることを書きます。

解答

整合性は全i,jで sᵢ|_{Uᵢ∩Uⱼ}=sⱼ|_{Uᵢ∩Uⱼ}。貼り合わせは s∈F(U) で全iに s|_{Uᵢ}=sᵢ を満たすものです。層条件は各整合族に貼り合わせが一意に存在すること。連続実数値関数では点ごとに s(x)=sᵢ(x)を選び、整合性がwell-definedness、局所的連続性が大域的連続性、一意性が被覆性から従います。

局所解から大域解を作る議論では、整合性、存在、一意性のどこが失敗し得るかを分けます。

問題2分離的だが層でない前層を構成する

Problem

問題

第58章の定値前層を、二つの互いに交わらない非空開集合を持つ空間上で考えます。大域定数は局所制限から一意に決まるため分離性を満たす一方、二領域に異なる値を置く整合族は貼り合わさらないことを示してください。一意性の証明と存在の反例を別々に書き、IsSeparatedFor と IsSheafFor の論理的な差へ翻訳します。局所定値関数の層へ置き換えると何が追加されるか説明できれば完了です。

ヒント

有界な連続関数を各開集合へ割り当て、非コンパクトな被覆で局所的に有界だが大域的に非有界な関数を貼ります。

解答

実数直線の開集合Uへ有界連続関数を割り当て、制限を通常の制限とします。二つの有界関数が被覆上で一致すれば点ごとに一致するので分離的です。一方U=Rを区間 (-n,n) で被覆し、各片に恒等関数x↦xを制限します。局所切断は有界で整合しますが、唯一の貼り合わせ候補x↦xはR上で非有界なので前層の大域切断ではありません。存在だけが失敗します。

層条件を「局所的性質が大域化するか」の検査として用い、局所性を持たない制約を発見します。

問題3層化の普遍性から一意性を導く

Problem

問題

層化射 η_P:P→i(aP) と層 Q への射 f:P→iQ を仮定します。随伴のhom全単射から射 f̄:aP→Q を構成し、η_P;f̄=f を示してください。同じ等式を満たす別の射が全単射の単射性により f̄ と等しいことを証明します。最後に、単に aP が層であるだけではこの一意性が得られない理由を述べ、層化の構成と普遍的特徴づけを区別できれば完了です。

ヒント

前層Fから層aFへの普遍射を二つ取り、互いへ一意に因子化します。

解答

層化 η:F→i(aF) は任意の層Gへの前層射 F→iG が一意に aF→G を経由するものです。二つの層化aF,bFがあれば、それぞれの普遍性で射 aF→bF と bF→aF を得ます。往復合成と恒等射はともに元のηを因子化するため一意性から一致し、標準同型になります。さらにηとの可換性を満たす同型は一意です。

反射部分圏への反射、局所化、完備化の一意性も同じ普遍射の往復で証明できます。

第61章

比較関手・モナド性・Beckの定理

問題1比較関手の代数法則を三角恒等式へ還元する

Problem

問題

K(Y) の作用を R(ε_Y):RLR(Y)→R(Y) と置き、単位法則と結合法則を展開してください。単位法則を随伴の三角恒等式へ、結合法則を余単位の自然性と関手の合成保存へ還元します。次に射 f:Y→Y' について R(f) が作用を保つ正方形を書き、余単位の自然性から証明してください。Leanの Monad.comparison の各フィールドと対応させ、モナド性を一度も仮定していないことを確認できれば完了です。

ヒント

随伴F⊣Gが誘導するT=GFについて、dをT代数 (Gd,Gε_d) へ送ります。

解答

単位則は Gη_{Gd}≫Gε_d=𝟙_{Gd} で、随伴の三角恒等式をGで読んだものです。結合則は GFGε_d≫Gε_d=Gε_{FGd}≫Gε_d と展開され、余単位εの自然性から従います。射h:d→d'についてG hが代数作用と可換することもεの自然性です。従って比較関手の定義義務は随伴のcoherenceへ還元されます。

抽象構造を比較圏へ送る際、どの法則が単位・余単位の自然性または三角恒等式に由来するか追跡します。

問題2三障害を具体例で分類する

Problem

問題

比較関手が忠実・完全・本質的全射であることの意味を、射の識別、代数準同型の復元、代数対象の復元としてそれぞれ説明してください。R が忠実なら K も忠実である証明を台射から与えます。一方、忠実性だけから完全性または本質的全射性が従うという誤った推論を特定し、それぞれに追加で何を構成すべきか述べてください。圏同値の判定条件へ三項を正しく対応させられれば完了です。

ヒント

比較関手Kについて、本質的全射性・充満性・忠実性の失敗を別々に述べます。

解答

本質的全射性の失敗は、T代数の中にDの対象から来ない「余分な解釈」があることです。充満性の失敗は、代数準同型が存在してもDの射へ持ち上がらないこと。忠実性の失敗は、異なるDの射がGで同じ射になり比較後に区別できないことです。例えばGが忠実でなければKも忠実になれません。三障害は対象・射の存在・射の区別という別の層なので、一つの反例で曖昧にまとめません。

圏同値を主張するときも、対象被覆・射の全射・射の単射を個別の証拠で担保します。

問題3Beckの仮定から擬逆の構成を追う

Problem

問題

T-代数 (A,a) に対する標準反射対 LTA⇉LA を書き、その共通切断を単位から構成してください。この対の余等化子を D で取り、得られる対象を比較関手の擬逆候補とします。R が余等化子を生成する仮定が対象の存在、射の持上げ、普遍性のどこで使われるかを区別してください。最後に保存・同型反映を使う別版と仮定を比較し、単に「余等化子がある」とだけ述べていないことを確認できれば完了です。

ヒント

T代数 (a:TX→X) から、自由代数間の反射対に対応するD内の余等化子を作ります。

解答

代数法則は自由代数 T²X⇉TX の二射 μ_X,T a をaが余等化することを述べます。Fで持ち上げた対応する反射対の D内余等化子を取り、その対象を擬逆L(X,a)とします。Gがこの余等化子を保存・反映する仮定により、比較後の代数は元の (X,a) と同型です。Dの対象dでは余単位が同じ余等化子を示し、L(Kd)≅dを得ます。選んだ余等化子の自然性と一意性からLの射作用を定めます。

モナド性定理を適用するときは定理名だけでなく、必要な余等化子の存在・保存・反映を具体的に検査します。

第62章

end・coend・双自然性

問題1自然変換をendの要素へ翻訳する

Problem

問題

関手 P,Q:J→Type と自然変換 α:P⇒Q を取り、族 j↦α_j を構成してください。hom双関手の反変作用を前合成、共変作用を後合成として展開し、end条件が P(f);α_j=α_i;Q(f) になることを示します。逆に endの要素から成分族と自然性証明を取り出して自然変換を作り、二構成が外延性により互いに逆であることを証明できれば完了です。

ヒント

Nat(F,G) を ∫_c Hom(Fc,Gc) とし、endのwedge条件を自然性へ展開します。

解答

endの要素は各cの射 η_c:Fc→Gc の族で、各 f:c→d に対し二つの作用が一致する条件を持ちます。hom双関手を展開すると Ff≫η_d=η_c≫Gf となり、自然変換の自然性そのものです。従って自然変換は対象ごとのhomの単なる積ではなく、射に沿う等化条件を課したendです。endの普遍性はこの整合族への写像を成分族として特徴づけます。

自然な操作の型をendで表すと、パラメトリックな成分族の整合条件を内部化できます。

問題2一対象圏で不変量と余不変量を比較する

Problem

問題

モノイド M を一対象圏とみなし、左作用と右作用を持つ集合から対応する双関手を作ってください。end条件が全ての m∈M に関して作用と可換する不変な要素を選ぶことを示します。coendでは二作用から生じる要素を同一視する商を記述してください。部分集合として残す操作と商集合へ送る操作の向きを比較し、endとcoendをどちらも単なる直積または直和とみなしていないことを確認できれば完了です。

ヒント

群Gの作用集合Xについて、endを固定点、coendを軌道集合として計算します。

解答

一対象群圏から集合への関手はG作用です。end型の不変量は全gで g·x=x を満たす固定点集合です。coend型の余不変量は関係 x∼g·x で商した軌道集合です。前者は作用で動かない要素を部分集合として残し、後者は作用で移り合う要素の区別を捨てます。極限と余極限、等化子と余等化子の差が一対象圏で具体化されます。

表現論の不変部分とcoinvariant quotientを、end/coendの双対的構成として比較します。

問題3co-Yoneda公式の商関係を検査する

Problem

問題

前層 P:Jᵒᵖ→Type と X:J に対し、対 ⟨p∈P(j),f:X→j⟩ を P(f)(p)∈P(X) へ送る関数を定めてください。射 g:j→k が生成するcoend関係の両辺が同じ値へ送られることを関手の合成保存から証明し、商からの関数を得ます。逆写像を x∈P(X) から ⟨x,id_X⟩ の同値類として作り、二つの逆法則を商の関係と恒等射保存によって示せれば完了です。

ヒント

coend ∫^c Hom(c,x)×F(c) の生成対 (f,u) を F(f)(u) へ送ります。

解答

coendの関係は h:c→d に対し (f∘h,u)∼(f,F(h)u) です。評価写像は両辺を関手の合成保存により同じ F(f)(F(h)u) へ送るのでwell-definedです。逆写像は v∈F(x) を (id_x,v) の類へ送ります。評価後はv、任意の (f,u) は関係により (id_x,F(f)u) と同じ類なので逆法則が成り立ちます。

coendを「添字付き和を作用の関係で商したもの」と読み、テンソル積やKan拡張の公式へ進みます。

第63章

Kan拡張——関手の普遍的な延長

問題1左右の普遍性を射の向きから再構成する

Problem

問題

L:C→D, F:C→H を固定し、左拡張候補と右拡張候補の対象・射を書き下してください。左側で η:F⇒L;E、右側で ε:L;E⇒F を選ぶ理由を、候補間の可換三角形から説明します。始対象と終対象の定義を適用して二つのhom全単射を導き、媒介変換の存在と一意性が全単射の逆法則になることを証明できれば完了です。

ヒント

K:C→D と F:C→E に対し、前合成 (-)∘K の左・右随伴として書きます。

解答

左Kan拡張Lan_K Fには単位 F→(Lan_K F)∘K があり、任意の F→G∘K が一意に Lan_K F→G を経由します。右Kan拡張Ran_K Fには余単位 (Ran_K F)∘K→F があり、任意の G∘K→F が一意に G→Ran_K F を経由します。左はFから外へ、右は外からFへ向く自然変換を分類します。記憶ではなく前合成関手との随伴のhom同型から復元できます。

自由延長と最良近似を使い分ける際、分類したい自然変換の向きを先に固定します。

問題2半順序の包含に沿う各点値を計算する

Problem

問題

半順序を、x≤y のときただ一つ射を持つ圏とみなします。部分半順序の包含 L:C→D と関手 F:C→H を取り、(L↓d) の対象が c≤d を満たす c、(d↓L) の対象が d≤c を満たす c に対応することを示してください。従って左拡張が下側の値の余極限、右拡張が上側の値の極限になることを導きます。該当する対象が空の場合も調べ、始対象と終対象のどちらが現れるかを説明できれば完了です。

ヒント

半順序を圏と見て、左Kan拡張は下側の値の上限、右Kan拡張は上側の値の下限になります。

解答

部分順序の包含 i:P↪Q と単調写像F:P→Lを考え、Lを完備格子とします。 (Lan_i F)(q)=sup{F(p)|i(p)≤q}、(Ran_i F)(q)=inf{F(p)|q≤i(p)} です。添字集合が空ならそれぞれ底と頂になります。 q=i(p₀)では単調性によりF(p₀)が対応する上限・下限と一致し、元の値を回収します。

抽象解釈の最良近似やデータ補間を、順序圏上のKan拡張として捉えられます。

問題3各点公式から射作用を構成する

Problem

問題

射 k:d→d' が (c,f:Lc→d) を (c,f;k:Lc→d') へ送る関手を定めることを確認してください。これを F と合成した二つの図式を比較し、余極限の標準射から (Lan_L F)(d)→(Lan_L F)(d') を構成します。恒等射と合成に対して得られる二射が一致することを余極限の射の外延性で証明してください。右Kan拡張について双対の構成を行い、どの矢印が反転するかを全て記述できれば完了です。

ヒント

(Lan_K F)(d)=colim_{(K↓d)}F∘π とし、射u:d→d'がコンマ圏間に誘導する関手を使います。

解答

対象 (c,Kc→d) をuとの合成で (c,Kc→d') へ送る関手 u_*:(K↓d)→(K↓d') を得ます。d'側余極限錐をu_*で引き戻すとd側図式からd'側頂点への余錐になるので、d側余極限の普遍性から Lan F(u):Lan F(d)→Lan F(d') が一意に得られます。恒等・合成保存は、誘導関手の恒等・合成と媒介射の一意性から従います。

対象ごとの公式を提示するときは、射作用と関手法則まで普遍性から構成して初めて関手になります。

問題4coend公式の生成関係をコンマ圏と照合する

Problem

問題

集合値関手 F:C→Type に対し、従属和 Σ c, Hom_D(Lc,d)×F(c) を考えます。射 g:c→c' が生む二つの代表 (f∘L(g),x) と (f,F(g)(x)) を同一視し、その商からコンマ圏上の余極限への写像を定めてください。逆写像を余極限の普遍性から構成し、生成関係がまさにコンマ圏の射に沿う余錐条件であることを示します。これにより左Kan拡張のcoend公式を、単なる記号変形ではなく商の普遍性として説明できれば完了です。

ヒント

Lan_K F(d)=∫^c Hom(Kc,d)⊙F(c) の対 (f,x) と、コンマ対象 (c,f) を対応させます。

解答

coendの生成元は f:Kc→d と x∈F(c) の対で、まさにコンマ圏対象(c,f)における要素です。射h:c→c'に対する関係 (f∘Kh,x)∼(f,Fh(x)) は、コンマ圏の射に沿って余極限の脚が可換するという同一視です。従ってコンマ圏余極限と coend商は同じ生成元と関係を持ちます。copowerは集合の各要素ぶんF(c)のコピーを用意します。

密度公式やプロ関手合成でも、coendの商関係を図式の射による同一視として読めます。

第64章

モノイダル圏——テンソル積と整合性

問題1`Type` の五角形を要素ごとに証明する

Problem

問題

四つの型 A,B,C,D と要素 a,b,c,d を固定し、(((a,b),c),d) から a,(b,(c,d)) へ至る五角形の二経路を関数として書いてください。各結合子の適用後の要素を一段ずつ記録し、両経路が同じ入れ子対へ到達することを示します。Leanでは関数外延性を使う証明と MonoidalCategory.pentagon を使う証明を比較し、具体計算と抽象公理の役割を区別できれば完了です。

ヒント

四重積の要素 (((a,b),c),d) を二つの結合子経路で a,(b,(c,d)) へ送ります。

解答

直積をテンソルとし、結合子を ((a,b),c)↦(a,(b,c)) とします。五角形の上経路は四重積を三回再括弧付けし、下経路は外側と内側を二段で再括弧付けします。どちらも要素 (((a,b),c),d) を (a,(b,(c,d))) へ送ります。関数外延性により射が等しく、五角形が可換します。結合子が存在するだけでなく、異なる再括弧付けが一致するcoherenceが必要です。

構造同型を自動で省略する前に、基本的な整合図式がどの具体計算を保証するか確認します。

Lean検査済みL422–443

open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open scoped MonoidalCategory

universe u

def pentagonUpper {W X Y Z : Type u} : (((W × X) × Y) × Z) → W × (X × (Y × Z)) :=
  fun value ↦ (value.1.1.1, (value.1.1.2, (value.1.2, value.2)))

def pentagonLower {W X Y Z : Type u} : (((W × X) × Y) × Z) → W × (X × (Y × Z)) :=
  fun value ↦ (value.1.1.1, (value.1.1.2, (value.1.2, value.2)))

theorem typePentagonElementwise {W X Y Z : Type u} :
    pentagonUpper (W := W) (X := X) (Y := Y) (Z := Z) = pentagonLower := by
  funext value
  rcases value with ⟨⟨⟨w, x⟩, y⟩, z⟩
  rfl

example (W X Y Z : Type u) :
    (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom :=
  MonoidalCategory.pentagon W X Y Z

問題2単位対象と終対象の違いを説明する

Problem

問題

体 k 上のベクトル空間と線形写像の圏を考え、テンソル単位が k、零対象が零ベクトル空間であることを確認してください。k→V という線形写像が V のベクトルの選択に対応して一般には一意でないことから、k が終対象でないことを示します。I⊗V≅V と「全ての対象から I への射が一意」を明確に分離できれば完了です。

ヒント

ベクトル空間のテンソル単位は基礎体ですが、終対象は零ベクトル空間です。

解答

モノイダル単位Iは I⊗X≅X≅X⊗I を満たす対象で、任意対象からの一意な射を要求しません。ベクトル空間ではI=k、終対象は0です。デカルトモノイダル圏ではテンソルが積なので単位は零項積である終対象になりますが、これは特殊事情です。単位対象を終対象と誤認すると、線形なテンソルに存在しない捨てる射 X→I を仮定してしまいます。

資源意味論では単位と終対象の分離が、値を捨てられるかどうかを表します。

問題3対象対応だけではモノイダル構造にならない理由を示す

Problem

問題

圏 C 上に二項対象対応 T:C×C→C の対象部分だけが与えられたと仮定します。結合子の自然性を書くために必要な四つの射作用を列挙し、T(f,g) がなければ可換正方形の辺さえ定義できないことを示してください。さらに射作用を与えても恒等・合成保存がなければ、五角形を射の合成として安定に移送できないことを説明します。

ヒント

モノイダル関手には対象写像に加え、テンソルと単位を比較する自然変換と整合性が必要です。

解答

関手Fが対象ごとに F(X⊗Y) と FX⊗FY を同型な対象へ送っても、同型の選択が射に自然とは限りません。強モノイダル関手には φ_{X,Y}:FX⊗FY≅F(X⊗Y) と φ₀:I_D≅F I_C、さらに結合子・左右単位子と可換する図式が必要です。対象の同型類だけではテンソルされた射の作用や異なる括弧付けとの整合性を決められません。

構造保存関手を設計するとき、厳密・強・lax・oplaxの比較射の向きを明記します。

問題4整合性定理の適用範囲を判定する

Problem

問題

結合子と単位子だけからなる等式、任意の射 f を単位子へ通す自然性の等式、モノイド対象の乗法 μ を含む結合律の三例を用意してください。どれが純粋な整合性だけで従い、どれが自然性またはモノイド対象の公理を必要とするかを分類します。それぞれをLeanで monoidal_coherence, simp, 明示した仮定のいずれかを使って証明し、自動化が数学的仮定を追加していないことを説明できれば完了です。

ヒント

結合子と単位子だけから作る標準射と、組紐や任意の射を含む図式を区別します。

解答

Mac Laneの整合性定理は、同じテンソル語の異なる括弧付け・単位挿入の間で結合子と単位子から作られる標準射が一意であることを保証します。従ってその範囲では括弧を安全に省略できます。組紐を含む場合は組紐付き整合性、対称性を含む場合は対称モノイダル整合性が別途必要です。任意の射や追加構造を含む図式が自動的に可換になるわけではありません。

形式化でsimpへ整合性を委ねる際も、どの正規化定理が背後で使われるかを把握します。

Lean検査済みL449–469

open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open scoped MonoidalCategory

universe u v

variable {C : Type u} [Category.{v} C] [MonoidalCategory C]

example (W X Y Z : C) :
    (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom :=
  MonoidalCategory.pentagon W X Y Z

example (X Y : C) :
    (α_ X (𝟙_ C) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y :=
  MonoidalCategory.triangle X Y

example {W W' X X' Y Y' : C} (f₁ : W ⟶ W') (f₂ : W' ⟶ X)
    (g₁ : Y ⟶ Y') (g₂ : Y' ⟶ X') :
    (f₁ ⊗ₘ g₁) ≫ (f₂ ⊗ₘ g₂) = (f₁ ≫ f₂) ⊗ₘ (g₁ ≫ g₂) :=
  MonoidalCategory.tensorHom_comp_tensorHom f₁ g₁ f₂ g₂

第65章

豊穣圏——hom集合を構造ある対象へ置き換える

問題1`Type`-豊穣圏の三法則を通常の圏法則へ戻す

Problem

問題

V=Type とし、テンソル積を直積、単位を PUnit としてください。eId を PUnit の唯一の要素で評価して恒等射を取り出し、eComp を対 (f,g) で評価して合成を定義します。豊穣化された左右単位律と結合律を関数の点ごとの等式として評価し、通常の id_comp, comp_id, assoc が得られることを示せば完了です。

ヒント

hom対象を型、合成射を関数、単位射 Unit→Hom(X,X) を恒等射の選択として展開します。

解答

Typeの直積モノイダル構造で、豊穣合成は Hom(Y,Z)×Hom(X,Y)→Hom(X,Z)、単位はUnitからHom(X,X)への写像です。結合図式を要素 (h,g,f) に適用すると (f≫g)≫h=f≫(g≫h)。左右単位図式は恒等射との合成律になります。従ってType-豊穣圏は通常の局所小圏と同じデータ・法則を回収します。

別の基底Vへ移ると、要素による説明をV内の射と図式へ置き換える必要があります。

問題2前順序を真理値豊穣化として構成する

Problem

問題

対象の型 P と二項関係 R:P→P→Prop を取り、hom対象を命題 R x y としてください。テンソル単位から R x x への射が反射性に、R x y∧R y z から R x z への射が推移性に対応することを示します。逆に反射的・推移的な関係から豊穣構造を構成し、反対称性が豊穣圏の法則には含まれないことを説明できれば完了です。

ヒント

基底を二値束 {false≤true}、テンソルを論理積とし、hom値を x≤y の真理値にします。

解答

各対(x,y)へ真理値 [x≤y] を割り当てます。単位射はtrue≤[x≤x]、すなわち反射性です。合成射 [y≤z]∧[x≤y]≤[x≤z] は推移性です。hom対象が高々一つの証拠しか区別しないため、得られるのは前順序です。反対称性は豊穣圏法則ではなく、同型な対象を等しいとする分離条件に対応します。

束値・量化された真理値を基底にすると、段階付き関係やファジィ順序へ一般化できます。

問題3Lawvere距離の向きを三角不等式から決定する

Problem

問題

非負拡大実数に通常と逆の順序を入れ、射 a→b を通常の順序で a≥b が成り立つこととします。テンソルを加法、単位を零として、恒等の一般化要素と合成射の存在条件を書いてください。それぞれが d(x,x)=0 の弱い形と三角不等式へ対応することを示し、なぜ順序を反転しないと不等号の向きが合わないか説明します。

ヒント

基底 [0,∞] の順序を通常と逆にし、テンソルを加法とします。

解答

豊穣合成は基底順序で d(y,z)+d(x,y)≤_V d(x,z) です。≤_V は通常の≥なので、通常順序では d(x,z)≤d(x,y)+d(y,z) となり三角不等式です。単位条件 0≤_V d(x,x) は通常順序で d(x,x)≤0、非負性と合わせて 0になります。順序を反転しないと不等式の向きが逆になり、距離の合成解釈を失います。

非対称距離や無限距離も許すことで、到達コスト・計算資源・類似度を豊穣圏として扱えます。

問題4自然変換型とhom対象の存在を分離する

Problem

問題

二つの V-豊穣関手 F,G について、成分族 I→Hom(FX,GX) と自然性条件から豊穣自然変換の型を定義してください。次に、その型を Hom_V(I,N) として表現する対象 N を得るには何が必要かを調べます。hom対象のend 公式を書き、必要な積・等化子・サイズ条件を列挙してください。成分族が型として定義できるだけでは N の存在を証明しないことを、Leanの EnrichedNatTrans と enrichedNatTransYoneda の型を比較して説明できれば完了です。