import Mathlib.CategoryTheory.Equivalence
import FormalLab.CategoryTheory.NaturalTransformations

/-!
# 第48章：同型・自然同型・圏同値

集合の全単射は逆関数を持ちますが、一般の圏では射が関数とは限りません。それでも射 `f:X→Y` に
両側逆射があれば、`X` と `Y` は圏の構造から見て同じ役割を果たします。これが対象の同型です。
一方、関手同士は各対象で同型になるだけでなく、その同型が自然でなければ構造的に比較できません。

さらに二つの圏が「同じ圏論」を表すために、対象型や射型の文字どおりの等しさを要求するのは強すぎます。
往復する関手の合成が恒等関手と自然同型になることを要求するのが圏同値です。本章ではこの三段階を、
等号との違い、逆射の二法則、自然性、完全忠実性と本質的全射性の順に組み立てます。

## 対象の同型は両側逆射を持つ

圏 `C` の対象 `X,Y` の同型 `e:X≅Y` は射

$$
e_{\mathrm{hom}}:X\to Y,
\qquad e_{\mathrm{inv}}:Y\to X
$$

と二つの逆法則から成ります。

$$
e_{\mathrm{inv}}\circ e_{\mathrm{hom}}=\mathrm{id}_X,
\qquad
e_{\mathrm{hom}}\circ e_{\mathrm{inv}}=\mathrm{id}_Y.
$$

一方の式だけでは足りません。集合の関数でも左逆だけを持つ単射、右逆だけを持つ全射があり、一般の圏でも
同じ区別が残ります。同型は対象の等式ではなく、圏の中にある可逆な射のデータです。
-/

namespace FormalLab.CategoryFoundations.Equivalences

open _root_.CategoryTheory
open FormalLab.CategoryFoundations
open FormalLab.CategoryFoundations.Functors

universe v₁ v₂ u₁ u₂

variable {C : Type u₁} [Category.{v₁} C]
variable {D : Type u₂} [Category.{v₂} D]
variable {X Y Z : C}

variable (e : X ≅ Y)

example : X ⟶ Y := e.hom
example : Y ⟶ X := e.inv
example : e.hom ≫ e.inv = 𝟙 X := e.hom_inv_id
example : e.inv ≫ e.hom = 𝟙 Y := e.inv_hom_id

/-!
mathlibの合成は進行順なので、`hom` の後に `inv` を進む第一式が `X` の恒等射になります。通常の
関数合成記法では `e.inv∘e.hom=id_X` と書くため、記号順だけを見ず始域から追います。

前章の一対象圏では、零射が恒等射です。零射は自分自身を逆射として同型を作ります。
-/

def starIdentityIso : star ≅ star where
  hom := additiveHom 0
  inv := additiveHom 0
  hom_inv_id := by rfl
  inv_hom_id := by rfl

example : starIdentityIso.hom ≫ starIdentityIso.inv = 𝟙 star := by simp

/-!
自然数加法では `m+n=0` なら両方が零なので、これ以外の射は可逆ではありません。一対象圏が持つ全ての射を
反転する反対圏と、実際に逆射を持つ同型射の部分を取り出すことは異なる操作です。

同型は合成できます。`X≅Y` と `Y≅Z` から `X≅Z` を作ると、順方向射と逆方向射では合成順序が逆に
なります。
-/

variable (d : Y ≅ Z)

example : X ≅ Z := e ≪≫ d
example : (e ≪≫ d).hom = e.hom ≫ d.hom := rfl
example : (e ≪≫ d).inv = d.inv ≫ e.inv := rfl

/-!
## 自然同型は可逆な自然変換である

関手 `F,G:C→D` の自然同型 `α:F≅G` は、自然変換 `α.hom:F⇒G` と逆向きの自然変換
`α.inv:G⇒F` が関手圏で互いに逆になるものです。したがって各成分 `α_X:F(X)≅G(X)` は同型ですが、
成分が同型であるだけでなく、全成分が射写像と自然に両立します。
-/

variable {F G : C ⥤ D}
variable (α : F ≅ G)

example : NatTrans F G := α.hom
example : NatTrans G F := α.inv
example (X : C) : F.obj X ≅ G.obj X := α.app X
example (X : C) : α.hom.app X ≫ α.inv.app X = 𝟙 (F.obj X) := α.hom_inv_id_app X

def scalingReflexiveIso (k : Nat) : scalingFunctor k ≅ scalingFunctor k := Iso.refl _

example : (scalingReflexiveIso 2).hom.app star = additiveHom 0 := rfl

/-!
「各 `X` について何らかの同型が存在する」という命題は、自然同型より弱い主張です。同型の選択が
`C` の射に対して自然性を満たす必要があるからです。自然同型は後の極限の保存、随伴のhom同型、
表現可能性の一意性で、関手を置き換えてよい精度を与えます。

## 圏同値は往復を自然同型で戻す

圏 `C,D` の圏同値は、関手

$$
F:C\to D,
\qquad G:D\to C
$$

と自然同型

$$
\eta:\mathrm{Id}_C\cong G\circ F,
\qquad
\varepsilon:F\circ G\cong\mathrm{Id}_D.
$$

を持ちます。さらに単位と余単位が整合する三角恒等式を課します。`G` は `F` の逆関数ではなく
擬逆関手であり、往復は恒等関手と等しい必要はなく自然同型なら十分です。
-/

variable (q : C ≌ D)

example : C ⥤ D := q.functor
example : D ⥤ C := q.inverse
example : 𝟭 C ≅ q.functor ⋙ q.inverse := q.unitIso
example : q.inverse ⋙ q.functor ≅ 𝟭 D := q.counitIso

example : C ≌ C := _root_.CategoryTheory.Equivalence.refl

/-!
恒等圏同値では往復が実際に恒等関手ですが、一般の圏同値はそうではありません。例えば圏から各同型類の
代表を一つずつ選んだ充満部分圏へ移ると、元の圏に異なるが同型な対象が複数あっても、代表側では一つに
まとめられます。対象型の全単射や圏の文字どおりの同型を要求すれば、この冗長性を除けません。

## 完全・忠実・本質的全射

関手 `F:C→D` が忠実であるとは、各 `X,Y` で射写像

$$
F_{X,Y}:\mathcal C(X,Y)\longrightarrow\mathcal D(FX,FY).
$$

が単射であることです。完全であるとは同じ写像が全射であることです。本質的全射とは、各 `Y:D` が
ある `F(X)` と同型であることです。「本質的」は対象の等号ではなく同型まで許すことを表します。

圏同値から得られる関手は完全、忠実、本質的全射です。逆に、完全・忠実・本質的全射な関手からは、
選択した逆像と同型を使って圏同値を構成できます。これは圏同値をhom集合と対象の到達性から判定する
実用的な特徴づけです。
-/

#check Functor.Full
#check Functor.Faithful
#check Functor.EssSurj
#check Functor.IsEquivalence

/-!
`IsEquivalence` は関手がこの特徴づけを満たすことを記録する型クラスです。圏同値 `C≌D` は往復関手と
自然同型をデータとして束ねるのに対し、`F.IsEquivalence` は一つの関手が圏同値を与え得るという性質を
表します。データと性質を用途に応じて区別します。

## 等号・同型・同値を使い分ける

対象の等号 `X=Y` からは輸送によって同型を作れますが、同型から一般に対象型の等号を得ることはしません。
関手の等号は全データの一致を要求し、自然同型は可逆な自然変換による比較を与えます。圏の文字どおりの
同型は往復合成が等号で恒等になることを要求し、圏同値は自然同型まで緩めます。定理の結論がどの強さを
必要とするかに合わせて選びます。

## 要点

* 対象の同型は順方向射、逆方向射、二つの逆法則から成る。
* 自然同型は関手圏における同型で、成分ごとの可逆性と自然性を同時に持つ。
* 圏同値は往復する関手の合成が恒等関手と自然同型になることを要求する。
* 圏同値は対象型の全単射や圏の文字どおりの同型より弱く、同型な対象の冗長性を無視する。
* 関手が圏同値を与えることは、完全・忠実・本質的全射であることによって特徴づけられる。

## 研究史と文献案内

自然同値はEilenberg–Mac Lane [EM45] の中心概念であり、同論文は自然性を通じて異なる構成を比較する
枠組みを与えました。圏同値と、完全・忠実・本質的全射による特徴づけの現代的な体系は [MAC98] を
参照してください。mathlibは圏同値を、三角恒等式を含むhalf-adjoint equivalenceとして束ねます。
本章の `Equivalence` と `Functor.IsEquivalence` の区別は [MATHLIB] の現行APIに従います。

## 問題

### 片側逆と同型を区別する

集合の圏で左逆を持つが右逆を持たない関数と、右逆を持つが左逆を持たない関数を一つずつ構成して
ください。各関数の始域・終域、片側の合成、失敗する側の反例を明記します。その後 `Iso` の二法則へ
翻訳してください。一方だけを省略すると対象の同型を定義できない理由を説明し、反対圏で射を読み直す
だけでは不足することも同じ例から確認できれば完了です。

### 自然同型の逆が自然であることを追う

自然同型 `α:F≅G` と射 `f:X→Y` を置き、`α.hom` の自然性と成分の逆法則から `α.inv` の自然性を
等式列で導いてください。合成の左右へ逆成分を付ける各段階で圏の結合律を明示します。成分ごとの同型を
無関係に選んだだけでは同じ導出を開始できないことを示し、自然性の役割を説明できれば完了です。

### 圏同値の判定条件を往復する

圏同値 `C≌D` から順方向関手が忠実、完全、本質的全射になる証明の構成を述べてください。逆向きには、
各 `D` の対象に選んだ逆像を擬逆関手の対象写像とし、完全性を使って射を持ち上げます。忠実性が関手法則の
一意性に、本質的全射性が余単位の成分に使われる箇所を特定し、選択への依存も説明できれば完了です。
-/

end FormalLab.CategoryFoundations.Equivalences