import Mathlib.CategoryTheory.Functor.Hom
import Mathlib.CategoryTheory.Limits.Types.End
import FormalLab.CategoryTheory.Limits

/-!
# 第62章：end・coend・双自然性

自然変換 `α:P⇒Q` は、各対象 `j` に射 `α_j:P(j)→Q(j)` を一つずつ割り当てるだけではありません。
全ての射 `f:i→j` に対して自然性正方形が可換するという等式で、成分族を同時に拘束します。成分の積を取り、
この等式を満たす部分だけを抜き出す構成がendの原型です。

双関手 `H:Jᵒᵖ×J→C` は同じ変数を反変・共変の二箇所に持ちます。対角成分 `H(j,j)` を集め、各射が
与える二つの作用を等しくする普遍対象がendです。全ての対角成分を、二作用が生成する関係で同一視する
双対の普遍対象がcoendです。本章ではwedgeとcowedgeの普遍性から両者を定義し、`Type` ではendが
整合族の部分型、coendが商型になることをLeanで確認します。

## 二変数を一つの射に沿って同時に動かす

関手

$$
H:J^{\mathrm{op}}\longrightarrow[J,\mathcal C].
$$

を考えます。これは非カリー化すれば `Jᵒᵖ×J→C` という双関手です。対象 `j` の対角値は `H(j,j)` です。
射 `f:i→j` からは共変変数を動かす射と反変変数を動かす射が得られます。

$$
H(i,i)\xrightarrow{H(i,f)}H(i,j)
\xleftarrow{H(f,j)}H(j,j).
$$

両方の終点は `H(i,j)` ですが、始点は異なります。この二作用を比較するには、各対角値へ射を持つ共通の
対象が必要です。
-/

namespace FormalLab.CategoryFoundations.EndsAndCoends

open _root_.CategoryTheory
open _root_.CategoryTheory.Limits

noncomputable section

universe w v' v u' u

variable {J : Type u} [Category.{v} J]
variable {C : Type u'} [Category.{v'} C]
variable (H : Jᵒᵖ ⥤ J ⥤ C)

example (j : J) : C := (H.obj (Opposite.op j)).obj j

example {i j : J} (f : i ⟶ j) :
    (H.obj (Opposite.op i)).obj i ⟶ (H.obj (Opposite.op i)).obj j :=
  (H.obj (Opposite.op i)).map f

example {i j : J} (f : i ⟶ j) :
    (H.obj (Opposite.op j)).obj j ⟶ (H.obj (Opposite.op i)).obj j :=
  (H.map f.op).app j

/-!
## wedgeは対角成分への整合する射族である

`H` のwedgeは対象 `W` と射族

$$
\omega_j:W\longrightarrow H(j,j)
$$

からなり、各 `f:i→j` に対して次の六角形を退化した等式を要求します。

$$
\omega_i;H(i,f)=\omega_j;H(f,j):W\longrightarrow H(i,j).
$$

この条件を双自然性条件と呼びます。通常の自然性では二つの関手の間に成分があり、ここでは一つの双関手の
反変・共変の二作用を対角上の成分族が結びます。
-/

example : Type _ := Wedge H

example (W : Wedge H) {i j : J} (f : i ⟶ j) :
    W.ι i ≫ (H.obj (Opposite.op i)).map f =
      W.ι j ≫ (H.map f.op).app j :=
  Wedge.condition W f

/-!
単なる射族 `W→H(j,j)` はwedgeではありません。上の等式が一つでも失敗すれば、二変数を同じ射に沿って
動かした結果が食い違います。endを成分の積だけとみなすと、この整合条件を落とします。

## endは普遍wedgeである

`H` のend `∫_j H(j,j)` は終対象的なwedgeです。標準射

$$
\pi_j:\int_j H(j,j)\longrightarrow H(j,j)
$$

を持ち、任意のwedge `ω_j:W→H(j,j)` から一意な射

$$
\mathsf{lift}(\omega):W\longrightarrow\int_j H(j,j)
$$

が存在して `lift(ω);π_j=ω_j` を満たします。積に全成分を集め、射ごとの二作用を等化する極限と考えられます。
-/

variable [HasEnd H]

example : C := end_ H

example (j : J) : end_ H ⟶ (H.obj (Opposite.op j)).obj j := end_.π H j

example {i j : J} (f : i ⟶ j) :
    end_.π H i ≫ (H.obj (Opposite.op i)).map f =
      end_.π H j ≫ (H.map f.op).app j :=
  end_.condition H f

variable {H}
variable {X : C}
variable (ω : ∀ j, X ⟶ (H.obj (Opposite.op j)).obj j)
variable (hω : ∀ ⦃i j : J⦄ (f : i ⟶ j),
  ω i ≫ (H.obj (Opposite.op i)).map f = ω j ≫ (H.map f.op).app j)

example : X ⟶ end_ H := end_.lift ω hω

example (j : J) : end_.lift ω hω ≫ end_.π H j = ω j :=
  end_.lift_π ω hω j

example {a b : X ⟶ end_ H}
    (h : ∀ j, a ≫ end_.π H j = b ≫ end_.π H j) : a = b :=
  end_.hom_ext h

/-!
`lift_π` が存在する媒介射の計算則、`hom_ext` が一意性です。`HasEnd H` はendの存在を仮定する命題で、
双関手の型だけからendが存在するとは限りません。値圏 `C` が必要な積と等化子を持つ場合に構成できます。

## `Type` 値endは整合する族の部分型である

`H:Jᵒᵖ→J→Type` の場合、全成分の従属積

$$
\prod_j H(j,j)
$$

から双自然性条件を満たす族だけを取ればendになります。

$$
\left\{x\in\prod_jH(j,j)\ \middle|\
H(i,f)(x_i)=H(f,j)(x_j)\text{ for every }f:i\to j\right\}.
$$

したがってendは「全成分の積に方程式を課す」極限です。部分型の第二成分は `Prop` の証明なので、Leanの
証明無関連性により同じ族と同じ条件の異なる証明を別要素として区別しません。
-/

variable (K : Jᵒᵖ ⥤ J ⥤ Type (max w u))

example : Type (max w u) := Types.end_ K

example (x : Types.end_ K) (j : J) : (K.obj (Opposite.op j)).obj j := x.1 j

example (x : Types.end_ K) {i j : J} (f : i ⟶ j) :
    (K.obj (Opposite.op i)).map f (x.1 i) = (K.map f.op).app j (x.1 j) :=
  x.2 f

/-!
## cowedgeは対角成分から出る射族である

射を全て反転すると、対象 `W` と射族

$$
\iota_j:H(j,j)\longrightarrow W
$$

を持つcowedgeが得られます。条件は

$$
H(f,i);\iota_i=H(j,f);\iota_j:H(j,i)\longrightarrow W.
$$

です。endのwedge条件と比べ、全射の向きと合成順序が反転しています。
-/

variable (H)

example : Type _ := Cowedge H

example (W : Cowedge H) {i j : J} (f : i ⟶ j) :
    (H.map f.op).app i ≫ W.π i =
      (H.obj (Opposite.op j)).map f ≫ W.π j :=
  Cowedge.condition W f

/-!
## coendは普遍cowedgeである

coend `∫^j H(j,j)` は始対象的なcowedgeです。標準射

$$
\iota_j:H(j,j)\longrightarrow\int^jH(j,j)
$$

を持ち、任意のcowedgeから一意な射 `desc:∫^jH(j,j)→W` が出ます。余積へ全対角成分を入れ、二作用から
来る射を余等化する余極限です。
-/

variable [HasCoend H]

example : C := coend H

example (j : J) : (H.obj (Opposite.op j)).obj j ⟶ coend H := coend.ι H j

example {i j : J} (f : i ⟶ j) :
    (H.map f.op).app i ≫ coend.ι H i =
      (H.obj (Opposite.op j)).map f ≫ coend.ι H j :=
  coend.condition H f

variable {H}
variable (γ : ∀ j, (H.obj (Opposite.op j)).obj j ⟶ X)
variable (hγ : ∀ ⦃i j : J⦄ (f : i ⟶ j),
  (H.map f.op).app i ≫ γ i = (H.obj (Opposite.op j)).map f ≫ γ j)

example : coend H ⟶ X := coend.desc γ hγ

example (j : J) : coend.ι H j ≫ coend.desc γ hγ = γ j :=
  coend.ι_desc γ hγ j

example {a b : coend H ⟶ X}
    (h : ∀ j, coend.ι H j ≫ a = coend.ι H j ≫ b) : a = b :=
  coend.hom_ext h

/-!
## `Type` 値coendは生成関係による商である

`Type` ではまず対角成分の従属和

$$
\coprod_j H(j,j)
$$

を取ります。射 `f:i→j` と `y∈H(j,i)` は、反変作用で得る `H(f,i)(y)∈H(i,i)` と、共変作用で得る
`H(j,f)(y)∈H(j,j)` を結びます。この関係が生成する商がcoendです。
-/

example : Type (max w u) := Types.coend K

example (j : J) : (K.obj (Opposite.op j)).obj j ⟶ Types.coend K :=
  Types.coend.ι K j

example {i j : J} (f : i ⟶ j) :
    (K.map f.op).app i ≫ Types.coend.ι K i =
      (K.obj (Opposite.op j)).map f ≫ Types.coend.ι K j :=
  Types.coend.condition f

/-!
endが部分型として条件を保持するのに対し、coendは商によって条件を等式へ強制します。`Quot` は同値類の
代表元を消去するので、coendから関数を定義するときは生成関係を保つことを証明しなければなりません。
積と余積、等化子と余等化子の双対が、部分型と商型という具体的な差として現れます。

## 自然変換はhom双関手のendとして読める

関手 `P,Q:J→C` に対し

$$
H(i,j)=\operatorname{Hom}_{\mathcal C}(P(i),Q(j)).
$$

と置きます。反変作用は `P(f)` の前合成、共変作用は `Q(f)` の後合成です。endの要素は成分族
`α_j:P(j)→Q(j)` と、全ての `f:i→j` に対する式

$$
P(f);\alpha_j=\alpha_i;Q(f).
$$

です。これは自然変換の定義そのものです。したがって集合として

$$
\operatorname{Nat}(P,Q)
\cong\int_j\operatorname{Hom}_{\mathcal C}(Pj,Qj).
$$

と読めます。ここでの同型は、hom双関手の構成と必要なendの存在を含みます。任意の成分族が自然変換になる
わけではなく、endの整合条件が自然性を正確に選び出します。

## co-Yoneda公式と重み付き合成への入口

集合値前層 `P:Jᵒᵖ→Type` と対象 `X` に対するco-Yoneda公式は概略

$$
\int^jP(j)\times\operatorname{Hom}(X,j)\cong P(X).
$$

という形を持ちます。左辺の要素は `j` と二つのデータの代表ですが、射に沿う移送を商で同一視するため、
表現対象の選び方に依存しない結果が得られます。この商の機構は、profunctorの合成、テンソル積、Kan拡張の
点ごとの公式にも繰り返し現れます。

## 要点

* 双関手 `H:Jᵒᵖ→J→C` は射の反変作用と共変作用を持つ。
* wedgeは射族 `W→H(j,j)` と双自然性条件からなり、endは普遍wedgeである。
* cowedgeは射族 `H(j,j)→W` を持ち、coendは普遍cowedgeである。
* `Type` 値endは整合族の部分型、coendは対角成分の従属和を生成関係で割った商型である。
* 自然変換全体はhom双関手のendとして表され、自然性はendの整合条件になる。
* endの存在は極限、coendの存在は余極限の仮定であり、双関手の型だけからは従わない。

## 研究史と文献案内

endとcoendの成立史には複数の研究経路が重なります。そこにはYonedaによる加法的な双自然変換の研究、
Kellyによる豊穣圏での一般化、Mac Laneによる通常圏論の体系化があります。積分記号の帰属も単一の資料へ安易に固定せず、本章では
現代の標準記法として使用します。通常の圏におけるwedge、双自然性、end計算は [MAC98]、豊穣化された
endとcoendは [KEL82] を参照してください。Leanの `Wedge`, `end_`, `Cowedge`, `coend` と `Type` における
部分型・商型の構成は [MATHLIB] の現行APIに従います。

## 問題

### 自然変換をendの要素へ翻訳する

関手 `P,Q:J→Type` と自然変換 `α:P⇒Q` を取り、族 `j↦α_j` を構成してください。hom双関手の反変作用を
前合成、共変作用を後合成として展開し、end条件が `P(f);α_j=α_i;Q(f)` になることを示します。逆に
endの要素から成分族と自然性証明を取り出して自然変換を作り、二構成が外延性により互いに逆であることを
証明できれば完了です。

### 一対象圏で不変量と余不変量を比較する

モノイド `M` を一対象圏とみなし、左作用と右作用を持つ集合から対応する双関手を作ってください。end条件が
全ての `m∈M` に関して作用と可換する不変な要素を選ぶことを示します。coendでは二作用から生じる要素を
同一視する商を記述してください。部分集合として残す操作と商集合へ送る操作の向きを比較し、endとcoendを
どちらも単なる直積または直和とみなしていないことを確認できれば完了です。

### co-Yoneda公式の商関係を検査する

前層 `P:Jᵒᵖ→Type` と `X:J` に対し、対 `⟨p∈P(j),f:X→j⟩` を `P(f)(p)∈P(X)` へ送る関数を
定めてください。射 `g:j→k` が生成するcoend関係の両辺が同じ値へ送られることを関手の合成保存から
証明し、商からの関数を得ます。逆写像を `x∈P(X)` から `⟨x,id_X⟩` の同値類として作り、二つの逆法則を
商の関係と恒等射保存によって示せれば完了です。
-/

end

end FormalLab.CategoryFoundations.EndsAndCoends