import Mathlib.CategoryTheory.Functor.Category
import FormalLab.CategoryTheory.Functors

/-!
# 第47章：自然変換と関手圏

二つの関手 `F,G:C→D` が同じ圏の間を結んでいても、各対象を別の対象へ送り得ます。そこで各対象
`X` ごとに射 `α_X:F(X)→G(X)` を選べば、関手を点ごとに比較できそうです。しかし成分を互いに
無関係に選ぶだけでは、`C` の射を先に移す場合と、成分で移った後に射を移す場合が一致しません。

自然変換は、全対象に一つずつ成分射を与え、全射についてこの二経路が一致するよう要求します。本章では
自然性の可換正方形を型と等式から導き、一対象圏で各辺を数値計算します。続いて恒等自然変換と垂直合成を
構成し、関手を対象、自然変換を射とする関手圏が生まれることを確かめます。

## 成分射を自然性で結ぶ

関手 `F,G:C→D` の間の自然変換 `α:F⇒G` は、各対象 `X` に対する成分

$$
\alpha_X:F(X)\to G(X)
$$

と、各射 `f:X→Y` に対する自然性条件から成ります。

$$
\alpha_Y\circ F(f)=G(f)\circ\alpha_X
\qquad(f:X\to Y).
$$

図の左上から右下へ進む二経路が等しいので、この正方形を可換と呼びます。成分の存在だけではなく、
始域の全射 `f` に対して同じ式が成り立つことが中心条件です。
-/

namespace FormalLab.CategoryFoundations.NaturalTransformations

open _root_.CategoryTheory
open FormalLab.CategoryFoundations
open FormalLab.CategoryFoundations.Functors

universe v₁ v₂ u₁ u₂

variable {C : Type u₁} [Category.{v₁} C]
variable {D : Type u₂} [Category.{v₂} D]
variable {F G H : C ⥤ D}

/-!
mathlibの `NatTrans F G` は成分 `app X` と自然性 `naturality f` を持ちます。合成記号 `≫` は
「先に左、次に右」なので、数式の式と同じ正方形を次の順序で表します。
-/

variable (α : NatTrans F G)

example (X : C) : F.obj X ⟶ G.obj X := α.app X

example {X Y : C} (f : X ⟶ Y) :
    F.map f ≫ α.app Y = α.app X ≫ G.map f := α.naturality f

/-!
等式の左辺は上辺の `F(f)` の後に右辺の `α_Y`、右辺は左辺の `α_X` の後に下辺の `G(f)` を
進みます。図を暗記する代わりに、各合成の中間対象を合わせれば向きを復元できます。

## 一対象圏で自然性を計算する

前章の `scalingFunctor k` からそれ自身への自然変換を作ります。唯一の対象で成分を自然数 `c` とすると、
射 `n` に対する自然性は

$$
kn+c=c+kn.
$$

です。自然数加法の可換性により、任意の `c` が成分になれます。
-/

/-- `scalingFunctor k` の中心にある射 `c` が定める自然自己変換。 -/
def centralTransformation (k c : Nat) :
    NatTrans (scalingFunctor k) (scalingFunctor k) where
  app X := show Nat from c
  naturality := by
    intro X Y f
    change k * (show Nat from f) + c = c + k * (show Nat from f)
    exact Nat.add_comm _ _

example : (centralTransformation 2 5).app star = additiveHom 5 := rfl

example :
    (scalingFunctor 2).map (additiveHom 3) ≫
        (centralTransformation 2 5).app star =
      (centralTransformation 2 5).app star ≫
        (scalingFunctor 2).map (additiveHom 3) := by
  exact (centralTransformation 2 5).naturality (additiveHom 3)

/-- 対象写像が同じでも、二倍関手から三倍関手への自然変換は存在しません。 -/
theorem noTransformationTwoToThree :
    ¬Nonempty (NatTrans (scalingFunctor 2) (scalingFunctor 3)) := by
  rintro ⟨transformation⟩
  have naturality := transformation.naturality (additiveHom 1)
  change 2 + (show Nat from transformation.app star) =
    (show Nat from transformation.app star) + 3 at naturality
  omega

/-!
この例では全ての成分候補が自然になりましたが、それは射の加法が可換だからです。一般の一対象圏、すなわち
一般のモノイドでは、自己変換の成分は全ての射と可換する中心の元でなければなりません。自然性は装飾的な
条件ではなく、点ごとの候補から構造と両立するものだけを選びます。

また `scalingFunctor 2` から `scalingFunctor 3` への成分 `c` を置くと、全ての `n` に対して
`2n+c=c+3n` が必要です。`n=1` ですでに不可能なので、対象写像が一致しても自然変換が存在するとは
限りません。

## 恒等自然変換と垂直合成

各関手 `F` には、各成分を恒等射とする恒等自然変換 `id_F:F⇒F` があります。`α:F⇒G` と
`β:G⇒H` は対象ごとに成分を合成して、垂直合成 `β∘α:F⇒H` を作ります。

$$
(\beta\circ\alpha)_X=\beta_X\circ\alpha_X.
$$

自然性は `α` と `β` の可換正方形を上下に貼り合わせれば従います。「垂直」という語は、二つの正方形を
縦に積む図式に由来します。
-/

example : NatTrans F F := NatTrans.id F

example (β : NatTrans G H) : NatTrans F H := NatTrans.vcomp α β

example (β : NatTrans G H) (X : C) :
    (NatTrans.vcomp α β).app X = α.app X ≫ β.app X := rfl

example :
    (NatTrans.vcomp (centralTransformation 2 3) (centralTransformation 2 4)).app star =
      additiveHom 7 := rfl

/-!
最後の計算は成分 `3` と `4` の合成が加法 `3+4` であることを示します。恒等自然変換と垂直合成の
単位律・結合律は、各対象における圏 `D` の単位律・結合律へ還元されます。

## 関手圏

圏 `C,D` を固定すると、関手 `C→D` を対象、自然変換を射として圏 `[C,D]` を作れます。恒等射は
恒等自然変換、射の合成は垂直合成です。mathlibでは関手の型 `C ⥤ D` 自身に圏構造が入り、
`F ⟶ G` を `NatTrans F G` と読めます。関手圏の射が個々の成分ではなく、自然性を証明した成分族であることが
重要です。
-/

example : Category (C ⥤ D) := inferInstance
example : (F ⟶ G) = NatTrans F G := rfl
example (β : G ⟶ H) : F ⟶ H := α ≫ β
example (β : G ⟶ H) (X : C) : (α ≫ β).app X = α.app X ≫ β.app X := rfl

/-!
関手圏の射の宇宙は、始域の対象宇宙と終域の射宇宙の双方に依存します。自然変換が「全ての対象 `X` に
対する成分」を持つためです。宇宙レベルは対象数の有限・無限ではなく、量化する型と成分射が属する型の
階層を記録します。

## 自然性と「自然な式」

日常語で式を自然と感じることは、自然変換であることの証明ではありません。自然性は、始域の全射に対する
明示的な可換等式です。基底や座標などの追加選択に依存する構成は、その選択を保たない射に対して正方形が
可換にならず、自然変換を定めないことがあります。後の米田の補題、随伴、極限では、この全射に対する
整合性が定理の型そのものになります。

## 要点

* 自然変換 `α:F⇒G` は成分 `α_X:F(X)→G(X)` と、全射に対する自然性から成る。
* 自然性は `F(f);α_Y` と `α_X;G(f)` が等しいという可換正方形である。
* 成分を点ごとに選べても、自然性を満たさなければ自然変換にはならない。
* 恒等自然変換と垂直合成により、関手を対象とする関手圏ができる。
* 関手圏の射は一つの成分射ではなく、自然性を備えた成分族である。

## 研究史と文献案内

Eilenberg–Mac Laneの1945年論文 [EM45] の題名は “General Theory of Natural Equivalences” です。
同論文では自然性が圏と関手を導入する動機の中心にあります。その用語法と現代の任意の自然変換をそのまま
同一視せず、現在の成分族・可換正方形・関手圏による定式化には [MAC98] を参照してください。
mathlibの `NatTrans` と関手圏の宇宙レベルおよび合成APIは [MATHLIB] に対応します。

## 問題

### 可換正方形を型から再構成する

`f:X→Y` と `α:F⇒G` だけを出発点に、四対象 `F(X),F(Y),G(X),G(Y)` と四射の型を書いてください。
左上から右下への二経路を型の合う順に合成し、自然性の等式を得ます。数式の `∘` とmathlibの `≫` の
双方で書いてください。成分の添字を交換するとどこで型が合わなくなるかを特定し、可換という語を
図の印象ではなく同じ始域・終域を持つ二射の等式として説明できれば完了です。

### 一対象圏で自然変換の存在を判定する

`scalingFunctor k` から `scalingFunctor l` への成分を自然数 `c` と仮定し、自然性を全ての自然数 `n` に
関する方程式へ翻訳してください。`k=l` なら任意の `c` が使える理由を証明し、`k≠l` なら `n=1` から
矛盾を導きます。次に非可換モノイドへ一般化し、自己変換の成分が中心に属する条件を導出してください。

### 関手圏の圏法則を成分で証明する

三つの自然変換 `α:F⇒G`, `β:G⇒H`, `γ:H⇒K` を置き、垂直合成の結合律を各対象 `X` の成分で
展開してください。左右単位律も同様に恒等自然変換の成分へ還元します。各等式が終域圏のどの圏公理から
従うかを明記し、自然変換全体の等式へ戻す際に成分外延性が必要であることを説明できれば完了です。
-/

end FormalLab.CategoryFoundations.NaturalTransformations