import FormalLab.CategoryTheory.RepresentableFunctors

/-!
# 第51章：米田の補題と米田埋め込み

表現可能関手 $h_X=\operatorname{Hom}_{\mathcal C}(-,X)$ から任意の反変関手 $P$ への自然変換は、全対象で関数を指定するため巨大な
データに見えます。ところが自然性により、その全成分はただ一つの要素から決まります。`X` における
恒等射をどこへ送るかだけで十分です。

米田の補題は自然変換の型 $\operatorname{Nat}(h_X,P)$ と要素の型 $P(X)$ の間に自然な全単射を与えます。
$P=h_Y$ とすれば、hom関手間の自然変換は元の射 $X\to Y$ と同じ情報になります。したがって各対象をそのhom関手へ送る
米田関手は完全忠実であり、圏を集合値関手の圏へ情報を失わず埋め込みます。

## 自然変換は恒等射での値から決まる

自然変換 $\alpha:h_X\Rightarrow P$ があれば、成分 $\alpha_X$ を恒等射へ適用して

$$
\alpha_X(1_X)\in P(X)
$$

を得ます。逆に $x\in P(X)$ があれば、各 $Y$ で

$$
\alpha^x_Y(f:Y\to X)=P(f)(x)
$$

と定義できます。関手法則が自然性を与えます。この二構成は互いに逆です。
-/

namespace FormalLab.CategoryFoundations.YonedaLemma

open _root_.CategoryTheory

universe v u

variable {C : Type u} [Category.{v} C]
variable {X Y : C}
variable {P : Cᵒᵖ ⥤ Type v}

example : (yoneda.obj X ⟶ P) ≃ P.obj (Opposite.op X) := yonedaEquiv

example (α : yoneda.obj X ⟶ P) :
    yonedaEquiv α = α.app (Opposite.op X) (𝟙 X) := yonedaEquiv_apply α

def transformationFromElement (x : P.obj (Opposite.op X)) : yoneda.obj X ⟶ P :=
  yonedaEquiv.symm x

example (x : P.obj (Opposite.op X)) (f : Y ⟶ X) :
    (transformationFromElement x).app (Opposite.op Y) f = P.map f.op x :=
  yonedaEquiv_symm_app_apply x (Opposite.op Y) f

example (x : P.obj (Opposite.op X)) :
    yonedaEquiv (transformationFromElement x) = x := yonedaEquiv.apply_symm_apply x

example (α : yoneda.obj X ⟶ P) : transformationFromElement (yonedaEquiv α) = α :=
  yonedaEquiv.symm_apply_apply α

/-!
最後の二式が全単射の逆法則です。任意の射 $f:Y\to X$ は $1_X$ の前へ $f$ を合成したものなので、自然性を
$f$ に適用すれば $\alpha_Y(f)=P(f)(\alpha_X(1_X))$ が得られます。全成分が恒等射での一点から復元される理由です。

## 反変性が自然性の式を決める

$P:\mathcal C^{\mathrm{op}}\to\mathbf{Set}$ を反変関手として書くと、射 $f:Y\to X$ は関数
$P(f):P(X)\to P(Y)$ を誘導します。さらに $u:Z\to Y$ に対し、$h_X(u)$ は $g:Y\to X$ を
$g\circ u:Z\to X$ へ送ります。自然性の可換平方は要素ごとに

$$
P(u)(\alpha_Y(g))=\alpha_Z(g\circ u)
$$

と読めます。$\alpha^x_Y(g)=P(g)(x)$ を代入すると、左辺は

$$
P(u)(P(g)(x))=P(g\circ u)(x)
$$

となり、反変関手の合成保存則そのものです。向きを一つでも逆にすると、関数の始域と終域が合わなくなります。
mathlibでは $P(f)$ に相当する作用を、反対圏の射 `f.op` に対する `P.map f.op` と書きます。

## 二つの写像が逆になる計算

評価写像と復元写像を

$$
\Phi(\alpha)=\alpha_X(1_X),
\qquad
\Psi(x)_Y(f)=P(f)(x)
$$

と置きます。一方の合成は関手の恒等射保存から

$$
\Phi(\Psi(x))=\Psi(x)_X(1_X)=P(1_X)(x)=x
$$

です。逆向きは、上の自然性を $g=1_X$、$u=f:Y\to X$ に適用して

$$
\Psi(\Phi(\alpha))_Y(f)
=P(f)(\alpha_X(1_X))
=\alpha_Y(1_X\circ f)
=\alpha_Y(f)
$$

を得ます。最後に自然変換の外延性を使い、全対象・全要素で成分が等しいことから
$\Psi(\Phi(\alpha))=\alpha$ を結論します。全単射は「自然性が情報を一点へ圧縮する」という主張であり、任意の
関数族には成立しません。

## hom関手間の自然変換は元の射である

`P=h_Y` とすると米田の全単射は

$$
\operatorname{Nat}(h_X,h_Y)\cong\operatorname{Hom}_{\mathcal C}(X,Y)
$$

になります。射 `g:X→Y` に対応する自然変換は、各 `Z` で後合成 `f↦g∘f` を行う変換です。
-/

example : (yoneda.obj X ⟶ yoneda.obj Y) ≃ (X ⟶ Y) := yonedaEquiv

example (g : X ⟶ Y) : yonedaEquiv (yoneda.map g) = g := yonedaEquiv_yoneda_map g

example (g : X ⟶ Y) {Z : C} (f : Z ⟶ X) :
    (yoneda.map g).app (Opposite.op Z) f = f ≫ g := rfl

/-!
この対応は射の合成も保ちます。したがって米田関手

$$
y:\mathcal C\longrightarrow[\mathcal C^{\mathrm{op}},\mathbf{Set}],
\qquad X\longmapsto h_X
$$

は各hom型の間に全単射を与える完全忠実関手です。

$\mathbf{Set}$ は通常の圏論記法です。mathlibでは宇宙サイズを明示するため、値域を `Type v` とし、関手圏を
`Cᵒᵖ ⥤ Type v` と表します。これは米田の補題を集合論から別の原理へ変更するのではなく、hom型と値の宇宙を
Leanの型として管理する具体化です。
-/

example : (yoneda (C := C)).FullyFaithful := Yoneda.fullyFaithful
example : (yoneda (C := C)).Full := inferInstance
example : (yoneda (C := C)).Faithful := inferInstance

/-- 表現可能関手の自然同型から、表現対象の同型を回収します。 -/
noncomputable def objectIsoFromYonedaIso
    (e : yoneda.obj X ≅ yoneda.obj Y) : X ≅ Y :=
  Yoneda.fullyFaithful.preimageIso e

/-!
忠実性は異なる射を異なる自然変換へ送ること、完全性はhom関手間の全自然変換が元の圏の射から来ることを
表します。「埋め込み」は対象型の部分型包含を意味せず、射の構造を完全に保存・反映する関手を意味します。

## 対象は全ての射によって識別される

もし $h_X\cong h_Y$ なら、その自然同型の順・逆自然変換は米田の全単射によって射 $X\to Y$, $Y\to X$ に対応します。
自然同型の逆法則を米田の忠実性で元へ戻せば `X≅Y` を得ます。対象を内部要素だけでなく、全ての対象から
入る射の体系によって同型まで識別できることが米田的な見方です。

これは「対象はhom集合そのものである」という等号ではありません。対象 `X` は表現可能関手 `h_X` へ完全忠実に
写され、元の圏の構造を関手圏内で回収できます。

## 米田の補題における二つの自然性

全単射 $\operatorname{Nat}(h_X,P)\cong P(X)$ は $X$ と $P$ の双方に自然です。$X$ の射に沿う自然性は前合成と $P$ の作用を
対応させ、`P⇒Q` に沿う自然性は自然変換の後合成と成分関数を対応させます。個々の型の全単射だけでなく、
二変数の変化と両立するため、極限、随伴、Kan拡張などの構成へ安定して代入できます。

具体的には、$k:X\to X'$、$\alpha:h_{X'}\Rightarrow P$、$\eta:P\Rightarrow Q$ に対して

$$
\Phi_{X,P}(\alpha\circ y(k))=P(k)(\Phi_{X',P}(\alpha)),
\qquad
\Phi_{X,Q}(\eta\circ\alpha)=\eta_X(\Phi_{X,P}(\alpha)).
$$

第一式は表現対象について反変、第二式は関手について共変な自然性を表します。単に各組 $(X,P)$ で同じ濃度の
集合があるだけでは、これらの式は得られません。

mathlibの `yonedaLemma` はこの二変数の自然性まで自然同型として束ねます。本章の `yonedaEquiv` は、
その各 `X,P` 成分を直接計算する形です。
-/

#check yonedaLemma

/-!
## 共米田の補題

射の向きを反転すれば、共変関手 $Q:\mathcal C\to\mathbf{Set}$ に対して

$$
\operatorname{Nat}(\operatorname{Hom}_{\mathcal C}(X,-),Q)\cong Q(X)
$$

を得ます。これは共米田の補題で、mathlibでは `coyonedaEquiv` として実装されます。米田の補題とは別原理を
追加するのではなく、反対圏で同じ定理を読みます。

## 要点

* `Nat(Hom(-,X),P)` は `P(X)` と自然に全単射である。
* 自然変換は `id_X` での値から復元され、復元式は `α_Y(f)=P(f)(α_X(id_X))` である。
* `P=Hom(-,Y)` とすると、hom関手間の自然変換は射 `X→Y` と同じ情報を持つ。
* 米田関手は完全忠実で、対象と射を集合値反変関手の圏へ情報を失わず埋め込む。
* 米田の全単射は表現対象と関手の双方に自然であり、反対圏から共米田の補題を得る。

## 研究史と文献案内

米田信夫の1954年論文 [YON54] は加群のホモロジー理論を主題とし、その中の補題が後に米田の補題として
広く抽象化されました。論文全体を現代の短い教科書的命題だけへ縮約しないことが重要です。自然性を含む
現代的定式化、完全忠実な米田埋め込み、表現可能性との関係は [MAC98] を参照してください。Leanで用いた
`yonedaEquiv`, `yonedaLemma`, `Yoneda.fullyFaithful` は [MATHLIB] の現行APIに従います。

## 問題

### 米田の全単射の逆法則を証明する

`x∈P(X)` から `α^x_Y(f)=P(f)(x)` を定義し、関手の合成保存則を使って自然性を証明してください。
`α^x_X(id_X)=x` は恒等射保存則から示します。逆に `α` から得た `x=α_X(id_X)` によって全成分が戻る
ことを自然性から導いてください。二つの写像が互いに逆であることを成分外延性まで含めて示し、
自然性を外すと一点の値だけでは変換を決定できない理由も説明できれば完了です。

### 完全忠実性を米田の補題から導く

米田の補題へ `P=h_Y` を代入し、`Nat(h_X,h_Y)≃Hom(X,Y)` を得てください。射 `g:X→Y` が後合成自然変換へ
写ることを恒等射で評価して確認します。全射性と単射性をそれぞれ関手の完全性・忠実性へ翻訳してください。
さらに射の合成と恒等射が米田関手で保たれることを確認し、単なる対象写像の単射を主張していないことまで
説明できれば完了です。

### 自然同型から対象同型を回収する

自然同型 `θ:h_X≅h_Y` の順方向と逆方向へ米田の全単射を適用し、射 `f:X→Y`, `g:Y→X` を得ます。
`θ.hom≫θ.inv=id` と逆向きの式を、米田関手が合成を保つことと忠実性によって元の圏へ戻してください。
二つの逆法則から `X≅Y` を構成し、表現対象の一意性へどう適用されるかを述べれば完了です。
-/

end FormalLab.CategoryFoundations.YonedaLemma