import Mathlib.CategoryTheory.Monoidal.Types.Basic
import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
import FormalLab.CategoryTheory.NaturalTransformations

/-!
# 第64章：モノイダル圏——テンソル積と整合性

集合の直積、ベクトル空間のテンソル積、自己関手の合成には共通した形があります。二対象から一対象を作る
二項演算と、その演算に対する単位対象があることです。しかし一般には `(X⊗Y)⊗Z` と `X⊗(Y⊗Z)` は
等号で一致せず、標準的な同型によって結ばれます。単位についても `I⊗X=X` と `X⊗I=X` を等号ではなく
同型として表します。

同型を選ぶだけでは不十分です。四対象の括弧を付け替える複数の経路や、単位対象を除く複数の経路が同じ射を
与えなければ、複合した式の意味が経路に依存します。モノイダル圏はテンソル積、単位対象、結合子、単位子に、
五角形公理と三角形公理を課した圏です。本章ではまず集合の直積から必要なデータを取り出し、射上のテンソル、
自然性、二つの整合性公理へ進みます。最後にMac Laneの整合性定理が括弧の計算をどこまで一意化するかを扱います。

## 対象だけの二項演算では足りない

圏 `C` 上のテンソル積は対象 `X,Y` を `X⊗Y` へ送るだけでなく、射 `f:X→X'`, `g:Y→Y'` を

$$
f\otimes g:X\otimes Y\longrightarrow X'\otimes Y'.
$$

へ送ります。恒等射と合成を保つので、非カリー化すれば関手 `C×C→C` です。対象対応だけを指定すると、
同型や可換図式を射に沿って移送できず、モノイダル構造にはなりません。
-/

namespace FormalLab.CategoryFoundations.MonoidalCategories

open _root_.CategoryTheory
open _root_.CategoryTheory.MonoidalCategory
open scoped MonoidalCategory

universe v u

variable {C : Type u} [Category.{v} C] [MonoidalCategory C]
variable {W X Y Z W' X' Y' Z' : C}

example (X Y : C) : C := X ⊗ Y

example (f : W ⟶ X) (g : Y ⟶ Z) : W ⊗ Y ⟶ X ⊗ Z := f ⊗ₘ g

example (f₁ : W ⟶ X) (f₂ : X ⟶ X') (g₁ : Y ⟶ Z) (g₂ : Z ⟶ Z') :
    (f₁ ⊗ₘ g₁) ≫ (f₂ ⊗ₘ g₂) = (f₁ ≫ f₂) ⊗ₘ (g₁ ≫ g₂) :=
  MonoidalCategory.tensorHom_comp_tensorHom f₁ g₁ f₂ g₂

example (X Y : C) : (𝟙 X) ⊗ₘ (𝟙 Y) = 𝟙 (X ⊗ Y) :=
  MonoidalCategory.id_tensorHom_id X Y

/-!
これら二式はテンソル積が射の恒等と合成を保つことを述べます。`⊗` は対象、`⊗ₘ` は射に使うLeanの記法です。
数学では両方を同じ記号で書くことが多いので、式の始域と終域からどちらかを判断します。

一方の対象を固定した作用も頻繁に使います。`X ◁ g` は左側に対象 `X` を固定し、`f ▷ Y` は右側に
対象 `Y` を固定します。射のテンソルは二つの作用の合成として表せます。
-/

example (X : C) (g : Y ⟶ Z) : X ⊗ Y ⟶ X ⊗ Z := X ◁ g

example (f : W ⟶ X) (Y : C) : W ⊗ Y ⟶ X ⊗ Y := f ▷ Y

example (f : W ⟶ X) (g : Y ⟶ Z) :
    f ⊗ₘ g = (f ▷ Y) ≫ (X ◁ g) :=
  MonoidalCategory.tensorHom_def f g

/-!
二変数関手の関手性により、先に左変数を動かしても先に右変数を動かしても同じ射になります。これは
interchangeまたはexchangeと呼ばれる交換法則で、テンソル積が二つの独立した射作用を一つにまとめられる理由です。

## 単位対象は始対象や終対象とは限らない

モノイダル圏には対象 `I` があり、各 `X` に対して `I⊗X≅X` と `X⊗I≅X` を与えます。`I` はテンソル積に
関する単位であり、圏の始対象または終対象であるとは限りません。例えばベクトル空間のテンソル積では基礎体が
単位対象ですが、零ベクトル空間ではありません。
-/

example : C := 𝟙_ C

example (X : C) : (𝟙_ C) ⊗ X ≅ X := λ_ X

example (X : C) : X ⊗ (𝟙_ C) ≅ X := ρ_ X

/-!
左単位子 `λ_X` と右単位子 `ρ_X` は対象ごとにばらばらな同型ではありません。射 `f:X→Y` に対して
次の正方形が可換し、単位子が自然であることを要求します。

$$
(I\otimes f);\lambda_Y=\lambda_X;f,
\qquad
(f\otimes I);\rho_Y=\rho_X;f.
$$
-/

example (f : X ⟶ Y) :
    (𝟙_ C) ◁ f ≫ (λ_ Y).hom = (λ_ X).hom ≫ f :=
  MonoidalCategory.leftUnitor_naturality f

example (f : X ⟶ Y) :
    f ▷ (𝟙_ C) ≫ (ρ_ Y).hom = (ρ_ X).hom ≫ f :=
  MonoidalCategory.rightUnitor_naturality f

/-!
## 結合子は括弧を付け替える自然同型である

三対象に対して結合子

$$
\alpha_{X,Y,Z}:(X\otimes Y)\otimes Z
  \mathbin{\cong}X\otimes(Y\otimes Z).
$$

を指定します。これは結合律の等式ではありません。左辺と右辺は異なる対象であってよく、選ばれた同型とその
逆射によって往復します。三本の射をテンソルしたとき、先に射を適用してから括弧を変える経路と、先に括弧を
変えてから射を適用する経路が一致することが結合子の自然性です。
-/

example (X Y Z : C) : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z) := α_ X Y Z

example (f : W ⟶ W') (g : X ⟶ X') (h : Y ⟶ Y') :
    ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ W' X' Y').hom =
      (α_ W X Y).hom ≫ (f ⊗ₘ (g ⊗ₘ h)) :=
  MonoidalCategory.associator_naturality f g h

/-!
## 五角形公理は四項の括弧変更を一意にする

四対象 `W,X,Y,Z` の括弧を `((W⊗X)⊗Y)⊗Z` から `W⊗(X⊗(Y⊗Z))` へ変えるには、結合子を二回使う
短い経路と三回使う長い経路があります。五角形公理はこの二経路が等しいことを要求します。

$$
(\alpha_{W,X,Y}\otimes Z);\alpha_{W,X\otimes Y,Z};
  (W\otimes\alpha_{X,Y,Z})
=
\alpha_{W\otimes X,Y,Z};\alpha_{W,X,Y\otimes Z}.
$$

図の辺は適切な結合子、または結合子を一方の対象でテンソルした射です。
-/

example (W X Y Z : C) :
    (α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom =
      (α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom :=
  MonoidalCategory.pentagon W X Y Z

/-!
結合子が各三対象について存在するだけでは五角形は従いません。任意に同型を選ぶと、四項の式を比較する射が
選んだ経路に依存し得ます。五角形は局所的な一公理によって、任意個の対象の括弧変更を制御する基礎になります。

## 三角形公理は結合子と単位子を両立させる

`(X⊗I)⊗Y` から `X⊗Y` へ進むには、右単位子を左側へ作用させる経路と、結合子の後に左単位子を作用させる
経路があります。三角形公理は二経路が一致することを要求します。
-/

example (X Y : C) :
    (α_ X (𝟙_ C) Y).hom ≫ X ◁ (λ_ Y).hom = (ρ_ X).hom ▷ Y :=
  MonoidalCategory.triangle X Y

/-!
左単位子、右単位子、結合子を互いに無関係に選ぶと三角形が失敗し得ます。従ってモノイダル圏の公理は、
テンソルの結合性と単位性を別々に述べるだけでなく、両者の相互作用も固定します。

## `Type` の直積はモノイダル構造の具体例である

型と関数の圏では `X⊗Y=X×Y`、単位対象を一要素型 `PUnit` とすればモノイダル圏になります。結合子は
`((x,y),z)` を `(x,(y,z))` へ移し、単位子は余分な一要素成分を除きます。
-/

theorem type_tensor_is_product {A B : Type u} : (A ⊗ B) = (A × B) := rfl

theorem type_tensor_unit_is_punit : 𝟙_ (Type u) = PUnit := rfl

theorem type_associator_apply {A B C : Type u} (a : A) (b : B) (c : C) :
    (α_ A B C).hom ((a, b), c) = (a, (b, c)) := rfl

theorem type_leftUnitor_apply {A : Type u} (a : A) :
    (λ_ A).hom (PUnit.unit, a) = a := rfl

theorem type_tensorHom_apply {A B T U : Type u}
    (f : A ⟶ B) (g : T ⟶ U) (a : A) (t : T) :
    dsimp% (f ⊗ₘ g) (a, t) = (f a, g t) := rfl

/-!
この例ではテンソル積が圏論的な積でもあります。そのため対角射や射影を使えますが、それらは一般の
モノイダル圏のデータではありません。ベクトル空間の通常のテンソル積には、二つのベクトルを同じ入力から
複製する自然な対角写像はありません。モノイダル積をデカルト積と同一視すると、線形性や資源の非複製性を
失います。

## 整合性定理は構造射だけの図式を決定する

Mac Laneの整合性定理は、構造射だけから作られる同じ始域・終域の標準射が等しいことを述べます。ここで構造射
には結合子と単位子、およびそれらの逆射を含めます。恒等射から始め、これらをテンソルと合成で組み立てます。
例えば単位対象自身に対する左右の単位子は一致します。
-/

theorem unitors_coincide : (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom :=
  MonoidalCategory.unitors_equal

/-!
Leanの `monoidal_coherence` は、この範囲の等式を正規化して証明します。これは任意の射を含む全図式が自動的に
可換するという意味ではありません。非構造射が入ればその自然性や追加法則が必要です。また整合性定理は
結合子を等号へ変更するものではなく、結合子から作る比較射の一意性を保証します。

## モノイダル圏とモノイド対象を区別する

モノイダル圏はテンソル積を持つ周囲の圏です。その内部で対象 `M` と射 `I→M`, `M⊗M→M` が単位律と結合律を
満たすとき、`M` をモノイド対象と呼びます。前者は圏全体の構造、後者はその圏内の一対象が持つ代数構造です。
`Type` のデカルト積に関するモノイド対象は通常のモノイドを回収しますが、一般のテンソル積では環、代数、
作用素など別の構造を表します。

## 要点

* テンソル積は対象の二項演算だけでなく、射の恒等と合成を保つ二変数関手である。
* 単位対象 `I` は `I⊗X≅X≅X⊗I` を満たすが、始対象や終対象である必要はない。
* 結合子は `(X⊗Y)⊗Z≅X⊗(Y⊗Z)` という自然同型であり、対象の等号ではない。
* 五角形公理は四項の括弧変更を、三角形公理は結合子と左右の単位子の相互作用を整合させる。
* 整合性定理は構造射だけから作る標準図式の可換性を与えるが、任意の射の法則を自動的には証明しない。
* デカルト積はモノイダル積の一例であり、複製や破棄の構造を一般のテンソル積へ持ち込めない。

## 研究史と文献案内

Mac Lane [MAC63] は自然な結合性・可換性の整合条件を研究し、後にモノイダル圏の整合性定理として体系化される
基礎を与えました。現在の定義、五角形・三角形公理、厳密化を含む標準的な扱いは [MAC98] を参照してください。
同論文には対称性も含まれますが、本章のモノイダル圏は交換子を仮定しません。Leanの `MonoidalCategory`,
`tensorHom`, `associator`, `leftUnitor`, `rightUnitor` と整合性タクティクは [MATHLIB] の現行APIに従います。

## 問題

### `Type` の五角形を要素ごとに証明する

四つの型 `A,B,C,D` と要素 `a,b,c,d` を固定し、`(((a,b),c),d)` から `a,(b,(c,d))` へ至る五角形の
二経路を関数として書いてください。各結合子の適用後の要素を一段ずつ記録し、両経路が同じ入れ子対へ到達する
ことを示します。Leanでは関数外延性を使う証明と `MonoidalCategory.pentagon` を使う証明を比較し、具体計算と
抽象公理の役割を区別できれば完了です。

### 単位対象と終対象の違いを説明する

体 `k` 上のベクトル空間と線形写像の圏を考え、テンソル単位が `k`、零対象が零ベクトル空間であることを
確認してください。`k→V` という線形写像が `V` のベクトルの選択に対応して一般には一意でないことから、`k` が
終対象でないことを示します。`I⊗V≅V` と「全ての対象から `I` への射が一意」を明確に分離できれば完了です。

### 対象対応だけではモノイダル構造にならない理由を示す

圏 `C` 上に二項対象対応 `T:C×C→C` の対象部分だけが与えられたと仮定します。結合子の自然性を書くために
必要な四つの射作用を列挙し、`T(f,g)` がなければ可換正方形の辺さえ定義できないことを示してください。さらに
射作用を与えても恒等・合成保存がなければ、五角形を射の合成として安定に移送できないことを説明します。

### 整合性定理の適用範囲を判定する

結合子と単位子だけからなる等式、任意の射 `f` を単位子へ通す自然性の等式、モノイド対象の乗法 `μ` を含む
結合律の三例を用意してください。どれが純粋な整合性だけで従い、どれが自然性またはモノイド対象の公理を必要と
するかを分類します。それぞれをLeanで `monoidal_coherence`, `simp`, 明示した仮定のいずれかを使って証明し、
自動化が数学的仮定を追加していないことを説明できれば完了です。
-/

end FormalLab.CategoryFoundations.MonoidalCategories