import Mathlib.CategoryTheory.Endofunctor.Algebra
import Mathlib.CategoryTheory.Types.Basic
import FormalLab.CategoryTheory.Functors

/-!
# 第54章：自己関手の代数と代数準同型

自然数では、零と後者を一つの写像 `1+ℕ→ℕ` にまとめられます。構文木では、一層分の演算記号と部分木を
完成した木へ組み立てる写像があります。この「一層分の形を既存の値へ畳み込む写像」を、自己関手の代数と
呼びます。

自己関手 `F` の代数は射 `F(A)→A` を一つ持つだけで、モナド代数の単位律・結合律を要求しません。本章では
Option自己関手の代数を具体化し、代数準同型の可換正方形を導きます。次章では全ての代数への一意な準同型を
持つ始代数を取り出し、foldと帰納的データの関係へ進みます。

## 一層の構造を値へ畳み込む

圏 `C` の自己関手 `F:C→C` に対し、`F`-代数は対象 `A` と構造射

$$
a:F(A)\to A.
$$

から成ります。`F(A)` は部分値の位置にすでに `A` を入れた一層分の構造、`a` はその一層を完成した値へ
畳み込みます。
-/

namespace FormalLab.CategoryFoundations.EndofunctorAlgebras

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor

universe v u

variable {C : Type u} [Category.{v} C]
variable {F : C ⥤ C}
variable (A : Algebra F)

example : C := A.a
example : F.obj A.a ⟶ A.a := A.str

/-!
ここで `A.a` は代数の台対象であり、`A.str` が構造射です。モナドのEilenberg–Moore代数 `T.Algebra` とは
別の構造です。自己関手代数には `η` や `μ` がなく、それらと両立する法則も課しません。

## Option自己関手の代数は既定値を選ぶ

型と関数の圏で `F(X)=Option X` とします。`Option.map` によって関数を射へ移せるため、これは自己関手です。
-/

def optionEndofunctor : Type u ⥤ Type u where
  obj X := Option X
  map f := ↾(Option.map f)
  map_id X := by
    ext x
    cases x <;> rfl
  map_comp f g := by
    ext x
    cases x <;> rfl

def optionAlgebraStructure (α : Type u) (base : α) : Option α → α
  | none => base
  | some x => x

def pointedOptionAlgebra (α : Type u) (base : α) : Algebra optionEndofunctor where
  a := α
  str := ↾(optionAlgebraStructure α base)

example (α : Type u) (base : α) : Option α → α := (pointedOptionAlgebra α base).str
theorem optionAlgebra_none : optionAlgebraStructure Nat 7 none = 7 := rfl
theorem optionAlgebra_some : optionAlgebraStructure Nat 7 (some 3) = 3 := rfl

/-!
この例の構造射は `none` の解釈として既定値を選び、`some x` を `x` へ戻します。ただし一般の
Option代数は任意の関数 `Option A→A` であり、必ず `some x=x` を満たすとは限りません。自己関手代数の
定義が要求するデータと、この具体例へ追加した性質を区別します。

## 代数準同型は構造の解釈を保つ

二つの `F`-代数 `(A,a)`, `(B,b)` の間の準同型は射 `f:A→B` で、次の正方形を可換にします。

$$
F(f);b=a;f.
$$

両辺はともに $F(A)\to B$ です。左辺は部分値を先に写してから解釈し、右辺は元の代数で解釈してから
台射で写します。
-/

variable {A B : Algebra F}
variable (f : A ⟶ B)

example : A.a ⟶ B.a := f.f
example : F.map f.f ≫ B.str = A.str ≫ f.f := f.h

/-!
Optionの具体例では、通常の関数 `f:α→β` が選んだ既定値を保てば代数準同型になります。
-/

def pointedMap {α β : Type u} {a : α} {b : β} (f : α → β) (h : f a = b) :
    pointedOptionAlgebra α a ⟶ pointedOptionAlgebra β b where
  f := ↾f
  h := by
    ext x
    cases x with
    | none => exact h.symm
    | some x => rfl

example : pointedOptionAlgebra Nat 0 ⟶ pointedOptionAlgebra Nat 1 :=
  pointedMap Nat.succ rfl

/-!
`none` の場合が既定値保存 `f(a)=b` を要求し、`some` の場合は自動的に可換します。可換正方形は、構造を
先に解釈してから写す経路と、部分値を写してから構造を解釈する経路が一致することを表します。

## 代数と代数準同型は圏をなす

恒等射は構造を保ち、構造を保つ射の合成も構造を保ちます。したがって `F`-代数を対象、代数準同型を射と
する圏 `Alg(F)` ができます。忘却関手は代数を台対象へ、準同型を台射へ送ります。
-/

example : Category (Algebra F) := inferInstance
example : Algebra F ⥤ C := Algebra.forget F

/-!
## 多項式関手との接続

定数、恒等、和、積から作る多項式関手では、`F(A)` は構成子の一層を表します。`F(X)=1+X` の代数は
一点 `1→A` と自己写像 `A→A`、`F(X)=1+X×X` の代数は葉と二項節点を解釈する操作を持ちます。
始代数を取ると有限に生成される構文・自然数・木とfoldが得られます。

## 要点

* 自己関手 `F` の代数は対象 `A` と構造射 `F(A)→A` から成る。
* 構造射は一層分の形を完成した値へ畳み込む。
* 代数準同型は `F(f);b=a;f` を満たし、構造の解釈を保つ。
* `F`-代数と準同型は圏をなし、台対象への忘却関手を持つ。
* 自己関手代数は、追加法則を持つモナドのEilenberg–Moore代数とは異なる。

## 研究史と文献案内

関手の代数による再帰構造の統一はLambek [LAM68] の不動点定理と、後の初期代数意味論へつながります。
帰納的データ型を始代数として扱う計算機科学側の展開は [LS86] と [AMM25] を参照してください。mathlibの
`Endofunctor.Algebra` と `Algebra.Hom` は [MATHLIB] の現行APIに従います。モナド代数の歴史 [EM65] を
自己関手代数一般の定義へそのまま帰属させません。

## 問題

### Option代数の準同型条件を特徴づける

`pointedOptionAlgebra α a` と `pointedOptionAlgebra β b` の間の関数 `f:α→β` について、代数準同型条件が
`f(a)=b` と同値であることを証明してください。可換正方形を `none` と `some x` で場合分けし、必要性と
十分性を別々に示します。一般のOption代数では同じ特徴づけが成立しない理由も反例から説明できれば完了です。

### 二項木の一層関手を構成する

`F(X)=1+X×X` を型と関数の圏の自己関手として実装し、関手法則を成分ごとに証明してください。自然数への
代数として、葉を `1`、節点を加法へ送る構造射を定義します。この代数が木の葉数を計算するfoldの終域に
なることを予想し、構造射の各分岐と再帰方程式を対応づけてください。葉と節点の順序を交換した別の和型でも
自然同型な関手が得られることを確認し、内部表現と代数の役割を区別できれば完了です。

### 代数準同型の合成を検査する

三代数と二準同型 `f:A→B`, `g:B→C` を置き、`F(f;g);c=a;(f;g)` を関手の合成保存則と二つの可換正方形から
導いてください。恒等射についても同様に証明し、代数の圏法則が台圏の法則へ還元される箇所と、構造保存が
閉じていることを示す箇所を分離してください。忘却関手がこの合成と恒等射をそのまま台射へ送ることまで
Leanの型で検査できれば完了です。
-/

end FormalLab.CategoryFoundations.EndofunctorAlgebras