import Mathlib.CategoryTheory.Functor.Basic
import FormalLab.CategoryTheory.Categories

/-!
# 第46章：関手——圏の構造を保つ写像

群の準同型は積と単位元を保ち、順序写像は比較を保ちます。同じように、圏から圏へ構造を移すには、
対象だけでなく射も移し、恒等射と合成を保たなければなりません。この二層の対応が関手です。
対象の対応だけでは、どの射がどの射へ移るかも、合成した結果が保たれるかも分かりません。

本章では関手の四つの成分を定義し、一対象圏の関手を自然数加法の準同型として計算します。恒等関手と
関手の合成を構成し、反変関手が「射を逆向きに送る例外」ではなく、反対圏を始域とする通常の関手で
あることを明確にします。最後に、対象上で同じ対応をする関手でも射上では異なり得ることを確かめます。

## 対象と射を同時に移す

圏 `C,D` の間の関手 `F:C→D` は、次のデータから成ります。

$$
\begin{aligned}
X\in\operatorname{Ob}(C)&\longmapsto F(X)\in\operatorname{Ob}(D),\\
f:X\to Y&\longmapsto F(f):F(X)\to F(Y),\\
F(\mathrm{id}_X)&=\mathrm{id}_{F(X)},\\
F(g\circ f)&=F(g)\circ F(f).
\end{aligned}
$$

最後の二式を恒等射保存則と合成保存則と呼びます。射の始域・終域が保たれることは、第二行の型に
組み込まれています。関手は対象の内部要素を写す必要はなく、圏に備わる射と合成を保ちます。
-/

namespace FormalLab.CategoryFoundations.Functors

open _root_.CategoryTheory
open FormalLab.CategoryFoundations

universe v₁ v₂ v₃ u₁ u₂ u₃

variable {C : Type u₁} [Category.{v₁} C]
variable {D : Type u₂} [Category.{v₂} D]
variable {E : Type u₃} [Category.{v₃} E]

/-!
mathlibの `C ⥤ D` は、対象写像 `obj`、射写像 `map`、二つの保存則 `map_id` と `map_comp` を
持ちます。数式の `F(f)` は `F.map f` に対応します。
-/

variable (F : C ⥤ D)

example (X : C) : D := F.obj X
example {X Y : C} (f : X ⟶ Y) : F.obj X ⟶ F.obj Y := F.map f
example (X : C) : F.map (𝟙 X) = 𝟙 (F.obj X) := F.map_id X
example {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    F.map (f ≫ g) = F.map f ≫ F.map g := F.map_comp f g

/-!
型が保証するのは、射が正しい始域・終域へ移ることです。二つの等式はさらに、恒等射と合成という
圏の計算を壊さないことを保証します。対象写像と射写像を与えただけでは関手になりません。

## 一対象圏の関手はモノイド準同型である

前章の一対象圏では射は自然数、恒等射は零、合成は加法でした。自然数 `n` を `k*n` へ送る写像は
零と加法を保つので関手になります。対象は一つしかないため、関手の実質的内容は射上の準同型です。
-/

def scaleMorphism (k : Nat) {X Y : AdditiveObject} (f : X ⟶ Y) : X ⟶ Y :=
  show Nat from k * (show Nat from f)

/-- 自然数射を `k` 倍する一対象圏の自己関手。 -/
def scalingFunctor (k : Nat) : AdditiveObject ⥤ AdditiveObject where
  obj X := X
  map f := scaleMorphism k f
  map_id X := by
    rfl
  map_comp f g := by
    change k * ((show Nat from f) + (show Nat from g)) =
      k * (show Nat from f) + k * (show Nat from g)
    exact Nat.mul_add k (show Nat from f) (show Nat from g)

theorem scalingFunctor_maps_three :
    (scalingFunctor 2).map (additiveHom 3) = additiveHom 6 := rfl

example :
    (scalingFunctor 2).map (additiveHom 3 ≫ additiveHom 4) =
      (scalingFunctor 2).map (additiveHom 3) ≫
        (scalingFunctor 2).map (additiveHom 4) := by
  exact (scalingFunctor 2).map_comp (additiveHom 3) (additiveHom 4)

/-!
ここで `map_comp` は分配律 `k(m+n)=km+kn` そのものです。もし射を `n↦n+1` と移せば恒等射
`0` が `1` へ移るので、恒等射保存則に失敗します。対象を正しく移せることと、関手であることの差は
保存則に現れます。

## 恒等関手と合成

各圏 `C` には対象も射も変えない恒等関手 `Id_C:C→C` があります。`F:C→D` と `G:D→E` の合成
`G∘F:C→E` は、対象と射の両方で順に写します。

$$
(G\circ F)(X)=G(F(X)),
\qquad
(G\circ F)(f)=G(F(f)).
$$

保存則は `F` と `G` の保存則を順に使えば従います。mathlibでは射の進行順に `F ⋙ G` と書きます。
-/

variable (G : D ⥤ E)

example : C ⥤ C := 𝟭 C
example : C ⥤ E := F ⋙ G
example (X : C) : (F ⋙ G).obj X = G.obj (F.obj X) := rfl
example {X Y : C} (f : X ⟶ Y) : (F ⋙ G).map f = G.map (F.map f) := rfl

example {X Y : AdditiveObject} (f : X ⟶ Y) :
    (scalingFunctor 2 ⋙ scalingFunctor 3).map f = (scalingFunctor 6).map f := by
  change 3 * (2 * (show Nat from f)) = 6 * (show Nat from f)
  omega

/-!
合成例では対象写像は初めから同じなので、違いが現れ得る射成分を比較しました。二倍してから三倍する
射写像が六倍の射写像と一致することまで検査しています。関手全体の等式を述べるには、対象成分と射成分を
依存する型に沿って比較する外延性がさらに必要です。

## 反変関手は反対圏からの関手である

通常の関手は `f:X→Y` を `F(f):F(X)→F(Y)` へ同じ向きに送るので共変関手とも呼ばれます。
反変関手 `P` は見かけ上

$$
f:X\to Y\quad\longmapsto\quad P(f):P(Y)\to P(X).
$$

と向きを反転します。これを別種の保存則で定義すると理論が二重になります。反対圏を使えば、反変関手は
`P:Cᵒᵖ→D` という通常の関手です。反対圏側ですでに合成順序が反転しているため、関手自身の保存則は
変わりません。
-/

def ContravariantFunctor (C : Type u₁) [Category.{v₁} C]
    (D : Type u₂) [Category.{v₂} D] := Cᵒᵖ ⥤ D

example : ContravariantFunctor C Cᵒᵖ := 𝟭 Cᵒᵖ

/-!
後に導入する前層は `Cᵒᵖ→Type`、固定対象から出るhom関手は反変に振る舞います。「反変」は
個々の射に逆射を要求しません。反対圏で同じ射を逆向きに読み、その上で構造を保つ写像を与えます。

## 対象上の一致だけでは関手を決めない

`scalingFunctor 2` と `scalingFunctor 3` は、唯一の対象をどちらも同じ対象へ送ります。しかし射 `1` の
像はそれぞれ `2` と `3` です。したがって対象写像だけを見て二関手を同一視できません。関手を比較する
には対象成分と射成分の双方が必要であり、次章の自然変換は各対象で射を与えて両者の射作用との整合性を
要求します。

## 要点

* 関手は対象写像と射写像を持ち、恒等射と合成を保つ。
* 射写像の型が始域・終域の保存を表し、二法則が圏の計算の保存を表す。
* 一対象圏の間の関手は、対応するモノイドの準同型として読める。
* 恒等関手と関手合成があり、mathlibの `F ⋙ G` は先に `F`、次に `G` と読む。
* 反変関手は反対圏を始域とする通常の関手であり、射の可逆性を仮定しない。

## 研究史と文献案内

Eilenberg–Mac Lane [EM45] は、代数的位相幾何で現れる構成の自然性を扱うため、圏とともに共変・反変
関手を体系化しました。同論文では関手が単なる対象対応ではなく、恒等写像と合成を保つ射対応を含むことが
明記されています。現代的な反対圏、関手圏、随伴への展開は [MAC98]、本章で用いた宇宙多相な実装と
記法は [MATHLIB] を参照してください。

## 問題

### 保存則を準同型の法則へ翻訳する

一対象圏の射を任意のモノイド `M` とし、関手の `map_id` と `map_comp` をモノイド準同型の二法則へ
翻訳してください。`scalingFunctor` では各法則が自然数のどの等式になったかをLeanの証明から抽出します。
さらに `n↦n+1` がどちらの法則に失敗するかを最小の反例で示し、対象写像だけでは不足する理由まで
説明できれば完了です。

### 合成関手の法則を成分ごとに復元する

`F:C→D`, `G:D→E`, `H:E→K` を置き、`(H∘G)∘F` と `H∘(G∘F)` の対象成分と射成分を展開して
一致を示してください。次に左右の恒等関手との合成を同様に計算します。圏の射の結合律ではなく、
関手を作る写像の合成が結合的であることを使っている箇所を区別し、mathlibの `⋙` 記法へ翻訳します。

### 反変性を反対圏の型として検査する

写像 `f:X→Y`, `g:Y→Z` に対し、反変関手の像の型と合成保存式を書いてください。まず通常の記法で
`P(g∘f)` を展開し、次に `Cᵒᵖ⥤D` の通常の `map_comp` として同じ式を得ます。`f.op` が逆射では
ないことを、非可逆な関数を一つ選んで確認してください。さらに反対圏側で恒等射保存則を展開し、
反変性のために関手法則を追加変更していないことを示して、反変性と可逆性を分離できれば完了です。
-/

end FormalLab.CategoryFoundations.Functors