import Mathlib.CategoryTheory.Enriched.Basic
import FormalLab.CategoryTheory.MonoidalCategories

/-!
# 第65章：豊穣圏——hom集合を構造ある対象へ置き換える

通常の圏では二対象 `X,Y` の間の射を集合 `Hom(X,Y)` に集めます。しかし数学で射が持つ構造は、集合だけでは
表せないことがあります。線形写像全体はベクトル空間をなし、連続写像全体には位相を入れられます。距離空間では
二点間の関係を一つの非負実数で測れます。これらの追加構造を忘れて集合へ落とす前に、homそのものを構造ある
対象として扱うのが豊穣化（enrichment）です。

モノイダル圏 `V` を値の世界として選びます。`V`-豊穣圏では `Hom(X,Y)` は集合ではなく `V` の対象です。
恒等射はテンソル単位からhom対象への射、合成はhom対象二つのテンソル積から第三のhom対象への射になります。
本章ではこの型の変化から単位律・結合律を再構成し、豊穣関手と豊穣自然変換へ進みます。最後に、通常の
自然変換の型と、自然変換を集める豊穣hom対象とを区別し、後者の存在に極限が必要な理由を明らかにします。

## homは集合でなく値圏の対象になる

モノイダル圏 `(V,⊗,I)` と対象の型 `C` を固定します。`V`-豊穣圏の第一のデータは

$$
\underline{\operatorname{Hom}}_{\mathcal V}(X,Y)\in\mathcal V.
$$

です。右辺は `V` の射の集合ではなく、`V` の対象です。例えば `V=Type` なら型、`V` がベクトル空間の圏なら
ベクトル空間になります。
-/

namespace FormalLab.CategoryFoundations.EnrichedCategories

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

noncomputable section

universe w v u

variable (V : Type v) [Category.{w} V] [MonoidalCategory V]
variable (C : Type u) [EnrichedCategory V C]

example (X Y : C) : V := X ⟶[V] Y

/-!
Leanの `X ⟶[V] Y` は豊穣hom対象を表します。通常の `X ⟶ Y` は二対象間の射の型を表すため、両者の
括弧と添字を省略できません。値圏 `V` が具体圏であっても、hom対象の要素をただちに `C` の射とみなすのでは
なく、まずテンソル単位 `I` から出る一般化要素として取り出します。

## 恒等射はテンソル単位からの一般化要素である

通常の圏では `id_X∈Hom(X,X)` と書きます。集合の要素 `x∈S` は関数 `1→S` と同じ情報なので、豊穣化すると

$$
j_X:I\longrightarrow\underline{\operatorname{Hom}}_{\mathcal V}(X,X).
$$

になります。ここで `I` は `V` のテンソル単位です。
-/

example (X : C) : (𝟙_ V) ⟶ X ⟶[V] X := eId V X

/-!
この射をhom対象内部の「要素」と呼ぶことはありますが、`V` が具体圏でない場合に集合論的な要素があるとは
限りません。`I→A` という射そのものが一般化要素です。

## 合成はhom対象間の射である

通常の合成は関数

$$
\operatorname{Hom}(X,Y)\times\operatorname{Hom}(Y,Z)
\longrightarrow\operatorname{Hom}(X,Z)
$$

です。直積を値圏のテンソル積へ置き換えると、豊穣合成は

$$
m_{X,Y,Z}:
\underline{\operatorname{Hom}}(X,Y)\otimes
\underline{\operatorname{Hom}}(Y,Z)
\longrightarrow\underline{\operatorname{Hom}}(X,Z).
$$

となります。
-/

example (X Y Z : C) :
    ((X ⟶[V] Y) ⊗ (Y ⟶[V] Z)) ⟶ (X ⟶[V] Z) :=
  eComp V X Y Z

/-!
合成の入力順はmathlibの図式順 `f ≫ g` に合わせて、`X→Y` が左、`Y→Z` が右です。値圏のテンソル積が
対称であるとは仮定しないため、この順序は交換できません。

## 単位律には単位子が現れる

`Hom(X,Y)` に恒等射を左から合成するには、まず左単位子の逆射で

$$
\underline{\operatorname{Hom}}(X,Y)
\longrightarrow I\otimes\underline{\operatorname{Hom}}(X,Y)
$$

へ移り、`j_X⊗id`、次に豊穣合成を適用します。この合成がhom対象の恒等射になることが左単位律です。
右単位律では右単位子を使います。
-/

example (X Y : C) :
    (λ_ (X ⟶[V] Y)).inv ≫ eId V X ▷ _ ≫ eComp V X X Y =
      𝟙 (X ⟶[V] Y) :=
  e_id_comp V X Y

example (X Y : C) :
    (ρ_ (X ⟶[V] Y)).inv ≫ _ ◁ eId V Y ≫ eComp V X Y Y =
      𝟙 (X ⟶[V] Y) :=
  e_comp_id V X Y

/-!
通常の式 `id;f=f` では積と単位集合の同型を省略しています。豊穣化した式は、省略されていた単位子と
テンソル作用を露出させます。これは余計な実装詳細ではなく、一般のモノイダル圏で始域と終域を一致させるために
必要な数学的データです。

## 結合律には結合子が現れる

三本のhom対象を合成する二経路を比較します。左二本を先に合成する経路と右二本を先に合成する経路では、
テンソル積の括弧が異なります。結合子で始域を揃えた後、二経路が一致することを要求します。
-/

example (W X Y Z : C) :
    (α_ _ _ _).inv ≫ eComp V W X Y ▷ _ ≫ eComp V W Y Z =
      _ ◁ eComp V X Y Z ≫ eComp V W X Z :=
  e_assoc V W X Y Z

/-!
モノイダル圏の五角形・三角形公理があるため、この三項の結合律から任意長の合成を整合的に扱えます。
豊穣圏の法則と値圏の整合性公理は役割が異なります。前者はhom対象の合成を制御し、後者はテンソル式の
括弧変更と単位除去を制御します。

## `Type`-豊穣圏は通常の圏を回収する

`V=Type` とし、テンソル積を直積、単位を一要素型とします。hom対象は射の型になり、`PUnit→Hom(X,X)` は
恒等射を一つ選ぶ関数、`Hom(X,Y)×Hom(Y,Z)→Hom(X,Z)` は通常の合成関数です。従って `Type`-豊穣圏の構造と
通常の圏構造は同値です。
-/

example (D : Type u) :
    EnrichedCategory (Type w) D ≃ Category.{w} D :=
  enrichedCategoryTypeEquivCategory D

/-!
この同値は全ての豊穣圏が通常の圏にすぎないという意味ではありません。`Type` の直積という特定の値圏を
選んだ場合だけ、hom対象がそのまま射の型になります。

## 一般の豊穣圏に「台圏」が自動であるとは限らない

hom対象 `Hom_V(X,Y)` から通常の射を取り出す標準候補は

$$
\operatorname{Hom}_{\mathcal C_0}(X,Y)=
\operatorname{Hom}_{\mathcal V}
\!\left(I,\underline{\operatorname{Hom}}_{\mathcal V}(X,Y)\right).
$$

です。mathlibの `ForgetEnrichment V C` はこの一般化要素を射とする通常の圏を構成します。
-/

example : Type u := ForgetEnrichment V C

example (X Y : ForgetEnrichment V C) :
    (X ⟶ Y) =
      ((𝟙_ V) ⟶ (ForgetEnrichment.to V X ⟶[V] ForgetEnrichment.to V Y)) :=
  rfl

/-!
名称に「忘却」とありますが、`V` から `Type` への任意の既存の忘却関手を使うわけではありません。テンソル単位
からのhom関手 `Hom_V(I,-)` を使います。具体圏の通常の台集合関手と一致する例は多いものの、一般には区別が
必要です。また豊穣圏の定義自体は、対象型 `C` に先に通常の `Category` 構造があることを要求しません。

## 豊穣関手はhom対象間の射を持つ

`V`-豊穣圏 `C,D` の間の豊穣関手 `F` は対象写像と、各対象対に対する `V` の射

$$
F_{X,Y}:\underline{\operatorname{Hom}}_{\mathcal C}(X,Y)
\longrightarrow
\underline{\operatorname{Hom}}_{\mathcal D}(F X,F Y).
$$

を持ちます。この射は豊穣恒等射と豊穣合成を保存します。
-/

variable {C}
variable {D : Type u} [EnrichedCategory V D]
variable (F : EnrichedFunctor V C D)

example (X : C) : D := F.obj X

example (X Y : C) : (X ⟶[V] Y) ⟶ (F.obj X ⟶[V] F.obj Y) :=
  F.map X Y

example (X : C) :
    eId V X ≫ F.map X X = eId V (F.obj X) :=
  F.map_id X

example (X Y Z : C) :
    eComp V X Y Z ≫ F.map X Z =
      (F.map X Y ⊗ₘ F.map Y Z) ≫ eComp V (F.obj X) (F.obj Y) (F.obj Z) :=
  F.map_comp X Y Z

/-!
通常の関手の `map` が各射を一つずつ写すのに対し、豊穣関手の `map X Y` はhom対象全体の構造を保つ
`V`-射です。例えばベクトル空間に豊穣化された圏では、射の写像が線形であることまで保持します。

恒等豊穣関手と豊穣関手の合成も構成できます。合成のhom作用は `V` の射の通常の合成です。
-/

example : EnrichedFunctor V C C := EnrichedFunctor.id V C

example {E : Type u} [EnrichedCategory V E] (G : EnrichedFunctor V D E) :
    EnrichedFunctor V C E :=
  F.comp V G

/-!
## `Type`-豊穣関手は通常の関手を回収する

値圏を `Type` にすると、hom対象間の関数が通常の射写像になり、二保存則も通常の関手法則になります。
-/

attribute [local instance] categoryOfEnrichedCategoryType

example {C D : Type u} [EnrichedCategory (Type w) C]
    [EnrichedCategory (Type w) D] :
    EnrichedFunctor (Type w) C D ≃ C ⥤ D :=
  enrichedFunctorTypeEquivFunctor

/-!
## 豊穣自然変換の成分は一般化要素である

二つの豊穣関手 `F,G:C→D` の間の豊穣自然変換は、各 `X` に成分

$$
\alpha_X:I\longrightarrow
\underline{\operatorname{Hom}}_{\mathcal D}(F X,G X).
$$

を持ち、豊穣化された自然性条件を満たします。これは台圏 `ForgetEnrichment V D` における通常の自然変換と
同じ情報です。mathlibの基本APIはこの型を `EnrichedNatTrans F G` として保持します。
-/

variable (G : EnrichedFunctor V C D)

example : Type _ := EnrichedNatTrans F G

example (α : EnrichedNatTrans F G) : F.forget ⟶ G.forget := α.out

example (α : EnrichedNatTrans F G) (X : C) :
    (𝟙_ V) ⟶ (F.obj X ⟶[V] G.obj X) :=
  ForgetEnrichment.homTo V (α.out.app (ForgetEnrichment.of V X))

/-!
成分の自然性は、`F` がhom対象へ与える射と `G` が与える射を、豊穣合成を介して比較する等式です。
`EnrichedNatTrans` が通常の自然変換を内部に持つ実装は、一般化要素を射とする台圏を既に構成したため可能です。
数学的定義を通常の自然性へ弱めたわけではありません。

## 自然変換の型と自然変換のhom対象は異なる

`EnrichedNatTrans F G` はLeanの一つの型です。さらに豊穣関手全体を `V`-豊穣圏にしたいなら、自然変換を
集める `V` の対象 `Nat_V(F,G)` が必要です。望ましい関係は

$$
\operatorname{EnrichedNatTrans}(F,G)
\cong
\operatorname{Hom}_{\mathcal V}
\!\left(I,\underline{\operatorname{Nat}}_{\mathcal V}(F,G)\right).
$$

です。このhom対象は一般に、各 `Hom_D(FX,GX)` を自然性条件で結ぶendとして構成されます。そのため値圏に
必要な極限が存在しなければなりません。

現行mathlibの基本APIは、適切な組紐構造のもとで、この未知のhom対象の米田像に当たる前層を構成します。
hom対象そのものを無条件に選んではいません。
-/

section GradedTransformations

variable [BraidedCategory V]

example : Vᵒᵖ ⥤ Type (max u w) := enrichedNatTransYoneda F G

end GradedTransformations

/-!
この実装境界は数学的な存在条件を反映します。自然変換の成分族という型が作れることから、その型を表現する
`V`-対象が自動的に存在すると推論してはいけません。`Type` では必要なendを型として構成でき、通常の自然変換型が
hom対象になりますが、一般の値圏では完備性やサイズ条件を確認します。

## 前順序と距離空間は豊穣化の形を示す

二値の真理値を `false≤true`、テンソルを論理積、単位を真とするモノイダル順序で考えると、hom対象は
「`x≤y` が成り立つか」という真理値になります。恒等射は反射性、合成は推移性を表し、豊穣圏は前順序を
回収します。

非負拡大実数を順序を反転して並べ、テンソルを加法、単位を零とすると、hom対象を距離 `d(x,y)` と読めます。
恒等律は `0≥d(x,x)`、結合律は反転した順序を戻せば三角不等式 `d(x,z)≤d(x,y)+d(y,z)` になります。対称性を
仮定しないため、一般には非対称距離も含みます。これは「射の集合を構造化する」だけでなく、真理値や数値を
hom対象として圏の公理を読む豊穣化の広さを示します。

## 要点

* `V`-豊穣圏のhomは集合ではなくモノイダル圏 `V` の対象である。
* 恒等射は `I→Hom_V(X,X)`、合成は `Hom_V(X,Y)⊗Hom_V(Y,Z)→Hom_V(X,Z)` という `V` の射である。
* 単位律と結合律には、値圏の単位子と結合子が明示的に現れる。
* 豊穣関手はhom対象間の `V`-射を持ち、豊穣恒等射と豊穣合成を保存する。
* 豊穣自然変換の型は一般化要素の族であり、自然変換を集める豊穣hom対象の存在とは区別する。
* `Type`-豊穣圏は通常の圏・関手を回収するが、前順序や距離空間など別の値圏も本質的な例を与える。

## 研究史と文献案内

EilenbergとKelly [EK66] は閉圏を体系的に扱い、内部homを値に取る圏論の基盤を整えました。Kelly [KEL82] は
豊穣圏、豊穣関手、豊穣自然変換、重み付き極限、Kan拡張を統一的に展開した標準研究書です。1966年の
論文と1982年の体系化を同一時点の完成形として扱わず、定義と用語の発展を区別します。現代の通常圏論との
比較は [MAC98] も参照してください。Leanの `EnrichedCategory`, `EnrichedFunctor`, `EnrichedNatTrans` と
`enrichedNatTransYoneda` は [MATHLIB] の現行APIに従います。

## 問題

### `Type`-豊穣圏の三法則を通常の圏法則へ戻す

`V=Type` とし、テンソル積を直積、単位を `PUnit` としてください。`eId` を `PUnit` の唯一の要素で評価して
恒等射を取り出し、`eComp` を対 `(f,g)` で評価して合成を定義します。豊穣化された左右単位律と結合律を関数の
点ごとの等式として評価し、通常の `id_comp`, `comp_id`, `assoc` が得られることを示せば完了です。

### 前順序を真理値豊穣化として構成する

対象の型 `P` と二項関係 `R:P→P→Prop` を取り、hom対象を命題 `R x y` としてください。テンソル単位から
`R x x` への射が反射性に、`R x y∧R y z` から `R x z` への射が推移性に対応することを示します。逆に反射的・
推移的な関係から豊穣構造を構成し、反対称性が豊穣圏の法則には含まれないことを説明できれば完了です。

### Lawvere距離の向きを三角不等式から決定する

非負拡大実数に通常と逆の順序を入れ、射 `a→b` を通常の順序で `a≥b` が成り立つこととします。テンソルを加法、
単位を零として、恒等の一般化要素と合成射の存在条件を書いてください。それぞれが `d(x,x)=0` の弱い形と
三角不等式へ対応することを示し、なぜ順序を反転しないと不等号の向きが合わないか説明します。

### 自然変換型とhom対象の存在を分離する

二つの `V`-豊穣関手 `F,G` について、成分族 `I→Hom(FX,GX)` と自然性条件から豊穣自然変換の型を定義して
ください。次に、その型を `Hom_V(I,N)` として表現する対象 `N` を得るには何が必要かを調べます。hom対象のend
公式を書き、必要な積・等化子・サイズ条件を列挙してください。成分族が型として定義できるだけでは `N` の存在を
証明しないことを、Leanの `EnrichedNatTrans` と `enrichedNatTransYoneda` の型を比較して説明できれば完了です。
-/

end

end FormalLab.CategoryFoundations.EnrichedCategories