import FormalLab.CategoryTheory.EndofunctorAlgebras

/-!
# 第55章：始代数・fold・Lambekの補題

自己関手の代数は一層分の構造を解釈しますが、どの代数を選ぶかは定義だけでは決まりません。全ての
`F`-代数へ一意な準同型を持つ代数を選ぶと、その一意な射があらゆる構造再帰を与えます。この普遍対象が
始代数です。

本章では `F(X)=1+X` の代数圏で自然数を始代数として構成します。任意の零候補と後者候補からfoldを定義し、
準同型条件と一意性を帰納法で証明します。最後に、始代数の構造射が同型になるLambekの補題を確認し、
不動点方程式と普遍性の論理的な順序を明確にします。

## `1+X` は零または一つの再帰位置を表す

型と関数の圏で自己関手

$$
F(X)=1+X.
$$

を考えます。左成分は再帰位置を持たない零項構成子、右成分は一つの再帰位置を持つ単項構成子です。
-/

namespace FormalLab.CategoryFoundations.InitialAlgebras

open _root_.CategoryTheory
open _root_.CategoryTheory.Endofunctor
open _root_.CategoryTheory.Limits

universe u

def onePlusFunctor : Type u ⥤ Type u where
  obj X := Unit ⊕ X
  map f := ↾(Sum.map id f)
  map_id X := by
    ext x
    cases x <;> rfl
  map_comp f g := by
    ext x
    cases x <;> rfl

def natStructure : Unit ⊕ Nat → Nat
  | .inl _ => 0
  | .inr n => n + 1

def natAlgebra : Algebra onePlusFunctor where
  a := Nat
  str := ↾natStructure

theorem natStructure_zero : natStructure (.inl ()) = 0 := rfl

theorem natStructure_successor : natStructure (.inr 4) = 5 := rfl

/-!
構造射 `[zero,succ]:1+ℕ→ℕ` は二構成子を一つの射にまとめます。しかしこの射が同型であることだけでは、
自然数の帰納法や再帰原理は得られません。始性を証明する必要があります。

## 任意の代数へのfold

任意の `F`-代数 `A` の構造射 `1+A→A` は、左成分から基底値を、右成分から一ステップの演算を与えます。
自然数から `A` へのfoldを

$$
\begin{aligned}
\mathsf{fold}_A(0)&=a(\mathsf{inl}(*)),\\
\mathsf{fold}_A(n+1)&=a(\mathsf{inr}(\mathsf{fold}_A(n))).
\end{aligned}
$$

と定義します。
-/

def fold (A : Algebra onePlusFunctor) : Nat → A.a
  | 0 => A.str (.inl ())
  | n + 1 => A.str (.inr (fold A n))

/-! 加法を計算する具体的な `onePlusFunctor`-代数を作ります。 -/

def addAlgebra (k : Nat) : Algebra onePlusFunctor where
  a := Nat
  str := ↾fun
    | .inl _ => 0
    | .inr n => n + k

def addFold (k n : Nat) : Nat := fold (addAlgebra k) n

theorem addFold_three_four : addFold 3 4 = 12 := rfl

/-!
`fold` が単なる再帰関数で終わらず代数準同型になることを、可換正方形として検査します。
-/

def foldHom (A : Algebra onePlusFunctor) : natAlgebra ⟶ A where
  f := ↾fold A
  h := by
    ext x
    cases x <;> rfl

example (A : Algebra onePlusFunctor) :
    onePlusFunctor.map (foldHom A).f ≫ A.str = natAlgebra.str ≫ (foldHom A).f :=
  (foldHom A).h

/-!
## 準同型はfoldに限る

任意の代数準同型 `f:natAlgebra→A` は、可換正方形を左成分で評価すると基底方程式、右成分で評価すると
再帰方程式を満たします。自然数帰納法によって全ての `n` で `f(n)=fold_A(n)` が従います。
-/

theorem fold_unique (A : Algebra onePlusFunctor) (f : natAlgebra ⟶ A) : f = foldHom A := by
  apply Algebra.ext
  ext n
  change f.f n = fold A n
  induction n with
  | zero =>
      have h := types_congr_hom f.h (Sum.inl ())
      exact h.symm
  | succ n ih =>
      have h := types_congr_hom f.h (Sum.inr n)
      change A.str (Sum.inr (f.f n)) = f.f (n + 1) at h
      calc
        f.f (n + 1) = A.str (Sum.inr (f.f n)) := h.symm
        _ = A.str (Sum.inr (fold A n)) := by rw [ih]
        _ = fold A (n + 1) := rfl

def natIsInitial : IsInitial natAlgebra :=
  IsInitial.ofUniqueHom (fun A => foldHom A) (fun A f => fold_unique A f)

/-!
`natIsInitial` は任意の `1+X`-代数へ一意な代数準同型が存在することを一つの値として束ねます。foldの
存在だけでなく、構造方程式を満たす関数の一意性まで含むため、始代数の普遍性になります。

## Lambekの補題

始 `F`-代数 `(μF,in)` の構造射

$$
\mathsf{in}:F(\mu F)\longrightarrow\mu F
$$

は同型です。逆射は、`F(μF)` に自然に入る `F`-代数への始性から得ます。二つの逆法則の一方は始性の
一意性、もう一方は関手で写した等式と代数準同型条件から従います。
-/

example : IsIso natAlgebra.str := Algebra.Initial.str_isIso natIsInitial

/-!
したがって `μF≅F(μF)` という不動点同型を得ます。しかし論理の向きは、始性から不動点同型を導く方向です。
方程式 `X≅F(X)` を満たす対象は複数あり得るため、その方程式だけから始代数性やfoldの一意性を結論できません。

## 帰納法との関係

foldは非依存な終域 `A` への再帰を表します。述語 `P(n)` を証明する帰納法は、各 `n` で変わるファイバーを
扱う依存的な除去原理です。始代数意味論と帰納法の対応には、ファイブレーションや述語持ち上げなど追加構造が
必要です。後の橋章で、帰納型理論と始代数を同一視せず条件を明示して接続します。

## 要点

* 始 `F`-代数から任意の `F`-代数へは一意な代数準同型が出る。
* `F(X)=1+X` では自然数の構造射が零と後者をまとめ、唯一の準同型がfoldになる。
* foldの存在は構造再帰、一意性は同じ再帰方程式を満たす関数の外延的な一意性を与える。
* Lambekの補題により始代数の構造射は同型になる。
* 不動点同型だけでは始性を含まず、非依存foldだけでは依存的帰納法を尽くさない。

## 研究史と文献案内

Lambek [LAM68] は完備圏に関する不動点定理の文脈で、始代数の構造射が同型になる原理を示しました。
始代数による帰納的データ型とfoldの整理は [LS86]、関手不動点の存在条件と終余代数との体系的比較は
[AMM25] を参照してください。mathlibの `Limits.IsInitial` と `Algebra.Initial.str_isIso` は [MATHLIB] の
現行APIに従います。

## 問題

### foldの一意性を可換正方形から再構成する

代数準同型 `f:natAlgebra→A` の条件を `inl(*)` と `inr(n)` で評価し、基底方程式と再帰方程式を得てください。
自然数帰納法で `f(n)=fold_A(n)` を証明し、関数外延性と代数準同型外延性を順に適用します。存在証明と
一意性証明がどの定義に対応するかを `IsInitial.ofUniqueHom` の引数まで追えれば完了です。

### Lambekの補題を始性だけから証明する

始代数 `(I,i)` に対し、`F(I)` 上の代数 `(F(I),F(i))` を作り、始性から射 `j:I→F(I)` を得てください。
`j;i=id_I` を始代数から自身への準同型の一意性で示します。残る `i;j=id_{F(I)}` を準同型条件、関手法則、
最初の逆法則から導き、どこにも不動点の存在を別仮定していないことを確認してください。

### 不動点と始代数を分ける反例を探す

自己関手 `F=Id` を考え、全ての対象が `X≅F(X)` を満たす一方、代数圏の始対象であるとは限らないことを
示してください。構造射として異なる自己写像を選ぶ場合も比較します。不動点方程式、`F`-代数、始代数の
三段階で要求されるデータと普遍性を表にし、逆向きの含意が失敗する箇所を説明できれば完了です。
-/

end FormalLab.CategoryFoundations.InitialAlgebras