import FormalLab.CategoryTheory.MonoidalCategories import FormalLab.CategoryTheory.Presheaves /-! # 全問題の解答：前層・層・圏論的拡張 ## 第58章：前層――局所データを制限する反変関手 ### 問題1：制限の合成則を二つの記法で導く #### ヒント 前層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により元の圏の 射順が反転します。二記法を対応させると、制限を二回行う領域の順序を誤りにくくなります。 座標変換、環の局所化、文脈への再添字付けも同じ反変合成則で追跡できます。 ### 問題2：対象ごとの写像を自然変換へ昇格する #### ヒント `η_U:P(U)→Q(U)` がすべての制限写像と可換する条件を書きます。 #### 解答 各Uの写像η_Uに対し、`f:V⟶U` について `Q(f)(η_U s)=η_V(P(f)s)` が必要です。左辺は変換後に制限し、右辺は制限後に 変換します。この式が全f,sで成り立てばηは前層間の自然変換です。例えば連続関数を値ごとに二乗する操作は制限と可換し、 「定義域全体で積分する」操作は一般に制限と可換しないため前層射になりません。 局所的なデータ変換をAPI化するとき、領域縮小との可換性を合成可能性の条件にします。 ### 問題3：定値前層が層にならない状況を分析する #### ヒント 非連結な開集合を二つの互いに素な開集合で被覆し、異なる定数を各成分に置きます。 #### 解答 集合Aをすべての非空開集合へ割り当て、制限を恒等とする定値前層を考えます。`U=U₁⊔U₂` が非連結なら、U₁にa、 U₂にb≠aを置いた局所切断は交わりが空なので整合します。しかしU上の定値切断は一つの値しか取れず、両方へ貼り合いません。 従ってAが一要素でない限り層条件に失敗します。局所定値関数の層は成分ごとに値を選べるため、この欠陥を修正します。 層条件は局所的一致だけでなく、位相の連結性に応じた大域データの柔軟性も要求します。 ## 第59章：篩・Grothendieck位相・サイト ### 問題1：主篩の普遍性を証明する #### ヒント 射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：引戻し公理の合成安定性を証明する #### ヒント 篩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：三公理から上方閉性を導く #### ヒント 被覆篩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：整合族と貼り合わせを定義から判定する #### ヒント 被覆 `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：分離的だが層でない前層を構成する #### ヒント 有界な連続関数を各開集合へ割り当て、非コンパクトな被覆で局所的に有界だが大域的に非有界な関数を貼ります。 #### 解答 実数直線の開集合Uへ有界連続関数を割り当て、制限を通常の制限とします。二つの有界関数が被覆上で一致すれば点ごとに 一致するので分離的です。一方U=Rを区間 `(-n,n)` で被覆し、各片に恒等関数x↦xを制限します。局所切断は有界で 整合しますが、唯一の貼り合わせ候補x↦xはR上で非有界なので前層の大域切断ではありません。存在だけが失敗します。 層条件を「局所的性質が大域化するか」の検査として用い、局所性を持たない制約を発見します。 ### 問題3：層化の普遍性から一意性を導く #### ヒント 前層Fから層aFへの普遍射を二つ取り、互いへ一意に因子化します。 #### 解答 層化 `η:F→i(aF)` は任意の層Gへの前層射 `F→iG` が一意に `aF→G` を経由するものです。二つの層化aF,bFがあれば、 それぞれの普遍性で射 `aF→bF` と `bF→aF` を得ます。往復合成と恒等射はともに元のηを因子化するため一意性から 一致し、標準同型になります。さらにηとの可換性を満たす同型は一意です。 反射部分圏への反射、局所化、完備化の一意性も同じ普遍射の往復で証明できます。 ## 第61章：比較関手・モナド性・Beckの定理 ### 問題1：比較関手の代数法則を三角恒等式へ還元する #### ヒント 随伴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：三障害を具体例で分類する #### ヒント 比較関手Kについて、本質的全射性・充満性・忠実性の失敗を別々に述べます。 #### 解答 本質的全射性の失敗は、T代数の中にDの対象から来ない「余分な解釈」があることです。充満性の失敗は、代数準同型が 存在してもDの射へ持ち上がらないこと。忠実性の失敗は、異なるDの射がGで同じ射になり比較後に区別できないことです。 例えばGが忠実でなければKも忠実になれません。三障害は対象・射の存在・射の区別という別の層なので、一つの反例で 曖昧にまとめません。 圏同値を主張するときも、対象被覆・射の全射・射の単射を個別の証拠で担保します。 ### 問題3：Beckの仮定から擬逆の構成を追う #### ヒント 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の要素へ翻訳する #### ヒント `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：一対象圏で不変量と余不変量を比較する #### ヒント 群Gの作用集合Xについて、endを固定点、coendを軌道集合として計算します。 #### 解答 一対象群圏から集合への関手はG作用です。end型の不変量は全gで `g·x=x` を満たす固定点集合です。coend型の余不変量は 関係 `x∼g·x` で商した軌道集合です。前者は作用で動かない要素を部分集合として残し、後者は作用で移り合う要素の 区別を捨てます。極限と余極限、等化子と余等化子の差が一対象圏で具体化されます。 表現論の不変部分とcoinvariant quotientを、end/coendの双対的構成として比較します。 ### 問題3：co-Yoneda公式の商関係を検査する #### ヒント 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：左右の普遍性を射の向きから再構成する #### ヒント `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：半順序の包含に沿う各点値を計算する #### ヒント 半順序を圏と見て、左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：各点公式から射作用を構成する #### ヒント `(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')` が一意に得られます。恒等・合成保存は、誘導関手の恒等・合成と媒介射の一意性から従います。 対象ごとの公式を提示するときは、射作用と関手法則まで普遍性から構成して初めて関手になります。 ### 問題4：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` の五角形を要素ごとに証明する #### ヒント 四重積の要素 `(((a,b),c),d)` を二つの結合子経路で `a,(b,(c,d))` へ送ります。 #### 解答 直積をテンソルとし、結合子を `((a,b),c)↦(a,(b,c))` とします。五角形の上経路は四重積を三回再括弧付けし、下経路は 外側と内側を二段で再括弧付けします。どちらも要素 `(((a,b),c),d)` を `(a,(b,(c,d)))` へ送ります。関数外延性により 射が等しく、五角形が可換します。結合子が存在するだけでなく、異なる再括弧付けが一致するcoherenceが必要です。 構造同型を自動で省略する前に、基本的な整合図式がどの具体計算を保証するか確認します。 ### 問題2：単位対象と終対象の違いを説明する #### ヒント ベクトル空間のテンソル単位は基礎体ですが、終対象は零ベクトル空間です。 #### 解答 モノイダル単位Iは `I⊗X≅X≅X⊗I` を満たす対象で、任意対象からの一意な射を要求しません。ベクトル空間ではI=k、 終対象は0です。デカルトモノイダル圏ではテンソルが積なので単位は零項積である終対象になりますが、これは特殊事情です。 単位対象を終対象と誤認すると、線形なテンソルに存在しない捨てる射 `X→I` を仮定してしまいます。 資源意味論では単位と終対象の分離が、値を捨てられるかどうかを表します。 ### 問題3：対象対応だけではモノイダル構造にならない理由を示す #### ヒント モノイダル関手には対象写像に加え、テンソルと単位を比較する自然変換と整合性が必要です。 #### 解答 関手Fが対象ごとに `F(X⊗Y)` と `FX⊗FY` を同型な対象へ送っても、同型の選択が射に自然とは限りません。強モノイダル 関手には `φ_{X,Y}:FX⊗FY≅F(X⊗Y)` と `φ₀:I_D≅F I_C`、さらに結合子・左右単位子と可換する図式が必要です。 対象の同型類だけではテンソルされた射の作用や異なる括弧付けとの整合性を決められません。 構造保存関手を設計するとき、厳密・強・lax・oplaxの比較射の向きを明記します。 ### 問題4：整合性定理の適用範囲を判定する #### ヒント 結合子と単位子だけから作る標準射と、組紐や任意の射を含む図式を区別します。 #### 解答 Mac Laneの整合性定理は、同じテンソル語の異なる括弧付け・単位挿入の間で結合子と単位子から作られる標準射が一意で あることを保証します。従ってその範囲では括弧を安全に省略できます。組紐を含む場合は組紐付き整合性、対称性を含む場合は 対称モノイダル整合性が別途必要です。任意の射や追加構造を含む図式が自動的に可換になるわけではありません。 形式化でsimpへ整合性を委ねる際も、どの正規化定理が背後で使われるかを把握します。 ## 第65章：豊穣圏——hom集合を構造ある対象へ置き換える ### 問題1：`Type`-豊穣圏の三法則を通常の圏法則へ戻す #### ヒント 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：前順序を真理値豊穣化として構成する #### ヒント 基底を二値束 `{false≤true}`、テンソルを論理積とし、hom値を `x≤y` の真理値にします。 #### 解答 各対(x,y)へ真理値 `[x≤y]` を割り当てます。単位射はtrue≤[x≤x]、すなわち反射性です。合成射 `[y≤z]∧[x≤y]≤[x≤z]` は推移性です。hom対象が高々一つの証拠しか区別しないため、得られるのは前順序です。 反対称性は豊穣圏法則ではなく、同型な対象を等しいとする分離条件に対応します。 束値・量化された真理値を基底にすると、段階付き関係やファジィ順序へ一般化できます。 ### 問題3：Lawvere距離の向きを三角不等式から決定する #### ヒント 基底 `[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対象の存在を分離する #### ヒント V-自然変換を外部の族として定義できることと、関手圏のhom対象をV内のendで作れることを区別します。 #### 解答 V-関手F,G間の自然変換は各Xの成分 `I→D(FX,GX)` と自然性図式として述べられます。しかし関手圏をV-豊穣圏にする hom対象 `∫_X D(FX,GX)` の存在には、Vが必要なendを持つことが要ります。成分族の集合が外部的に定義できても、 それを表すV内対象が存在するとは限りません。サイズ条件もendの存在に影響します。 内部homや豊穣関手圏を主張するときは、基底の完備性・閉性・宇宙条件を明示します。 -/ namespace FormalLab.Appendix.Solutions.Chapter058Exercise001 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 end FormalLab.Appendix.Solutions.Chapter058Exercise001 namespace FormalLab.Appendix.Solutions.Chapter064Exercise001 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 end FormalLab.Appendix.Solutions.Chapter064Exercise001 namespace FormalLab.Appendix.Solutions.Chapter064Exercise004 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₂ end FormalLab.Appendix.Solutions.Chapter064Exercise004