import Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
import Mathlib.CategoryTheory.Monoidal.Closed.Braided
import Mathlib.CategoryTheory.Monoidal.Closed.Enrichment
import FormalLab.CategoryTheory.MonoidalCategories
import FormalLab.CategoryTheory.EnrichedCategories
import FormalLab.Bridges.CartesianClosedCategories

/-!
# 第75章：モノイダル閉圏——内部hom・評価・自己豊穣化

第70章のデカルト閉圏では、積 `A×X` と関数型 `A⇒B` の間に

$$
\operatorname{Hom}(A\times X,B)
\cong\operatorname{Hom}(X,A\Rightarrow B).
$$

という対応がありました。この式では、`×` が二つの異なる役割を同時に担っています。一方では二つの対象を
組み合わせるモノイダル積であり、他方では射影・対角射を備えた圏論的積です。関数を適用するために必要なのは
第一の役割とカリー化であって、入力を捨てたり複製したりする第二の役割ではありません。

モノイダル閉圏（monoidal closed category）は、デカルト積を一般のテンソル積 `⊗` に置き換え、各 `A` に対して

$$
A\otimes-\dashv[A,-].
$$

を要求します。右随伴 `[A,-]` が内部homです。本章では、評価・カリー化の計算法則、射をテンソル単位から出る
一般化要素として読む方法、内部hom自身のカリー化、内部恒等射と内部合成を順に構成します。最後に、これらが
圏を自分自身の上で豊穣化する理由と、複製・破棄を持たないことが線形型へどうつながるかを明らかにします。

## 閉対象は一方のテンソル関手に右随伴を持つ

モノイダル圏 `C` の対象 `A` を固定すると、左から `A` をテンソルする関手

$$
A\otimes-:\mathcal C\longrightarrow\mathcal C
$$

が得られます。この関手が右随伴を持つとき、`A` を右閉対象と呼びます。右随伴を `[A,-]` と書けば、全ての
`X,B` について自然な全単射

$$
\operatorname{Hom}_{\mathcal C}(A\otimes X,B)
\cong\operatorname{Hom}_{\mathcal C}(X,[A,B]).
$$

があります。全ての対象が右閉であるモノイダル圏を、ここではモノイダル閉圏と呼びます。
-/

namespace FormalLab.Bridges.MonoidalClosedCategories

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

universe uC vC

variable {C : Type uC} [Category.{vC} C] [MonoidalCategory C] [MonoidalClosed C]
variable {A B X Y Z : C}

def internalHom (A B : C) : C := (ihom A).obj B

example (A : C) : tensorLeft A ⊣ ihom A := ihom.adjunction A

example (A X B : C) : (A ⊗ X ⟶ B) ≃ (X ⟶ internalHom A B) :=
  (ihom.adjunction A).homEquiv X B

/-!
Leanの `Closed A` は、右随伴が存在するという命題だけでなく、右随伴関手と随伴を選択したデータです。
`MonoidalClosed C` は各 `A` にそのデータを与えます。右随伴は自然同型を除いて一意ですが、定義上の等しさまで
一意ではありません。したがって、選択した内部homに依存する式では自然同型と定義的等号を区別します。

「右閉」という語の左右は、右随伴があることではなく、mathlibの規約では `A⊗-` を固定したことに対応します。
文献によって左右の呼称やテンソル因子の順序は異なるため、名称だけで判断せず、hom同値の式を確認してください。

## 評価と余評価は随伴の余単位と単位である

随伴 `A⊗- ⊣ [A,-]` の余単位を対象 `B` で評価すると、評価射

$$
\mathsf{ev}_{A,B}:A\otimes[A,B]\longrightarrow B
$$

を得ます。単位を対象 `X` で評価すると、余評価射

$$
\mathsf{coev}_{A,X}:X\longrightarrow[A,A\otimes X]
$$

を得ます。評価は内部関数へ入力を渡し、余評価は `x:X` に対して `a↦a⊗x` に相当する内部関数を作ります。
-/

def evaluation (A B : C) : A ⊗ internalHom A B ⟶ B :=
  (ihom.ev A).app B

def coevaluation (A X : C) : X ⟶ internalHom A (A ⊗ X) :=
  (ihom.coev A).app X

example (f : B ⟶ Z) :
    A ◁ (ihom A).map f ≫ evaluation A Z = evaluation A B ≫ f :=
  ihom.ev_naturality A f

example (f : X ⟶ Y) :
    f ≫ coevaluation A Y = coevaluation A X ≫ (ihom A).map (A ◁ f) :=
  ihom.coev_naturality A f

/-!
この二式は評価と余評価の自然性です。`B` の射は内部homの値側へ共変に作用し、`X` の射はテンソルしてから
内部homへ送られます。一つの評価射を選ぶだけでは閉性になりません。全対象にわたる自然性と随伴の三角恒等式が、
任意の射を評価経由で一意に表すことを保証します。

## カリー化と逆カリー化は互いに逆である

射 `f:A⊗X→B` の随伴転置を `curry(f):X→[A,B]` と呼びます。逆に `g:X→[A,B]` を評価射へつなぐと
`uncurry(g):A⊗X→B` を得ます。
-/

def closedCurry (f : A ⊗ X ⟶ B) : X ⟶ internalHom A B := curry f

def closedUncurry (g : X ⟶ internalHom A B) : A ⊗ X ⟶ B := uncurry g

theorem closed_uncurry_curry (f : A ⊗ X ⟶ B) :
    closedUncurry (closedCurry f) = f :=
  uncurry_curry f

theorem closed_curry_uncurry (g : X ⟶ internalHom A B) :
    closedCurry (closedUncurry g) = g :=
  curry_uncurry g

theorem closed_beta (f : A ⊗ X ⟶ B) :
    A ◁ closedCurry f ≫ evaluation A B = f :=
  whiskerLeft_curry_ihom_ev_app A B f

/-!
`closed_beta` はカリー化した射を評価すると元の射へ戻るβ則です。`closed_curry_uncurry` は、内部関数を全ての
入力へ適用して再び抽象すれば元へ戻るη則です。β則だけなら転置の単射性は保証されず、η則だけなら全射性は
保証されません。二つの逆法則を合わせてhom集合の全単射になります。

デカルト閉圏のラムダ抽象と同じ形が現れますが、文脈結合は `×` ではなく `⊗` です。したがって変数を二回使う
ための対角射や、使わない変数を捨てる終対象への射は閉性からは得られません。カリー化は関数形成と適用を説明し、
弱化と縮約は別の構造として残します。

## 外部の射は内部homの一般化要素になる

テンソル単位を `I` と書きます。右単位子 `A⊗I≅A` を使って `f:A→B` を `A⊗I→B` とみなし、カリー化すると

$$
\ulcorner f\urcorner:I\longrightarrow[A,B]
$$

を得ます。逆向きには一般化要素 `I→[A,B]` を逆カリー化し、右単位子で `A` へ戻します。この対応は

$$
\operatorname{Hom}_{\mathcal C}(A,B)
\cong\operatorname{Hom}_{\mathcal C}(I,[A,B]).
$$

です。内部homの「点」は集合論的要素ではなく、テンソル単位から出る射として観測されます。
-/

def nameOfMorphism (f : A ⟶ B) : 𝟙_ C ⟶ internalHom A B := curry' f

def morphismOfName (g : 𝟙_ C ⟶ internalHom A B) : A ⟶ B := uncurry' g

theorem name_morphismOfName (g : 𝟙_ C ⟶ internalHom A B) :
    nameOfMorphism (morphismOfName g) = g :=
  curry'_uncurry' g

theorem morphismOfName_name (f : A ⟶ B) :
    morphismOfName (nameOfMorphism f) = f :=
  uncurry'_curry' f

example (A B : C) : (A ⟶ B) ≃ (𝟙_ C ⟶ internalHom A B) := curryHomEquiv'

/-!
この同値は外部hom集合と内部hom対象を同一視しません。左辺はLeanの型として存在する射の集まりであり、右辺は
圏 `C` の中で `I` から内部hom対象へ入る射の集まりです。単位からの一般化要素が対象を十分に識別しない圏もある
ため、内部homの構造をその大域要素だけへ還元することはできません。

## 内部homもカリー化できる

通常のカリー化は外部hom集合の間の全単射でした。閉性を二度用いると、その対応自体を圏内の同型

$$
[A\otimes B,C]\cong[B,[A,C]].
$$

として表せます。これは内部カリー化です。結合子が必要なのは、評価を二回行うときに
`(A⊗B)⊗X` と `A⊗(B⊗X)` の括弧を合わせるためです。
-/

def internalCurryIso (A B C : C) :
    internalHom (A ⊗ B) C ≅ internalHom B (internalHom A C) :=
  ihomCurryIso A B C

example (A B C : C) :
    (internalCurryIso A B C).hom ≫ (internalCurryIso A B C).inv =
      𝟙 (internalHom (A ⊗ B) C) :=
  Iso.hom_inv_id _

example (A B C : C) :
    (internalCurryIso A B C).inv ≫ (internalCurryIso A B C).hom =
      𝟙 (internalHom B (internalHom A C)) :=
  Iso.inv_hom_id _

/-!
対象 `A⊗B` の閉性は、全対象が閉であるという仮定から得ています。一つの対象 `A` だけが閉であっても、上の
同型に必要な `B` と `A⊗B` の閉性は自動的にはそろいません。対象ごとの閉性と圏全体の閉性を区別する理由です。

## 恒等射と合成を内部の射として表す

恒等射 `id_A:A→A` の名はテンソル単位から内部homへ入る射です。また二つの内部homをテンソルし、評価を二回
行ってカリー化すると、内部合成を得ます。

$$
j_A:I\longrightarrow[A,A],
\qquad
c_{A,B,C}:[A,B]\otimes[B,C]\longrightarrow[A,C].
$$

テンソル因子の順は、先に `A→B`、次に `B→C` を置くmathlibの規約です。
-/

def internalIdentity (A : C) : 𝟙_ C ⟶ internalHom A A :=
  MonoidalClosed.id A

def internalComposition (A B C : C) :
    internalHom A B ⊗ internalHom B C ⟶ internalHom A C :=
  MonoidalClosed.comp A B C

example (A : C) : internalIdentity A = nameOfMorphism (𝟙 A) := by
  symm
  exact curry'_id A

example (A B : C) :
    (λ_ (internalHom A B)).inv ≫ internalIdentity A ▷ internalHom A B ≫
      internalComposition A A B = 𝟙 (internalHom A B) :=
  MonoidalClosed.id_comp A B

example (A B X D : C) :
    (α_ (internalHom A B) (internalHom B X) (internalHom X D)).inv ≫
        internalComposition A B X ▷ internalHom X D ≫ internalComposition A X D =
      internalHom A B ◁ internalComposition B X D ≫ internalComposition A B D :=
  MonoidalClosed.assoc A B X D

/-!
左右の単位律と結合律には、モノイダル圏の単位子と結合子が現れます。対象の積が厳密に結合的であると仮定して
式を省略しているのではありません。第64章の整合性が、内部合成の型を正しく接続します。

## モノイダル閉圏は自分自身の上で豊穣化される

第65章で、`V`-豊穣圏は各二対象に `V` のhom対象を割り当て、恒等と合成を `V` の射として持つと定義しました。
ここで `V=C`、hom対象を `[A,B]` とし、直前に構成した `internalIdentity` と `internalComposition` を使えます。
単位律と結合律も既に成立するので、モノイダル閉圏 `C` は標準的に `C` 自身の上で豊穣化されます。
-/

section SelfEnrichment

open scoped MonoidalClosed

example (A B : C) : EnrichedCategory.Hom A B = internalHom A B :=
  MonoidalClosed.enrichedCategorySelf_hom A B

example (A : C) : eId C A = internalIdentity A :=
  MonoidalClosed.enrichedCategorySelf_id A

example (A B D : C) : eComp C A B D = internalComposition A B D :=
  MonoidalClosed.enrichedCategorySelf_comp A B D

end SelfEnrichment

/-!
この自己豊穣化は内部homがあるというだけの比喩ではありません。hom対象、豊穣恒等射、豊穣合成と三法則が
同じデータから構成されます。さらに `Hom_C(A,B)≃Hom_C(I,[A,B])` によって、元の通常圏の射も自己豊穣化の
一般化要素として回収されます。

一方、任意のモノイダル圏が自分自身の上で豊穣化されるわけではありません。内部homがなければ外部homを `C` の
対象として戻せず、この構成は開始できません。閉性はモノイダル構造と豊穣圏論を結ぶ条件です。

## 左閉性と右閉性は一般には別である

ここまで固定したのは `A⊗-` でした。反対側の関手 `-⊗A` に右随伴があるという条件も考えられます。非対称な
モノイダル圏では二条件は別であり、一方から他方を無条件には導けません。

組紐モノイダル圏では、組紐 `X⊗A≅A⊗X` が `-⊗A` と `A⊗-` を自然同型で結びます。従って一方の閉性を
反対側へ運べます。対称モノイダル圏は特に組紐モノイダル圏なので、左右の内部homは標準的な自然同型を通じて
比較できます。ただし、同じ関手であるという定義的等号ではありません。
-/

section Braided

variable [BraidedCategory C]

example (A : C) : (tensorRight A).IsLeftAdjoint := inferInstance

end Braided

/-!
このLean宣言は `tensorRight A` の右随伴を具体的な名前で新たに定義するのではなく、組紐によって左随伴性を
移したことを記録します。左内部homを式で用いるときは、選ばれた右随伴と比較同型を別途追跡します。

## デカルト閉圏は特別なモノイダル閉圏である

`Type` ではテンソル積が直積、内部homが関数型です。従って第70章のカリー化が本章のカリー化の具体例になります。
-/

example (A X B : Type uC) :
    (A ⊗ X ⟶ B) ≃ (X ⟶ (ihom A).obj B) :=
  (ihom.adjunction A).homEquiv X B

example {A X B : Type uC} (f : A × X → B) (x : X) (a : A) :
    FormalLab.Bridges.CartesianClosedCategories.typeCurry f x a = f (a, x) := rfl

/-!
しかし `Type` には内部hom以外の追加構造があります。任意の型 `A` に対して削除 `A→PUnit` と複製
`A→A×A` が自然に定まり、射影もあります。一般のモノイダル閉圏には次の射は含まれません。

$$
\mathsf{discard}_A:A\longrightarrow I,
\qquad
\mathsf{duplicate}_A:A\longrightarrow A\otimes A.
$$

たとえばベクトル空間のテンソル積で `v↦v⊗v` は加法を保たないため、通常は線形写像ではありません。基底を
選んで複製を作っても自然性を失います。従ってテンソル積を単なる記号違いの直積と考えることはできません。

削除は変数を使わない弱化に、複製は変数を二度使う縮約に対応します。これらを無条件に認めないまま評価と
カリー化を残すと、各仮定を資源として一度ずつ扱う線形ラムダ計算の意味論が現れます。次章では、この観察を
線形論理の結合子と型付け規則へ発展させます。

## テンソルは余極限を保つ

各 `A` について `A⊗-` は右随伴 `[A,-]` を持つ左随伴です。従って、存在する余極限を保存します。これは
テンソルが余積や余等化子と両立する多くの例で、個別の計算を随伴の一般定理へ還元します。

ただし右閉性だけから `-⊗A` も余極限を保存するとはいえません。組紐があれば二つのテンソル関手が同型なので
反対側にも移せます。また右随伴 `[A,-]` は、存在する極限を保存します。閉性はカリー化だけでなく、テンソルと
極限・余極限の相互作用も統制します。

## 現行mathlibが形式化する境界

mathlibの `Closed A` は `tensorLeft A` に選ばれた右随伴を持たせ、`MonoidalClosed C` はその構造を全対象へ
与えます。`ihom A`、`ihom.ev A`、`ihom.coev A` は右随伴、余単位、単位です。`curry` と `uncurry` は随伴の
hom同値を使用し、`ihomCurryIso` は内部hom間のカリー化同型を構成します。

自己豊穣化は別ファイルのscoped instanceとして提供されます。同じ圏が別の仕方でも豊穣化され得るため、Leanは
これを大域的に常時有効にはしません。必要な節だけでスコープを開くことは、数学的な一意性の主張ではなく、
インスタンス探索の曖昧さを避ける実装上の選択です。

## 要点

* 対象 `A` が右閉であるとは、`A⊗-` が右随伴 `[A,-]` を持つことである。
* モノイダル閉圏では `Hom(A⊗X,B)≃Hom(X,[A,B])` が自然に成り立つ。
* 評価と余評価は随伴の余単位と単位であり、カリー化のβ・η則は二つの逆法則である。
* 外部の射 `A→B` は内部homの一般化要素 `I→[A,B]` として回収できるが、内部hom対象そのものではない。
* 内部恒等射と内部合成によって、モノイダル閉圏は自分自身の上で豊穣化される。
* 非対称なモノイダル圏では左右の閉性を区別し、組紐がある場合に一方を他方へ移せる。
* 閉性だけでは削除や複製は得られず、弱化と縮約を制限する線形型の意味論へつながる。

## 研究史と文献案内

EilenbergとKelly [EK66] は、内部homと外部homの関係を含む閉圏の体系を構築した一次資料です。同論文の
“closed category” は、後に標準化されたモノイダル閉圏の用語や現行mathlibの型クラスと細部まで同一では
ありません。歴史的定義を現在のAPIへそのまま遡及させず、構造の発展と記法の変化を区別してください。

Mac Lane [MAC63] は自然な結合性と可換性の整合条件を研究した一次資料であり、本章で評価と内部合成の括弧を
制御するモノイダル整合性の歴史的基盤です。豊穣圏、内部hom、自己豊穣化を含む成熟した体系はKelly [KEL82] が
標準的です。Leanの `Closed`, `MonoidalClosed`, `ihomCurryIso` と自己豊穣化の宣言は [MATHLIB] の現行APIに
従います。

## 問題

### 評価射からhom同値の一意性を再構成する

対象 `[A,B]` と射 `ev:A⊗[A,B]→B` が与えられ、全ての `f:A⊗X→B` に対して射
`λf:X→[A,B]` が存在し、`A◁λf≫ev=f` を満たすとします。さらにこの等式を満たす射が一意であることを仮定し、
`curry` と `uncurry` が互いに逆であることを証明してください。逆に二つの逆法則から媒介射の存在一意性を導き、
hom同値の自然性には追加で何を確かめる必要があるかを列挙できれば完了です。

### 内部カリー化同型の二重評価を追跡する

`[A⊗B,C]→[B,[A,C]]` を、評価射、結合子、二回のカリー化だけで構成してください。その射を二回逆カリー化すると
`(A⊗B)⊗[A⊗B,C]→C` が元の評価射と一致することを示します。逆向きも構成し、二つの合成が恒等射になる証明で
β則とη則をそれぞれどこに使うかを明記してください。Leanでは `ihomCurry`, `ihomUncurry` と
`uncurry_uncurry_ihomCurry` の型を比較します。

### 内部合成から通常の射の合成を回収する

`f:A→B`, `g:B→C` をそれぞれ `I→[A,B]`, `I→[B,C]` へ移し、単位対象の逆単位子を介して二つをテンソルし、
`[A,B]⊗[B,C]→[A,C]` へ合成してください。得られた `I→[A,C]` が `f≫g` の名と一致することを示します。
豊穣合成の単位律・結合律が通常の圏の三法則へ移る過程まで図式で説明できれば完了です。

### デカルト構造が弱化と縮約を生むことを示す

デカルトモノイダル圏で、終対象への一意射 `discard_A:A→1` と対角射
`duplicate_A=⟨𝟙_A,𝟙_A⟩:A→A×A` を構成してください。両者が `A` について自然であり、可換コモノイドの法則を
満たすことを示します。次に一般のモノイダル閉圏の公理一覧を調べ、どのデータが不足して同じ構成が止まるかを
特定してください。「射が思いつかない」ではなく、積の普遍性のどの部分を使えないかを述べれば完了です。

### 組紐によって左右の閉性を移す

組紐モノイダル圏で自然同型 `-⊗A≅A⊗-` を書き、`A⊗- ⊣ [A,-]` と合成して `-⊗A` の右随伴を構成して
ください。hom集合の同値を射ごとに書き、組紐の逆射を使う位置を確認します。対称性ではなく組紐だけで十分な理由と、
組紐のない圏では証明できない箇所を区別できれば完了です。さらに、移送して得た右随伴が元の内部hom関手と
同じ定義になるとは限らず、右随伴の一意性が与える自然同型までが標準的な比較であることを説明してください。
Leanでは `BraidedCategory.tensorLeftIsoTensorRight A` の向きと `tensorRight A` の `IsLeftAdjoint` インスタンスを
照合し、数学的な構成とライブラリが自動推論する性質を一対一に対応させます。

### 左随伴としてのテンソルが余極限を保つことを導く

小圏 `J` と図式 `F:J→C` の余極限が存在するとします。`A⊗-` が左随伴であることから、
`A⊗colim F→colim(A⊗F-)` の標準比較射が同型になる一般定理を適用してください。余積と余等化子を特別な場合として
書き下し、右随伴 `[A,-]` が極限を保つ双対的な主張も述べます。存在しない余極限まで作られるとは主張しないことが
重要です。
-/

end FormalLab.Bridges.MonoidalClosedCategories