import Mathlib.CategoryTheory.Adjunction.Basic
import FormalLab.CategoryTheory.RepresentableFunctors

/-!
# 第52章：随伴——homの自然同型・単位・余単位

自由モノイドを作ってからモノイド準同型を与えることと、生成元の集合から台集合へ関数を与えることは
同じ情報です。このような対応は一つの対象対だけでなく、両方の対象を変えても自然に保たれます。二関手が
このhomの自然な全単射を持つとき、一方を左随伴、他方を右随伴と呼びます。

随伴は関手の逆関係ではありません。自由構成と忘却のように情報量の異なる圏を結び、往復が恒等になる必要も
ありません。本章ではhom全単射から単位・余単位を取り出し、逆に単位・余単位と三角恒等式からhom全単射を
復元します。最後に随伴を、対象ごとの表現可能性が関手的に選ばれたものとして読み直します。

## homの自然な全単射

関手 `F:C→D`, `G:D→C` に対して随伴 `F⊣G` とは、全ての `X:C`, `Y:D` に自然な全単射

$$
\operatorname{Hom}_{\mathcal D}(F X,Y)
\cong
\operatorname{Hom}_{\mathcal C}(X,G Y).
$$

があることです。左辺の射の転置を右辺へ、右辺の射の逆転置を左辺へ送ります。`X` の射に対する前合成と
`Y` の射に対する後合成の双方に自然である必要があります。
-/

namespace FormalLab.CategoryFoundations.Adjunctions

open _root_.CategoryTheory

universe vC vD uC uD

variable {C : Type uC} [Category.{vC} C]
variable {D : Type uD} [Category.{vD} D]
variable {F : C ⥤ D} {G : D ⥤ C}
variable (adj : F ⊣ G)
variable {X X' : C} {Y Y' : D}

example (X : C) (Y : D) : (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y) := adj.homEquiv X Y

example (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
    adj.homEquiv X' Y (F.map f ≫ g) = f ≫ adj.homEquiv X Y g :=
  adj.homEquiv_naturality_left f g

example (f : F.obj X ⟶ Y) (g : Y ⟶ Y') :
    adj.homEquiv X Y' (f ≫ g) = adj.homEquiv X Y f ≫ G.map g :=
  adj.homEquiv_naturality_right f g

/-!
第一式は `X` の変化、第二式は `Y` の変化に関する自然性です。対象対ごとに偶然同じ濃度のhom型があるだけでは
随伴になりません。射の合成を転置の前後で同じように処理できることが、構成を全圏へ一貫して拡張します。

## 単位は恒等射の転置である

hom全単射で `Y=F(X)` とし、恒等射 `id_{F(X)}` を転置すると

$$
\eta_X:X\longrightarrow G(F(X)).
$$

を得ます。これらは自然変換 `η:Id_C⇒F;G` をなし、随伴の単位と呼ばれます。
-/

example : 𝟭 C ⟶ F ⋙ G := adj.unit
example (X : C) : X ⟶ G.obj (F.obj X) := adj.unit.app X
example (X : C) : adj.homEquiv X (F.obj X) (𝟙 (F.obj X)) = adj.unit.app X :=
  adj.homEquiv_id X

/-!
自由・忘却随伴では `η_X` は各生成元を一文字の語へ入れる写像です。単位という名称はモノイドの単位元ではなく、
随伴を合成した自己関手への標準的な比較射を指します。

## 余単位は恒等射の逆転置である

`X=G(Y)` とし、`id_{G(Y)}` を逆転置すると

$$
\varepsilon_Y:F(G(Y))\longrightarrow Y.
$$

を得ます。これらは自然変換 `ε:G;F⇒Id_D` をなし、余単位と呼ばれます。
-/

example : G ⋙ F ⟶ 𝟭 D := adj.counit
example (Y : D) : F.obj (G.obj Y) ⟶ Y := adj.counit.app Y
example (Y : D) :
    (adj.homEquiv (G.obj Y) Y).symm (𝟙 (G.obj Y)) = adj.counit.app Y :=
  adj.homEquiv_symm_id Y

/-!
自由・忘却随伴では余単位は、形式的な語を `Y` の演算で評価します。単位が生成元を自由対象へ挿入し、余単位が
自由に作った式を既存の代数で評価するという対照が得られます。

## 転置と逆転置の公式

単位と余単位があれば、射 `f:F(X)→Y` の転置と `g:X→G(Y)` の逆転置は

$$
f^\flat=\eta_X;G(f),
\qquad
g^\sharp=F(g);\varepsilon_Y.
$$

で与えられます。
-/

example (f : F.obj X ⟶ Y) :
    adj.homEquiv X Y f = adj.unit.app X ≫ G.map f := rfl

example (g : X ⟶ G.obj Y) :
    (adj.homEquiv X Y).symm g = F.map g ≫ adj.counit.app Y := rfl

/-!
二公式を続けて元の射へ戻すために、単位・余単位の自然性だけでは一歩不足します。往復の余分な `FGF` または
`GFG` を消す三角恒等式が必要です。

## 三角恒等式

随伴の単位と余単位は各 `X,Y` で

$$
F(\eta_X);\varepsilon_{F(X)}=\mathrm{id}_{F(X)},
\qquad
\eta_{G(Y)};G(\varepsilon_Y)=\mathrm{id}_{G(Y)}.
$$

を満たします。この二式が、転置と逆転置を互いに逆にします。
-/

example (X : C) :
    F.map (adj.unit.app X) ≫ adj.counit.app (F.obj X) = 𝟙 (F.obj X) :=
  adj.left_triangle_components X

example (Y : D) :
    adj.unit.app (G.obj Y) ≫ G.map (adj.counit.app Y) = 𝟙 (G.obj Y) :=
  adj.right_triangle_components Y

/-!
mathlibの `Adjunction` は単位、余単位、二つの三角恒等式を基本データとして持ち、そこから `homEquiv` を
構成します。homの自然同型を基本にする定義と内容は同値ですが、どの方向を構成に使うかが異なります。

恒等関手は自分自身に随伴です。この場合、単位・余単位は恒等自然変換であり、転置は射を変えません。
-/

example : (𝟭 C) ⊣ (𝟭 C) := Adjunction.id

/-!
## 随伴は表現可能性の関手的な族である

`Y:D` を固定すると

$$
X\longmapsto\operatorname{Hom}_{\mathcal D}(F(X),Y).
$$

は `C` 上の反変関手です。随伴のhom全単射は、この関手が `G(Y)` によって表現されることを示します。
さらに `Y` を動かしたとき表現対象 `G(Y)` が関手をなし、全単射も `Y` に自然です。
-/

example (Y : D) : (F.op ⋙ yoneda.obj Y).RepresentableBy (G.obj Y) :=
  adj.representableBy Y

/-!
したがって右随伴を構成する問題は、各 `Y` でこの反変関手の表現対象を選び、それらが射に沿って関手をなすことを
示す問題として理解できます。普遍射による随伴の定義も、この表現の普遍元を対象ごとに与える形です。

## 圏同値との違い

圏同値では単位と余単位が自然同型です。一般の随伴では成分は可逆とは限りません。自由モノイドの台集合から
自由モノイドへ戻っても元のモノイドに等しくならないため、自由・忘却随伴は通常、圏同値ではありません。
随伴は可逆な対称性ではなく、最適近似や自由構成を表す非対称な関係です。

## 要点

* 随伴 `F⊣G` は `Hom_D(FX,Y)≃Hom_C(X,GY)` という二変数に自然な全単射である。
* 単位は `id_{FX}` の転置、余単位は `id_{GY}` の逆転置である。
* 任意の転置・逆転置は単位・余単位との合成によって計算できる。
* 三角恒等式が転置と逆転置の往復を恒等にする。
* 右随伴は `X↦Hom_D(FX,Y)` の表現対象を `Y` に関手的に選ぶものと読める。

## 研究史と文献案内

随伴関手はDaniel M. Kanの1958年論文 [KAN58] で導入され、普遍構成を統一する中心概念となりました。
同論文には後にKan拡張と呼ばれる構成も現れます。homの自然同型、単位・余単位、普遍射による三つの
現代的定式化とその同値性は [MAC98] を参照してください。mathlibの `Adjunction` は単位・余単位と
三角恒等式を保持し、`homEquiv` を導出する [MATHLIB] の現行APIです。

## 問題

### hom全単射から単位と余単位を取り出す

二変数に自然な全単射 `Φ_{X,Y}:Hom(FX,Y)≃Hom(X,GY)` を仮定してください。`η_X=Φ(id_{FX})` と
`ε_Y=Φ⁻¹(id_{GY})` を定義し、`X,Y` の射に関する自然性を用いて両者が自然変換になることを証明します。
さらに全単射の逆法則から二つの三角恒等式を導き、どちらの自然性を各段階で使うか明記できれば完了です。

### 単位・余単位から転置を復元する

単位 `η`, 余単位 `ε` と三角恒等式を仮定し、`f↦η;Gf` と `g↦Fg;ε` を定義してください。一方を他方へ
続けた式を展開し、関手法則、自然性、結合律、三角恒等式の順に書き換えて元の射へ戻します。二写像が
全単射であるだけでなく、両変数に自然であることまで合成計算で示してください。三角恒等式の一方だけを
仮定した場合に、どちらの逆法則までしか得られないかを区別できれば完了です。

### 自由・忘却随伴を具体的に読む

集合 `X` 上の有限語からなる自由モノイドと、モノイド `M` の台集合を考えてください。生成元上の関数
`X→U(M)` を語の評価によって準同型 `Free(X)→M` へ延長し、制限が逆写像になることを証明します。
単位を一文字語、余単位を語の評価として同定し、この随伴が通常は圏同値でない反例まで示せれば完了です。
-/

end FormalLab.CategoryFoundations.Adjunctions