import Mathlib.CategoryTheory.Limits.IsLimit
import FormalLab.CategoryTheory.Equivalences

/-!
# 第49章：図式・錐・極限・余極限

積は二対象への射を同時に束ね、終対象は射を一本も指定しない普遍対象でした。この二例を別々に定義すると、
対象が三つ以上ある場合、対象間にも射がある場合、無限個の場合ごとに新しい定義が必要になります。図式は
対象と射の配置を一つの関手として記録し、錐はその全体を一つの対象から整合的に観察します。

極限は全ての錐から一意な媒介射を受ける錐です。射を全て反転すると余錐と余極限になります。本章では
図式から自然性と媒介射の三条件までを順に展開します。終対象、積、等化子、引戻しが同じ定義の異なる形で
あることを明らかにします。

## 図式は形を圏へ移す関手である

小さな圏 `J` を図式の形、圏 `C` を値域とします。図式は関手 `F:J→C` です。`J` の対象は図式の頂点、
射は辺を表し、関手法則が恒等辺と辺の合成を保ちます。対象の族だけでは、頂点間の射とその方程式を
記録できません。

例えば離散な二対象を形にすれば二対象の積、平行な二射を形にすれば等化子、共通の終点を持つ二射を
形にすれば引戻しが現れます。形を変えても普遍性の定義は変わりません。
-/

namespace FormalLab.CategoryFoundations.Limits

open _root_.CategoryTheory
open _root_.CategoryTheory.Limits

universe vJ vC uJ uC

variable {J : Type uJ} [Category.{vJ} J]
variable {C : Type uC} [Category.{vC} C]
variable {F : J ⥤ C}

example : J ⥤ C := F
example (j : J) : C := F.obj j
example {i j : J} (f : i ⟶ j) : F.obj i ⟶ F.obj j := F.map f

/-!
## 錐は一つの頂点から図式全体を見る

図式 `F:J→C` 上の錐 `s` は、錐頂点 `s.pt` と、各 `j:J` への脚

$$
\pi_j:s_{\mathrm{pt}}\to F(j)
$$

を持ちます。図式の射 `f:i→j` に対して、脚は

$$
F(f)\circ\pi_i=\pi_j
\qquad(f:i\to j).
$$

を満たします。mathlibは脚の族とこの整合性を、定値関手から `F` への自然変換 `s.π` として束ねます。
-/

variable (s : Cone F)

example : C := s.pt
example (j : J) : s.pt ⟶ F.obj j := s.π.app j
example {i j : J} (f : i ⟶ j) : s.π.app i ≫ F.map f = s.π.app j := s.w f

/-!
錐の条件は、図式の辺をたどる観察と、目的頂点を直接観察する脚が一致することです。任意の射の族では
ありません。積の図式が離散なら頂点間の辺がないため、この整合条件は自明になり、二本の射だけが残ります。

## 極限は全ての錐を一意に媒介する

錐 `t` が極限錐であるとは、任意の錐 `s` に対して一意な射

$$
\mathsf{lift}_s:s_{\mathrm{pt}}\to t_{\mathrm{pt}}
$$

があり、全ての脚を保存することです。

$$
\mathsf{lift}_s;\pi^t_j=\pi^s_j
\qquad(j:J).
$$

存在だけでなく、この方程式を満たす射が `lift_s` に等しいという一意性を要求します。
-/

variable {t : Cone F} (ht : IsLimit t)

example : s.pt ⟶ t.pt := ht.lift s
example (j : J) : ht.lift s ≫ t.π.app j = s.π.app j := ht.fac s j

example (m : s.pt ⟶ t.pt) (hm : ∀ j : J, m ≫ t.π.app j = s.π.app j) :
    m = ht.lift s := ht.uniq s m hm

/-!
`lift` がデータ、`fac` が要求された可換性、`uniq` が普遍性の一意性です。以前の積では `lift` が対を
作る写像、`fac` が二つの射影計算則、`uniq` が対を作る写像の外延性でした。極限は同じ骨格を任意の
図式へ一般化します。

## 極限対象は一意な同型を除いて一意である

同じ図式に二つの極限錐 `s,t` があれば、各普遍性から相手への媒介射を得ます。その合成と恒等射はどちらも
同じ脚を保存するため、一意性によって等しくなります。したがって二つの錐頂点は同型です。
-/

variable {r : Cone F} (hr : IsLimit r)

def limitPointIso : r.pt ≅ t.pt := IsLimit.conePointUniqueUpToIso hr ht

example : (limitPointIso (ht := ht) (hr := hr)).hom = ht.lift r := rfl
example (j : J) :
    (limitPointIso (ht := ht) (hr := hr)).hom ≫ t.π.app j = r.π.app j := by
  exact IsLimit.conePointUniqueUpToIso_hom_comp hr ht j

/-!
得られるのは任意の同型ではなく、脚と可換する一意な同型です。極限の「一意性」を対象の等号として
述べない理由がここにあります。

## 余錐と余極限は全射を反転する

余錐 `s` は各図式対象から一つの余錐頂点へ向かう脚 `s.ι_j:F(j)→s.pt` を持ちます。余極限錐 `t` から
任意の余錐 `s` へ一意な媒介射 `desc_s:t.pt→s.pt` が出ます。
-/

variable (q : Cocone F)
variable {p : Cocone F} (hp : IsColimit p)

example (j : J) : F.obj j ⟶ q.pt := q.ι.app j
example : p.pt ⟶ q.pt := hp.desc q
example (j : J) : p.ι.app j ≫ hp.desc q = q.ι.app j := hp.fac q j

example (m : p.pt ⟶ q.pt) (hm : ∀ j : J, p.ι.app j ≫ m = q.ι.app j) :
    m = hp.desc q := hp.uniq q m hm

/-!
反対圏では `C` の余錐が `Cᵒᵖ` の錐になり、余極限が極限になります。積と余積、終対象と始対象、
等化子と余等化子、引戻しと押出しはこの双対性の具体例です。双対化は逆射を仮定せず、定義中の全射と
合成順序を一貫して反転します。

## 代表的な形

空な形の極限は終対象、空な形の余極限は始対象です。離散な二点の極限は積、余極限は余積です。平行な
二射の極限は等化子、余極限は余等化子です。`X→Z←Y` の形の極限は引戻し、反対向きの余極限は押出しです。
無限の形も同じ定義で扱えますが、圏が全ての形の極限を持つとは限りません。普遍性の定義と存在定理を
分けて扱います。

## 要点

* 図式は形の圏から値域圏への関手で、頂点・辺・合成をまとめて記録する。
* 錐は一つの頂点と図式全体への自然な脚の族から成る。
* 極限錐は任意の錐から一意な媒介射を受け、全ての脚を保存する。
* 二つの極限対象は、脚と可換する一意な同型によって結ばれる。
* 余錐と余極限は射を反転した双対概念であり、定義と存在は別問題である。

## 研究史と文献案内

極限という統一概念は、積・逆極限・核など個別の普遍構成をまとめる過程で形成されました。Eilenberg–
Mac Lane [EM45] の圏・関手・自然性の枠組みだけへ現代の極限定義を遡及させません。錐と普遍性による
標準的な定式化、極限と余極限の双対性は [MAC98] を参照してください。mathlibの `Cone`, `IsLimit`,
`Cocone`, `IsColimit` は [MATHLIB] の現行APIに従います。

## 問題

### 積を離散二点図式の極限として復元する

二対象だけを持ち非恒等射を持たない形を用意し、錐のデータを頂点 `P` と二本の射影へ展開してください。
`IsLimit.lift`, `fac`, `uniq` を第43章の媒介射、二つの計算則、一意性へ一項ずつ対応させます。形が離散で
あるため錐の自然性条件が追加方程式を生まないことまで説明できれば完了です。

### 二つの極限を結ぶ同型を構成する

極限錐 `s,t` を仮定し、双方の `lift` から射 `s.pt→t.pt` と `t.pt→s.pt` を作ってください。合成と
恒等射が同じ脚を持つことを `fac` で示し、`uniq` を使って二つの逆法則を導きます。単なる対象同型ではなく、
脚と可換する同型が一意であることまで証明のどの段階から従うかを示してください。

### 引戻しと押出しを双対化する

図式 `X→Z←Y` の錐を展開し、二本の脚と `Z` への合成が等しい条件を得てください。その極限の媒介射が
引戻しの普遍性になることを述べます。全ての射を反転して押出しの余錐と余極限条件を作り、逆関数を一つも
仮定していないこと、また任意の圏で存在するとは主張していないことを確認できれば完了です。
-/

end FormalLab.CategoryFoundations.Limits