import Mathlib.CategoryTheory.Opposites
import FormalLab.TypeTheory.TypeClasses

/-!
# 第45章：圏・射・反対圏・宇宙

集合の間の関数、順序の比較、型の間の写像は別々の対象ですが、恒等写像と結合的な合成を持つ点は
共通しています。圏は対象の内部要素を忘れ、対象間を結ぶ射とその合成だけを公理化します。これにより
積・余積などの構成を、集合や型に固有の要素計算から切り離して記述できます。

本章では圏のデータと法則を定義し、mathlibの `Category` と対応づけます。自然数加法から一対象圏を
構成して法則を検査した後、全射の向きを反転する反対圏を導入します。最後に対象の宇宙と射の宇宙を
区別し、小さい圏・大きい圏という語を対象数の有限性と混同しないようにします。

## 圏は対象、射、恒等射、合成から成る

圏 `C` は次のデータを持ちます。

* 対象 `X,Y,…`。
* 各二対象に対する射の集まり `Hom_C(X,Y)`。射 `f` を `f:X→Y` と書く。
* 各対象の恒等射 `id_X:X→X`。
* `f:X→Y` と `g:Y→Z` の合成 `g∘f:X→Z`。

さらに左右単位律と結合律を要求します。

$$
\mathrm{id}_Y\circ f=f,
\qquad
f\circ\mathrm{id}_X=f,
\qquad
h\circ(g\circ f)=(h\circ g)\circ f.
$$

射の等式は同じ始域・終域を持つ射の間でだけ述べます。対象の集まりがあるだけでも、任意の二対象間に
矢印を置いただけでも圏にはなりません。合成の型が合い、三法則を満たす必要があります。
-/

namespace FormalLab.CategoryFoundations

open _root_.CategoryTheory

universe v u

/-!
mathlibでは対象型 `C : Type u` に対し、`X ⟶ Y` が射の型、`𝟙 X` が恒等射、`f ≫ g` が
「先に `f`、次に `g`」という合成です。通常の `g∘f` と順序が逆に見えるので、式を読む際は矢印の
進行順を固定します。
-/

variable {C : Type u} [_root_.CategoryTheory.Category.{v} C]

example (X : C) : X ⟶ X := 𝟙 X

example {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
    (f ≫ g) ≫ h = f ≫ (g ≫ h) := by
  simp

example {X Y : C} (f : X ⟶ Y) : 𝟙 X ≫ f = f := by simp
example {X Y : C} (f : X ⟶ Y) : f ≫ 𝟙 Y = f := by simp

/-!
三つのLean証明は圏の公理を使います。`simp` が公理を発見して書き換えるのであって、任意の二項演算に
対して結合律を証明しているのではありません。`[Category C]` という型クラス引数が、射・演算・法則を
まとめた構造値を供給します。

## 一対象圏はモノイドを圏として読む

対象を一つだけ持つ圏では、全ての射がその対象から自身への射です。射の合成は一つの集合上の結合的な
二項演算となり、恒等射は単位元になります。これはモノイドと同じデータ・法則です。

自然数を射、零を恒等射、加法を合成とする一対象圏を構成します。
-/

inductive AdditiveObject where
  | star
  deriving DecidableEq, Repr

instance : _root_.CategoryTheory.CategoryStruct AdditiveObject where
  Hom _ _ := Nat
  id _ := 0
  comp first second := first + second

instance : _root_.CategoryTheory.Category AdditiveObject where
  id_comp := by
    intro X Y f
    exact Nat.zero_add f
  comp_id := by
    intro X Y f
    exact Nat.add_zero f
  assoc := by
    intro W X Y Z f g h
    exact Nat.add_assoc f g h

def star : AdditiveObject := .star

def additiveHom (n : Nat) : star ⟶ star := n

example (m n : Nat) : additiveHom m ≫ additiveHom n = additiveHom (m + n) := rfl
example : additiveHom 2 ≫ additiveHom 3 ≫ additiveHom 4 = additiveHom 9 := rfl

/-!
圏の結合律は自然数加法の結合律へ、単位律は零の左右単位律へ還元されました。一対象圏の射が可換である
必要はありません。自然数加法を選んだためこの例は可換ですが、一般のモノイドから作る一対象圏では
`f≫g` と `g≫f` が異なり得ます。

## 関数の圏では射が実際の関数である

型を対象、関数を射とする圏では恒等射は恒等関数、合成は関数合成です。しかし一般の圏で射を
「関数」と定義してはいけません。一対象圏の自然数射のように、射が関数でない圏もあります。

圏が具体圏であるとは、ある基礎的な対象の圏への忠実な忘却関手を備えることです。この語は後に関手と
忠実性を定義してから扱います。対象に要素があるという直観を一般の圏へ無断で持ち込みません。

## 反対圏は全ての射を反転する

圏 `C` の反対圏 `Cᵒᵖ` は同じ対象を持ち、射を

$$
\mathrm{Hom}_{\mathcal C^{\mathrm{op}}}(X,Y)
\;\overset{\mathrm{def}}{=}\;
\mathrm{Hom}_{\mathcal C}(Y,X)
$$

と定めます。恒等射は同じで、合成順序は反転します。`f:X→Y` を反対圏の射
`fᵒᵖ:Yᵒᵖ→Xᵒᵖ` として読めます。
-/

variable {X Y Z : C}

example (f : X ⟶ Y) : Opposite.op Y ⟶ Opposite.op X := f.op

example (f : X ⟶ Y) (g : Y ⟶ Z) :
    (f ≫ g).op = g.op ≫ f.op := rfl

example (X : C) : (𝟙 X).op = 𝟙 (Opposite.op X) := rfl

/-!
反対圏は各射へ逆射を追加する構成ではありません。`f.op` は元の `f` を逆向きに読み直した射であり、
`f` が同型であることや逆射を持つことを意味しません。双対原理は、圏の定義と定理を反対圏へ移して
全ての射向きを反転する原理です。

## 対象と射は独立した宇宙レベルを持つ

mathlibの `Category.{v} C` では対象が `Type u`、射 `X⟶Y` が `Type v` に属します。二レベルは独立です。
小さい圏は対象と射を同じ一つの宇宙内で扱える圏を指し、大きい圏はより高い対象宇宙を必要とします。

型の圏は対象が型自身なので、対象の宇宙はその型の要素より一段上がります。「小さい」は対象が有限個、
「大きい」は対象が無限個という意味ではありません。有限性・基数と宇宙サイズを別の分類として扱います。

## 要点

* 圏は対象、hom型、恒等射、合成と左右単位律・結合律から成る。
* 一般の射は関数とは限らず、始域と終域を持つ合成可能な構造である。
* 一対象圏はモノイドと同じデータを持ち、合成がモノイド演算になる。
* 反対圏は射の向きと合成順を反転するが、各射へ逆射を与えない。
* 対象の宇宙と射の宇宙は独立で、圏の大小は有限性とは異なる。

## 研究史と文献案内

Eilenberg–Mac Laneの1945年論文 [EM45] は圏、関手、自然同値を代数的位相幾何の写像比較から
体系的に導入した一次資料です。現在の教科書で用いる反対圏、普遍性、随伴、極限の全体系を同論文一つへ
遡及的に帰属させません。現代的な圏論の標準的展開は [MAC98]、mathlibの宇宙多相な `Category` の
現行APIは [MATHLIB] を参照してください。

## 問題

### 圏の法則を型の整合から検査する

四対象と三射を置き、結合律の両辺について中間対象を一つずつ追ってください。始域・終域が合わず
合成できない射列も一つ作ります。通常記法 `h∘g∘f` とmathlib記法 `f≫g≫h` を相互に翻訳し、
各単位律で使う恒等射の対象を誤らず書いてください。最後に三つの圏法則から一つを除いた構造を考え、
型が合うことだけではその法則を回復できない例を示せれば完了です。

### 別のモノイドから一対象圏を構成する

文字列と連結、整数と加法、正方行列と乗法の一つを選び、`AdditiveObject` と同様の圏を構成してください。
恒等射、合成、三法則を元のモノイド法則へ対応づけます。非可換な例では二射の合成順を計算し、
圏の公理が可換律を要求しないことをLeanの不等式または具体的行列から確認すれば完了です。

### 反対圏で定理を双対化する

`f≫g≫h` を反対圏へ移し、射の型と合成順を全段階で書いてください。始対象の定義を反対圏で読み直すと
終対象になることを、既習の存在一意性から説明します。`f.op` と逆射 `f⁻¹` の型・存在条件を比較し、
反対圏を群oid化と混同していないことを反例とともに示してください。非全単射な関数を射として選び、
その `op` は常に作れる一方、逆関数は作れないことまで型と論理式で区別できれば完了です。
-/

end FormalLab.CategoryFoundations