import Mathlib.CategoryTheory.Monad.Monadicity
import FormalLab.CategoryTheory.Monads

/-!
# 第61章：比較関手・モナド性・Beckの定理

随伴 `L⊣R` からモナド `T=LR` が生じても、右随伴の定義域 `D` が自動的にEilenberg–Moore圏
`C^T` と同じになるわけではありません。各 `Y∈D` は `R(Y)` と余単位から作用 `T(RY)→RY` を持ちますが、
任意の `T`-代数がこの形から得られるか、代数準同型が `D` の射から来るかは別の問題です。

この差を測るのが比較関手 `K:D→C^T` です。`K` が圏同値であるとき右随伴 `R` をモナド的と呼びます。
本章では比較関手の対象・射作用を余単位の自然性から構成し、モナド性を完全性・忠実性・本質的全射性へ
分解します。最後に、圏同値を直接構成する代わりに特定の余等化子の生成・保存・反映を検査するBeck型の
モナド性定理を位置づけます。

## 随伴が各対象へ代数構造を与える

圏 `C,D` と随伴

$$
L:\mathcal C\to\mathcal D,
\qquad R:\mathcal D\to\mathcal C,
\qquad L\dashv R.
$$

を固定します。誘導モナドは `T=LR:C→C` で、単位は随伴の単位、乗法は中央で余単位を使う射です。
対象 `Y∈D` の `R(Y)` には作用

$$
L(RY)\xrightarrow{\varepsilon_Y}Y,
\qquad
T(RY)=R(L(RY))\xrightarrow{R(\varepsilon_Y)}RY.
$$

が入ります。随伴の三角恒等式と余単位の自然性から、これは `T` のEilenberg–Moore代数の二法則を満たします。
-/

namespace FormalLab.CategoryFoundations.Monadicity

open _root_.CategoryTheory

noncomputable section

universe v u₂ u₁

variable {C : Type u₁} {D : Type u₂}
variable [Category.{v} C] [Category.{v} D]
variable {L : C ⥤ D} {R : D ⥤ C}
variable (adj : L ⊣ R)

example : Monad C := adj.toMonad

example (Y : D) : adj.toMonad.Algebra := (Monad.comparison adj).obj Y

example (Y : D) : ((Monad.comparison adj).obj Y).A = R.obj Y := rfl

example (Y : D) :
    ((Monad.comparison adj).obj Y).a = R.map (adj.counit.app Y) := rfl

/-!
Leanの `adj.toMonad` は `L⋙R` を自己関手として持ちます。mathlibでは合成を図式順に書くため、通常の
関数記法 `R∘L` と文字順が逆に見えます。対象に適用すれば `R(LX)` なので、どちらの圏上のモナドかを
始域と終域から確認できます。

## 比較関手は射を右随伴で写す

射 `f:Y→Y'` は `R(f):R(Y)→R(Y')` を与えます。これが代数準同型になる条件は

$$
R(\varepsilon_Y);R(f)=T(R(f));R(\varepsilon_{Y'}).
$$

です。関手法則で `R` の外へ戻すと余単位の自然性

$$
\varepsilon_Y;f=L(R(f));\varepsilon_{Y'}.
$$

になります。したがって対象作用と射作用が一つの関手 `K` にまとまります。
-/

example : D ⥤ adj.toMonad.Algebra := Monad.comparison adj

example {Y Y' : D} (f : Y ⟶ Y') :
    ((Monad.comparison adj).map f).f = R.map f := rfl

example : Monad.comparison adj ⋙ adj.toMonad.forget ≅ R :=
  Monad.comparisonForget adj

/-!
最後の自然同型は、比較関手で代数にしてから台対象を忘れると元の右随伴 `R` に戻ることを述べます。
これは比較関手が圏同値であることをまだ意味しません。`K` の値が `R` の値を台対象に持つという一致だけです。

## モナド性は比較関手が圏同値であることをいう

右随伴 `R` がモナド的であるとは、ある左随伴との比較関手がEilenberg–Moore圏への圏同値になることです。
この条件のもとでは `D` の対象と射を、誘導モナドの代数と代数準同型として同型まで回収できます。

$$
\mathcal D\simeq\mathcal C^T.
$$

単に `R` が右随伴であること、忠実であること、モナド `T` が存在することのいずれも、単独ではモナド性を
与えません。比較関手が完全・忠実・本質的全射である必要があります。
-/

example [MonadicRightAdjoint R] :
    (Monad.comparison (monadicAdjunction R)).IsEquivalence := inferInstance

example [MonadicRightAdjoint R] : R.IsRightAdjoint := inferInstance

/-!
`MonadicRightAdjoint R` は左随伴、随伴、比較関手の圏同値性を保持します。左随伴の単なる存在命題ではなく
選ばれたデータを含みますが、異なる左随伴は一意な自然同型で結ばれるので、モナド性の数学的内容は
その選択に依存しません。

## Eilenberg–Moore忘却関手は標準的にモナド的である

任意のモナド `T` には自由代数関手と忘却関手の随伴

$$
\mathsf{Free}_T\dashv U_T:\mathcal C^T\longrightarrow\mathcal C.
$$

があります。この随伴から再び作ったモナドは `T` を回収し、比較関手はEilenberg–Moore圏を自分自身へ
戻します。したがって `U_T` はモナド的です。これはモナド的右随伴の基準例です。
-/

variable (T : Monad C)

example : T.free ⊣ T.forget := T.adj

example : MonadicRightAdjoint T.forget := inferInstance

example : (Monad.comparison T.adj).IsEquivalence := by
  letI : MonadicRightAdjoint T.forget := inferInstance
  change (Monad.comparison (monadicAdjunction T.forget)).IsEquivalence
  infer_instance

/-!
この例は「全ての右随伴がモナド的」であることを示しません。最初からEilenberg–Moore圏として構成された
忘却関手では比較が同値になる、という標準形を示します。一般の `R:D→C` については、`D` がこの標準形を
どこまで再現するかを証明しなければなりません。

## 比較関手の三つの障害

比較関手 `K` が忠実でないなら、`D` の異なる射が同じ代数準同型へ潰れます。完全でないなら、台対象間には
作用を保つ射があっても `D` の射として実現できません。本質的全射でないなら、モナド法則を満たす代数の
中に `D` の対象から来ないものが残ります。

右随伴 `R` が忠実なら比較関手も忠実です。実際、`K(f)` の台射は `R(f)` なので、`R` が射を区別すれば
`K` も区別します。しかし `R` の忠実性だけでは完全性も本質的全射性も得られません。
-/

example [R.Faithful] : (Monad.comparison adj).Faithful := inferInstance

/-!
圏同値を示すには三障害を全て除く必要があります。Beckの定理は、それらを個別に直接証明する代わりに、
右随伴が特定の余等化子をどのように扱うかという構成可能な条件へ置き換えます。

## 分裂対と余等化子

平行射 `f,g:A⇉B` の余等化子は、`f` と `g` を等しくする普遍射 `q:B→Q` です。右随伴 `R` を適用した
平行対が `C` で分裂しているとき、`f,g` を `R`-分裂対と呼びます。分裂データは余等化子の存在と保存を
強く制御するため、任意の余等化子を要求するより狭い検査対象になります。

比較関手の本質的全射性を作る際、`T`-代数 `(A,a)` から生じる標準的な反射対

$$
L(TA)\rightrightarrows L(A).
$$

の余等化子を `D` で取ります。この余等化子が比較関手の擬逆となる対象を構成します。余等化子の普遍性が
射の復元を与え、右随伴による保存・反映が単位と余単位を同型にします。

## Beck型モナド性定理

一つの標準形は次のように述べられます。`R` が左随伴を持ち、`R`-分裂対の余等化子を生成するなら、`R` は
モナド的です。「生成する」とは、`R` を適用した図式の余極限から `D` の余極限を一意に持ち上げ、さらに
その普遍性を反映することです。単なる余等化子の存在より強い条件です。
-/

example [Monad.CreatesColimitOfIsSplitPair R] : MonadicRightAdjoint R :=
  Monad.monadicOfCreatesGSplitCoequalizers adj

/-!
別の標準形では、`D` に `R`-分裂対の余等化子が存在し、`R` がそれを保存し、かつ同型を反映することを
仮定します。定理の版によって「生成」「保存かつ反映」「同型反映」の組合せが異なるため、Beckの定理という
名前だけで仮定を省略せず、使用する版を明記します。
-/

example [R.ReflectsIsomorphisms]
    [Monad.HasCoequalizerOfIsSplitPair R]
    [Monad.PreservesColimitOfIsSplitPair R] : MonadicRightAdjoint R :=
  Monad.monadicOfHasPreservesGSplitCoequalizersOfReflectsIsomorphisms adj

/-!
逆向きには、モナド的右随伴は `R`-分裂対の余等化子を生成します。したがって生成条件を使う版は単なる
十分条件ではなく、適切な意味で必要条件も表します。
-/

#check Monad.createsGSplitCoequalizersOfMonadic

/-!
## 余モナド性は全射を反転した双対である

左随伴 `L:C→D` から `D` 上の余モナドが生じ、比較関手 `C→Coalg(G)` を構成できます。この比較関手が
圏同値なら `L` は余モナド的です。Beck型条件では余等化子が等化子へ、右随伴が左随伴へ、分裂対が
双対の分裂対へ移ります。モナド性と余モナド性を同じ向きの忘却操作として混同しません。
-/

example {G : Comonad D} : ComonadicLeftAdjoint G.forget := inferInstance

/-!
## 要点

* 随伴 `L⊣R` は `C` 上のモナド `T=LR` と比較関手 `K:D→C^T` を生む。
* `K(Y)` の台対象は `R(Y)`、作用は `R(ε_Y)`、射作用は `R(f)` である。
* `R` がモナド的であるとは、比較関手が圏同値であり `D≃C^T` となることをいう。
* Eilenberg–Moore忘却関手はモナド的だが、一般の右随伴は自動的にモナド的ではない。
* Beck型定理は比較関手の圏同値性を、分裂対の余等化子の生成・保存・反映へ還元する。
* 定理の版ごとに仮定が異なり、余モナド性では全ての射と極限・余極限を双対化する。

## 研究史と文献案内

Eilenberg–Moore [EM65] は随伴、triple、代数の圏を結ぶ基礎を与えました。Beckの1967年学位論文
[BEC67] はtriple、代数、コホモロジーを展開します。2003年版の編集者序文によれば、草稿は1964年に
先行して流通しました。現在「Beckのモナド性定理」と呼ばれる諸定式化は仮定と用語が一様でなく、
単一の現代的命題を学位論文へ無注釈で投影しません。比較関手と標準的な定理の版は [MAC98] を参照し、
Leanの `Monad.comparison`, `MonadicRightAdjoint`, Beck型の各構成は [MATHLIB] の現行APIに従います。

## 問題

### 比較関手の代数法則を三角恒等式へ還元する

`K(Y)` の作用を `R(ε_Y):RLR(Y)→R(Y)` と置き、単位法則と結合法則を展開してください。単位法則を
随伴の三角恒等式へ、結合法則を余単位の自然性と関手の合成保存へ還元します。次に射 `f:Y→Y'` について
`R(f)` が作用を保つ正方形を書き、余単位の自然性から証明してください。Leanの `Monad.comparison` の
各フィールドと対応させ、モナド性を一度も仮定していないことを確認できれば完了です。

### 三障害を具体例で分類する

比較関手が忠実・完全・本質的全射であることの意味を、射の識別、代数準同型の復元、代数対象の復元として
それぞれ説明してください。`R` が忠実なら `K` も忠実である証明を台射から与えます。一方、忠実性だけから
完全性または本質的全射性が従うという誤った推論を特定し、それぞれに追加で何を構成すべきか述べてください。
圏同値の判定条件へ三項を正しく対応させられれば完了です。

### Beckの仮定から擬逆の構成を追う

`T`-代数 `(A,a)` に対する標準反射対 `LTA⇉LA` を書き、その共通切断を単位から構成してください。
この対の余等化子を `D` で取り、得られる対象を比較関手の擬逆候補とします。`R` が余等化子を生成する仮定が
対象の存在、射の持上げ、普遍性のどこで使われるかを区別してください。最後に保存・同型反映を使う別版と
仮定を比較し、単に「余等化子がある」とだけ述べていないことを確認できれば完了です。
-/

end

end FormalLab.CategoryFoundations.Monadicity