import Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
import FormalLab.CategoryTheory.Adjunctions
import FormalLab.CategoryTheory.Limits

/-!
# 第63章：Kan拡張——関手の普遍的な延長

関手 `F:C→H` の定義域を、関手 `L:C→D` に沿って `D` へ広げたいとします。対象 `d:D` が
`L(c)` の像でないとき、`F` だけから `d` での値を一意に指定することはできません。それでも、候補となる
全ての延長を自然変換で比較し、その中で普遍なものを選ぶことはできます。この選択がKan拡張です。

左Kan拡張は `L(c)→d` という射を通じて `F(c)` の情報を `d` へ集めるので、各点では余極限になります。
右Kan拡張は `d→L(c)` という射を通じて互換な情報を要求するので、各点では極限になります。本章ではまず
自然変換の普遍性として左右のKan拡張を定義し、次に前合成関手の左右随伴としてまとめます。最後にコンマ圏を
使う各点公式を導き、単なる対象ごとの選択が関手にならない理由を明らかにします。

## 延長候補には比較射が必要である

圏 `C,D,H`、関手

$$
L:\mathcal C\longrightarrow\mathcal D,
\qquad F:\mathcal C\longrightarrow\mathcal H.
$$

を固定します。`D→H` という型を持つ関手 `E` だけでは、`F` の延長であるとはいえません。`E` を `L` で
前合成した関手 `E∘L:C→H` と `F` を比較する自然変換が必要です。比較射には二つの向きがあります。

$$
\text{左候補: }\eta:F\Rightarrow E\circ L,
\qquad
\text{右候補: }\varepsilon:E\circ L\Rightarrow F.
$$

等号 `E∘L=F` を要求しない点が重要です。自由化、局所化、包含に沿う拡張では、像の上でも標準的な比較射は
同型とは限りません。Kan拡張は、比較射の向きを保ったまま候補全体を普遍性で比較します。
-/

namespace FormalLab.CategoryFoundations.KanExtensions

open _root_.CategoryTheory
open _root_.CategoryTheory.Functor
open _root_.CategoryTheory.Limits

noncomputable section

universe vH vD vC uH uD uC

variable {C : Type uC} [Category.{vC} C]
variable {D : Type uD} [Category.{vD} D]
variable {H : Type uH} [Category.{vH} H]
variable (L : C ⥤ D) (F : C ⥤ H)

example : (D ⥤ H) ⥤ (C ⥤ H) := (whiskeringLeft C D H).obj L

example (E : D ⥤ H) : ((whiskeringLeft C D H).obj L).obj E = L ⋙ E := rfl

/-!
Leanの `L ⋙ E` は、まず `L`、次に `E` を適用する図式順の合成です。通常の関数合成記号なら `E∘L` に
当たります。前合成は対象だけでなく自然変換も成分ごとに `L(c)` で評価し、関手圏の間の関手になります。

## 左Kan拡張は延長候補の始対象である

自然変換 `η:F⇒L;E` を持つ候補 `(E,η)` を考えます。左Kan拡張 `Lan_L F` は、任意の候補
`(G,β)` に対して一意な自然変換 `γ:Lan_L F⇒G` があり、次を満たすものです。

$$
\eta;(L\mathbin{;}\gamma)=\beta:
F\Rightarrow L\mathbin{;}G.
$$

すなわち `η ; (L;γ)=β` です。候補と可換な比較射からなる圏では、左Kan拡張は始対象です。「左」という語は
射が左向きという意味ではなく、後で見るように前合成関手の左随伴になることを表します。
-/

variable {L F}
variable {E : D ⥤ H} (η : F ⟶ L ⋙ E)

example : Prop := E.IsLeftKanExtension η

variable [E.IsLeftKanExtension η]

example (G : D ⥤ H) (β : F ⟶ L ⋙ G) : E ⟶ G :=
  E.descOfIsLeftKanExtension η G β

example (G : D ⥤ H) (β : F ⟶ L ⋙ G) :
    η ≫ whiskerLeft L (E.descOfIsLeftKanExtension η G β) = β :=
  E.descOfIsLeftKanExtension_fac η G β

example (G : D ⥤ H) : (E ⟶ G) ≃ (F ⟶ L ⋙ G) :=
  E.homEquivOfIsLeftKanExtension η G

/-!
最後の全単射は普遍性を圧縮した形です。左辺の `γ` は右辺の `η;(L;γ)` へ送られ、逆写像は普遍性による
一意な媒介変換です。したがって左Kan拡張は、対象ごとの近似ではなく、全ての関手 `G:D→H` に対する
自然変換を同時に分類します。

`IsLeftKanExtension` は `Prop` です。普遍であることの証明をデータとして何通りも区別するのではなく、候補
`E` と比較射 `η` が条件を満たすかを記録します。実際の媒介変換は普遍性から選ばれるため、一般には
`noncomputable` です。

## 右Kan拡張は延長候補の終対象である

右Kan拡張 `Ran_L F` は向きを全て反転します。比較射は `ε:L;Ran_L F⇒F` で、任意の候補
`β:L;G⇒F` から一意な `γ:G⇒Ran_L F` が存在します。

$$
(L\mathbin{;}\gamma);\varepsilon=\beta:
L\mathbin{;}G\Rightarrow F.
$$

式では `(L;γ);ε=β` です。右拡張候補の圏でこれは終対象になります。
-/

variable {R : D ⥤ H} (ε : L ⋙ R ⟶ F)

example : Prop := R.IsRightKanExtension ε

variable [R.IsRightKanExtension ε]

example (G : D ⥤ H) (β : L ⋙ G ⟶ F) : G ⟶ R :=
  R.liftOfIsRightKanExtension ε G β

example (G : D ⥤ H) (β : L ⋙ G ⟶ F) :
    whiskerLeft L (R.liftOfIsRightKanExtension ε G β) ≫ ε = β :=
  R.liftOfIsRightKanExtension_fac ε G β

example (G : D ⥤ H) : (G ⟶ R) ≃ (L ⋙ G ⟶ F) :=
  R.homEquivOfIsRightKanExtension ε G

/-!
左拡張では普遍対象から出る射を `desc`、右拡張では普遍対象へ入る射を `lift` と呼びます。この違いは
余極限の `desc` と極限の `lift` と同じ向きです。二つの定義を別々に暗記せず、始対象と終対象の双対として
復元できます。

## 存在と選ばれたKan拡張を区別する

`HasLeftKanExtension L F` は左拡張候補の圏に始対象が存在するという命題、`HasRightKanExtension L F` は
右拡張候補の圏に終対象が存在するという命題です。存在を仮定すると、mathlibは一つの代表を選び、その比較
自然変換を同時に提供します。
-/

variable (L F)

example : Prop := L.HasLeftKanExtension F
example : Prop := L.HasRightKanExtension F

variable [L.HasLeftKanExtension F] [L.HasRightKanExtension F]

example : D ⥤ H := L.leftKanExtension F
example : F ⟶ L ⋙ L.leftKanExtension F := L.leftKanExtensionUnit F

example : D ⥤ H := L.rightKanExtension F
example : L ⋙ L.rightKanExtension F ⟶ F := L.rightKanExtensionCounit F

/-!
普遍対象は通常、等号ではなく一意な自然同型まで定まります。従って選ばれた代表の内部表現に依存した計算を
期待せず、単位・余単位と媒介変換の計算則を使います。`HasLeftKanExtension` と
`HasRightKanExtension` は互いを含意しません。値圏が必要な余極限だけを持つ場合は左拡張だけが、必要な
極限だけを持つ場合は右拡張だけが存在し得ます。

## 全ての関手を拡張すると随伴になる

`F:C→H` ごとに左Kan拡張が存在するなら、それらは関手

$$
\operatorname{Lan}_L:[\mathcal C,\mathcal H]
\longrightarrow[\mathcal D,\mathcal H].
$$

にまとまります。自然変換 `F⇒F'` の像は、左Kan拡張の普遍性によって一意に定まります。前合成関手を
`L*:[D,H]→[C,H]` と書けば、普遍性の全単射は

$$
\operatorname{Nat}(\operatorname{Lan}_L F,G)
\cong\operatorname{Nat}(F,L^*G).
$$

なので `Lan_L ⊣ L*` です。同様に右Kan拡張は `L* ⊣ Ran_L` を与えます。個々のKan拡張は一つの
普遍対象であり、Kan拡張関手はそれらを全ての `F` について整合的に選んだものです。
-/

section ExtensionAdjunctions

variable [∀ (G : C ⥤ H), L.HasLeftKanExtension G]

example : (C ⥤ H) ⥤ (D ⥤ H) := L.lan

example : L.lan ⊣ (whiskeringLeft C D H).obj L := L.lanAdjunction H

example (G : C ⥤ H) (K : D ⥤ H) :
    (L.lan.obj G ⟶ K) ≃ (G ⟶ L ⋙ K) :=
  (L.lanAdjunction H).homEquiv G K

end ExtensionAdjunctions

section CoextensionAdjunctions

variable [∀ (G : C ⥤ H), L.HasRightKanExtension G]

example : (C ⥤ H) ⥤ (D ⥤ H) := L.ran

example : (whiskeringLeft C D H).obj L ⊣ L.ran := L.ranAdjunction H

example (K : D ⥤ H) (G : C ⥤ H) :
    (L ⋙ K ⟶ G) ≃ (K ⟶ L.ran.obj G) :=
  (L.ranAdjunction H).homEquiv K G

end CoextensionAdjunctions

/-!
この随伴による特徴づけは、Kan拡張が「可能な限り自由な延長」または「可能な限り整合的な延長」であることを
正確にします。左拡張は指定された比較射から他の候補への射を生成し、右拡張は他の候補から指定された比較射へ
射を受け取ります。

## 左Kan拡張の各点公式

対象 `d:D` を固定します。コンマ圏 `(L↓d)` の対象は組

$$
(c,f:L(c)\to d).
$$

であり、射は三角形を可換にする `C` の射です。射 `f` は `F(c)` の情報を拡張先の `d` へ運ぶ経路を表します。
射影 `(L↓d)→C` の後に `F` を合成した図式の余極限を取ると

$$
(\operatorname{Lan}_L F)(d)
\cong\operatorname*{colim}_{(c,Lc\to d)\in(L\downarrow d)}F(c).
$$

を得ます。余極限は全ての経路から来る情報を集め、コンマ圏の射が表す整合関係を課します。
-/

example (d : D) : Type _ := CostructuredArrow L d

example (d : D) : CostructuredArrow L d ⥤ H :=
  CostructuredArrow.proj L d ⋙ F

example (d : D) : Prop := L.HasPointwiseLeftKanExtensionAt F d

section PointwiseLeft

variable [L.HasPointwiseLeftKanExtension F]

example (d : D) :
    (L.leftKanExtension F).obj d ≅
      colimit (CostructuredArrow.proj L d ⋙ F) :=
  L.leftKanExtensionObjIsoColimit F d

end PointwiseLeft

/-!
例えば `C` が `D` の部分圏で `L` が包含関手なら、`d` へ射を持つ既知の対象 `c` を全て集め、それらの
`F(c)` を貼り合わせた値が左Kan拡張です。ある `d` へ至る射が一つもなければコンマ圏は空です。この場合の
余極限は値圏の始対象なので、左拡張の存在には少なくとも該当する空余極限が必要です。

## 右Kan拡張の各点公式

右側ではコンマ圏 `(d↓L)` を使います。その対象は

$$
(c,f:d\to L(c)).
$$

で、各 `F(c)` への観測がコンマ圏の射に沿って整合することを要求します。従って

$$
(\operatorname{Ran}_L F)(d)
\cong\operatorname*{lim}_{(c,d\to Lc)\in(d\downarrow L)}F(c).
$$

です。左公式では余極限、`Lc→d`、始対象が現れます。右公式ではそれぞれ極限、`d→Lc`、終対象へ反転します。
-/

example (d : D) : Type _ := StructuredArrow d L

example (d : D) : StructuredArrow d L ⥤ H :=
  StructuredArrow.proj d L ⋙ F

example (d : D) : Prop := L.HasPointwiseRightKanExtensionAt F d

section PointwiseRight

variable [L.HasPointwiseRightKanExtension F]

example (d : D) :
    (L.rightKanExtension F).obj d ≅
      limit (StructuredArrow.proj d L ⋙ F) :=
  RightExtension.IsPointwiseRightKanExtensionAt.isoLimit
    (isPointwiseRightKanExtensionOfIsRightKanExtension
      (L.rightKanExtension F) (L.rightKanExtensionCounit F) d)

end PointwiseRight

/-!
`d` から像 `L(c)` へ射が一つもなければ、右公式は空図式の極限、すなわち終対象になります。この境界例は
左と右の向きを確認する簡潔な方法です。左拡張で空コンマ圏から終対象が出る、または右拡張から始対象が出る
と考えたなら、極限と余極限の向きを取り違えています。

## 対象ごとの公式から関手性が生じる

各 `d` について余極限または極限を独立に選んだだけでは、まだ `D→H` は得られません。射 `k:d→d'` は
左側のコンマ圏の間に関手 `(L↓d)→(L↓d')` を誘導し、余極限の普遍性から
`(Lan_L F)(d)→(Lan_L F)(d')` を生みます。右側では射が誘導する図式間の比較と極限の普遍性から
`(Ran_L F)(d)→(Ran_L F)(d')` を得ます。

恒等射保存と合成保存は、選んだ媒介射の一意性から従います。これが「各点で値を計算できる」ことと
「それらの値が関手をなす」ことの間にある論理的な段差です。mathlibの点ごとのKan拡張は、この段差を
コンマ圏の図式と普遍錐・普遍余錐によって埋めます。

## 通常のKan拡張と各点Kan拡張

通常のKan拡張は関手圏内の始対象または終対象として定義されます。各点Kan拡張は、全ての `d:D` で上の
コンマ圏公式が普遍錐または普遍余錐になることを要求します。各点性から通常の普遍性は導けますが、任意の
2-圏的状況で通常の普遍性だけから各点性が自動的に従うわけではありません。本章の `HasPointwise...` は、
値圏 `H` に必要な形の極限・余極限が存在するという、より計算可能な十分条件を明示します。

## end・coendによる計算法との関係

値圏に集合の冪やテンソルに相当する構造があると、各点公式はhomを重みとするcoendまたはendでも表せます。
集合値の場合の概略は

$$
\begin{aligned}
(\operatorname{Lan}_L F)(d)
  &\cong\int^c\operatorname{Hom}_{\mathcal D}(Lc,d)\times F(c),\\
(\operatorname{Ran}_L F)(d)
  &\cong\int_c F(c)^{\operatorname{Hom}_{\mathcal D}(d,Lc)}.
\end{aligned}
$$

です。coendの商は `Lc→d` の異なる表示を射に沿って同一視し、endの整合条件は `d→Lc` に沿う観測族を
選びます。ただしend・coendはKan拡張の定義上の前提ではありません。コンマ圏上の極限・余極限が基本公式で、
end・coend表示は追加の構造がある値圏で使える計算法です。

## 要点

* 左Kan拡張は自然変換 `F⇒L;E` を持つ候補の始対象であり、右Kan拡張は `L;E⇒F` を持つ候補の終対象である。
* 普遍性は `Nat(Lan_L F,G)≅Nat(F,L;G)` と `Nat(G,Ran_L F)≅Nat(L;G,F)` に圧縮できる。
* 全ての関手について存在すれば、左Kan拡張は前合成の左随伴、右Kan拡張は前合成の右随伴になる。
* 左拡張の各点値は `(L↓d)` 上の余極限、右拡張の各点値は `(d↓L)` 上の極限で計算される。
* 各点で普遍対象を選ぶだけでは足りず、コンマ圏間の関手と普遍性から射作用と関手法則を得る必要がある。
* end・coend表示は有用な計算法だが、Kan拡張の定義やコンマ圏による各点公式の厳密な前提ではない。

## 研究史と文献案内

Kan [KAN58] は随伴関手の研究の中で、後にKan拡張と呼ばれる普遍構成を導入しました。同論文の記法と
現代の関手圏・単位・余単位による定式化は同一ではないため、歴史的な初出と現在の標準APIを区別する必要が
あります。普遍性、各点公式、随伴との関係の現代的な扱いは [MAC98] を参照してください。豊穣圏における
Kan拡張とend・coend計算は [KEL82] が体系的です。Leanの `IsLeftKanExtension`,
`IsRightKanExtension`, `lan`, `ran` と点ごとの構成は [MATHLIB] の現行APIに従います。

## 問題

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

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

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

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

### 各点公式から射作用を構成する

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

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

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

end

end FormalLab.CategoryFoundations.KanExtensions