import Mathlib.CategoryTheory.Yoneda
import FormalLab.CategoryTheory.NaturalTransformations

/-!
# 第50章：hom関手・普遍元・表現可能関手

対象 `Y` を固定すると、各対象 `X` に射の型 `Hom(X,Y)` を対応させられます。射 `f:X'→X` は、
`X→Y` の射の前へ合成することで `Hom(X,Y)→Hom(X',Y)` を与えます。この対応は反変関手です。
対象を、その対象へ入る全射の振舞いとして外部から記述する「hom関手」が得られます。

集合値反変関手 `P` があるhom関手と自然同型であるとき、`P` は表現可能です。表現対象と一つの普遍元が
決まれば、`P(X)` の全要素を射 `X→Y` から一意に生成できます。本章ではこの対応を、自然な全単射、
普遍元、表現対象の一意性という三つの同値な見方から構成します。

## 固定した終点への射は反変に動く

圏 `C` の対象 `Y` を固定し、

$$
h_Y(X)=\mathcal C(X,Y)
$$

と置きます。射 `f:X'→X` に対する作用は前合成です。

$$
h_Y(f)(g)=g\circ f:X'\to Y.
$$

恒等射との前合成は何も変えず、合成射との前合成は前合成を二回行うことに等しいので、
`h_Y:Cᵒᵖ→Type` は関手になります。
-/

namespace FormalLab.CategoryFoundations.RepresentableFunctors

open _root_.CategoryTheory

universe v u

variable {C : Type u} [Category.{v} C]
variable {X X' Y : C}

example (Y : C) : Cᵒᵖ ⥤ Type v := yoneda.obj Y
example (X Y : C) : (yoneda.obj Y).obj (Opposite.op X) = (X ⟶ Y) := rfl

example (f : X' ⟶ X) (g : X ⟶ Y) :
    (yoneda.obj Y).map f.op g = f ≫ g := rfl

/-!
mathlibの `yoneda.obj Y` が `h_Y` です。圏 `C` の射 `k:Y→Z` は各 `X` で後合成
`Hom(X,Y)→Hom(X,Z)` を与え、hom関手間の自然変換になります。こうして `Y↦h_Y` 自身が関手
`C→[Cᵒᵖ,Type]` になります。
-/

example : C ⥤ Cᵒᵖ ⥤ Type v := yoneda
example {Z : C} (k : Y ⟶ Z) : yoneda.obj Y ⟶ yoneda.obj Z := yoneda.map k
example {Z : C} (k : Y ⟶ Z) (g : X ⟶ Y) :
    (yoneda.map k).app (Opposite.op X) g = g ≫ k := rfl

/-!
## 表現可能性は自然な全単射である

反変関手 `P:Cᵒᵖ→Type` が `Y` によって表現されるとは、全ての `X` について全単射

$$
\varphi_X:\mathcal C(X,Y)\xrightarrow{\;\cong\;}P(X)
$$

があり、`X` の射に関して自然であることです。`f:X'→X`, `g:X→Y` に対する自然性は

$$
\varphi_{X'}(g\circ f)=P(f)(\varphi_X(g)).
$$

です。単に各型の濃度が同じなのではなく、前合成と `P` の作用が対応しなければなりません。
-/

variable (P : Cᵒᵖ ⥤ Type v)
variable (R : P.RepresentableBy Y)

example : (X ⟶ Y) ≃ P.obj (Opposite.op X) := R.homEquiv

example (f : X' ⟶ X) (g : X ⟶ Y) :
    R.homEquiv (f ≫ g) = P.map f.op (R.homEquiv g) := R.homEquiv_comp f g

/-!
この構造は自然同型 `h_Y≅P` と同じ内容です。`RepresentableBy Y` は表現対象をデータとして保持します。
`IsRepresentable P` は何らかの表現対象が存在するという命題で、具体的な選択を結論の情報として残しません。
-/

example : P.IsRepresentable := R.isRepresentable
example (Y : C) : (yoneda.obj Y).IsRepresentable := inferInstance

/-!
## 普遍元一つから全要素を生成する

表現 `R` において恒等射 `id_Y` の像

$$
u=\varphi_Y(\mathrm{id}_Y)\in P(Y).
$$

を普遍元と呼びます。任意の `x∈P(X)` には一意な射 `f:X→Y` が対応し、`x=P(f)(u)` となります。
表現の自然な全単射全体が、表現対象 `Y` と一点 `u` に圧縮されます。
-/

def universalElement : P.obj (Opposite.op Y) := R.homEquiv (𝟙 Y)

example (g : X ⟶ Y) :
    R.homEquiv g = P.map g.op (universalElement P R) := R.homEquiv_eq g

def classifyingMorphism (x : P.obj (Opposite.op X)) : X ⟶ Y := R.homEquiv.symm x

example (x : P.obj (Opposite.op X)) :
    R.homEquiv (classifyingMorphism P R x) = x := R.homEquiv.apply_symm_apply x

/-!
存在は `homEquiv.symm x` が与え、一意性は全単射の単射性から従います。「普遍元」は特別な名前を持つ
要素というだけではなく、全ての要素が一意な射による引戻しとして得られる元です。

## 普遍性と表現可能性

極限錐の集合を対象 `X` ごとに集めると、`X` を錐頂点とする錐の型が反変関手をなします。極限対象 `L` は
この錐関手を `Hom(-,L)` として表現します。積、終対象、引戻しも同様です。普遍構成を表現可能性として
読むと、「任意の入力データから一意な媒介射」という共通形式が自然なhom全単射になります。

ただし表現可能性の定義だけから、任意の反変関手が表現可能とは結論できません。表現対象と自然な全単射を
構成することが存在定理の内容です。

## 表現対象の一意性

同じ `P` を `Y` と `Z` が表現すれば、自然同型 `h_Y≅P≅h_Z` を得ます。次章の米田の補題により、
この自然同型は一意な対象同型 `Y≅Z` から生じます。したがって表現対象は等号で一意なのではなく、
普遍元を保つ一意な同型を除いて一意です。

## 共変版

共変関手 `Q:C→Type` が `Hom(Y,-)` と自然同型なら、`Q` は余表現可能です。mathlibでは
`CorepresentableBy` と `coyoneda` がこの向きを表します。「表現可能」の向きは文献によって規約があるため、
homのどちらの変数を固定したかを式で確認します。

## 要点

* `Hom(-,Y)` は前合成によって反変関手になる。
* 表現可能関手は、あるhom関手と自然同型な集合値反変関手である。
* 表現は各 `X` における全単射だけでなく、前合成に関する自然性を要求する。
* 恒等射の像である普遍元から、関手の全要素が一意な分類射によって得られる。
* 表現可能性は普遍構成をhom全単射として統一するが、表現対象の存在は別に証明する。

## 研究史と文献案内

表現可能性は普遍問題をhom関手として理解する語彙であり、米田の仕事 [YON54] と、その後の圏論の
体系化を通じて中心的になりました。[YON54] の主題全体を現代の「表現可能関手」の教科書的定義へ
還元せず、現代的な普遍元との対応と表現対象の一意性には [MAC98] を参照してください。mathlibの
`yoneda`, `RepresentableBy`, `IsRepresentable` は [MATHLIB] の現行APIに従います。

## 問題

### hom関手の法則を合成律へ還元する

`h_Y(f)(g)=g∘f` から恒等射保存則と合成保存則を数式で証明してください。反変性により二射の順序が
どこで反転するかを、反対圏の合成と通常の合成の双方から追います。mathlibの `yoneda.obj Y` の `map_id`
と `map_comp` へ対応させ、可逆性を一度も仮定していないことまで確認できれば完了です。

### 普遍元から自然な全単射を復元する

`u∈P(Y)` とし、各 `X` で `f:X→Y` を `P(f)(u)` へ送る写像を定義してください。この写像が全単射に
なるために必要な存在一意性を明記し、`f:X'→X` に関する自然性を関手の合成保存則から証明します。
逆に表現 `R` から `u=R.homEquiv(id_Y)` を取り出し、二構成が互いに戻ることを示してください。最後に
普遍元を任意の元と取り違えると分類射の存在または一意性が失敗する例を一つ示せれば完了です。

### 積の普遍性を表現可能性へ翻訳する

固定した `A,B` に対し、`X` を `Hom(X,A)×Hom(X,B)` へ送る反変関手を定義してください。積対象 `P` の
射影から `Hom(X,P)≃Hom(X,A)×Hom(X,B)` を構成し、自然性を合成計算で証明します。全単射の順・逆写像を
第43章の媒介射と射影へ対応させ、積の存在と関手の表現可能性が同じ主張になることを説明できれば完了です。
-/

end FormalLab.CategoryFoundations.RepresentableFunctors