feat(CategoryTheory): a closed monoidal category is an ordinary enric…

…hed category over itself (#21436)

Let `C` be a closed monoidal category. It was previously shown (#17326) that `C` is enriched over itself. In this PR, we show that the category structure on `C` is determined by this enriched category structure, i.e. `EnrichedOrdinaryCategory C C` holds.

Mathlib/CategoryTheory/Closed/Enrichment.lean

@@ -1,9 +1,9 @@
 /-
 Copyright (c) 2024 Daniel Carranza. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Daniel Carranza
+Authors: Daniel Carranza, Joël Riou
 -/
-import Mathlib.CategoryTheory.Enriched.Basic
+import Mathlib.CategoryTheory.Enriched.Ordinary.Basic
 import Mathlib.CategoryTheory.Closed.Monoidal
 
 /-!
@@ -25,17 +25,56 @@ universe u v
 
 namespace CategoryTheory
 
+open Category MonoidalCategory
+
 namespace MonoidalClosed
 
-variable {C : Type u} [Category.{v} C] [MonoidalCategory C] [MonoidalClosed C]
+variable (C : Type u) [Category.{v} C] [MonoidalCategory C] [MonoidalClosed C]
 
 /-- For `C` closed monoidal, build an instance of `C` as a `C`-category -/
-scoped instance : EnrichedCategory C C where
+scoped instance enrichedCategorySelf : EnrichedCategory C C where
   Hom x := (ihom x).obj
   id _ := id _
   comp _ _ _ := comp _ _ _
   assoc _ _ _ _ := assoc _ _ _ _
 
+section
+
+variable {C}
+
+lemma enrichedCategorySelf_hom (X Y : C) :
+    EnrichedCategory.Hom X Y = (ihom X).obj Y := rfl
+
+lemma enrichedCategorySelf_id (X : C) :
+    eId C X = id X := rfl
+
+lemma enrichedCategorySelf_comp (X Y Z : C) :
+    eComp C X Y Z = comp X Y Z := rfl
+
+end
+
+/-- A monoidal closed category is an enriched ordinary category over itself.  -/
+scoped instance enrichedOrdinaryCategorySelf : EnrichedOrdinaryCategory C C where
+  homEquiv := curryHomEquiv'
+  homEquiv_id X := curry'_id X
+  homEquiv_comp := curry'_comp
+
+lemma enrichedOrdinaryCategorySelf_eHomWhiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
+    eHomWhiskerLeft C X g = (ihom X).map g := by
+  change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _
+  rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]
+
+lemma enrichedOrdinaryCategorySelf_eHomWhiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
+    eHomWhiskerRight C f Y = (pre f).app Y := by
+  change (λ_ _).inv ≫ curry' f ▷ _ ≫ comp X₁ X₂ Y = _
+  rw [curry'_whiskerRight_comp, Iso.inv_hom_id_assoc]
+
+lemma enrichedOrdinaryCategorySelf_homEquiv {X Y : C} (f : X ⟶ Y) :
+    eHomEquiv C f = curry' f := rfl
+
+lemma enrichedOrdinaryCategorySelf_homEquiv_symm {X Y : C} (g : 𝟙_ C ⟶ (ihom X).obj Y):
+    (eHomEquiv C).symm g = uncurry' g := rfl
+
 end MonoidalClosed
 
 end CategoryTheory

Mathlib/CategoryTheory/Closed/Monoidal.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kim Morrison, Bhavik Mehta
+Authors: Kim Morrison, Bhavik Mehta, Daniel Carranza, Joël Riou
 -/
 import Mathlib.CategoryTheory.Monoidal.Functor
+import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
 import Mathlib.CategoryTheory.Adjunction.Limits
 import Mathlib.CategoryTheory.Adjunction.Mates
 
@@ -196,6 +197,16 @@ theorem curry_id_eq_coev : curry (𝟙 _) = (ihom.coev A).app X := by
   rw [curry_eq, (ihom A).map_id (A ⊗ _)]
   apply comp_id
 
+@[reassoc (attr := simp)]
+lemma whiskerLeft_curry_ihom_ev_app (g : A ⊗ Y ⟶ X) :
+    A ◁ curry g ≫ (ihom.ev A).app X = g := by
+  simp [curry_eq]
+
+theorem uncurry_ihom_map (g : Y ⟶ Y') :
+    uncurry ((ihom A).map g) = (ihom.ev A).app Y ≫ g := by
+  apply curry_injective
+  rw [curry_uncurry, curry_natural_right, ← uncurry_id_eq_ev, curry_uncurry, id_comp]
+
 /-- The internal hom out of the unit is naturally isomorphic to the identity functor.-/
 def unitNatIso [Closed (𝟙_ C)] : 𝟭 C ≅ ihom (𝟙_ C) :=
   conjugateIsoEquiv (Adjunction.id (C := C)) (ihom.adjunction (𝟙_ C))
@@ -219,11 +230,23 @@ theorem uncurry_pre (f : B ⟶ A) (X : C) :
     MonoidalClosed.uncurry ((pre f).app X) = f ▷ _ ≫ (ihom.ev A).app X := by
   simp [uncurry_eq]
 
+@[reassoc]
+lemma curry_pre_app (f : B ⟶ A) {X Y : C} (g : A ⊗ Y ⟶ X) :
+    curry g ≫ (pre f).app X = curry (f ▷ _ ≫ g) := uncurry_injective (by
+  rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
+    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app])
+
 @[reassoc (attr := simp)]
 theorem coev_app_comp_pre_app (f : B ⟶ A) :
     (ihom.coev A).app X ≫ (pre f).app (A ⊗ X) = (ihom.coev B).app X ≫ (ihom B).map (f ▷ _) :=
   unit_conjugateEquiv _ _ ((tensoringLeft C).map f) X
 
+@[reassoc]
+lemma uncurry_pre_app (f : Y ⟶ A ⟶[C] X) (g : B ⟶ A) :
+    uncurry (f ≫ (pre g).app X) = g ▷ _ ≫ uncurry f :=
+  curry_injective (by
+    rw [curry_uncurry, ← curry_pre_app, curry_uncurry])
+
 @[simp]
 theorem pre_id (A : C) [Closed A] : pre (𝟙 A) = 𝟙 _ := by
   rw [pre, Functor.map_id]
@@ -388,6 +411,91 @@ lemma assoc (w x y z : C) [Closed w] [Closed x] [Closed y] :
 
 end Enriched
 
+section OrdinaryEnriched
+
+/-- The morphism `𝟙_ C ⟶ (ihom X).obj Y` corresponding to a morphism `X ⟶ Y`. -/
+def curry' {X Y : C} [Closed X] (f : X ⟶ Y) : 𝟙_ C ⟶ (ihom X).obj Y :=
+  curry ((ρ_ _).hom ≫ f)
+
+/-- The morphism `X ⟶ Y` corresponding to a morphism `𝟙_ C ⟶ (ihom X).obj Y`. -/
+def uncurry' {X Y : C} [Closed X] (g : 𝟙_ C ⟶ (ihom X).obj Y) : X ⟶ Y :=
+  (ρ_ _).inv ≫ uncurry g
+
+/-- `curry'` and `uncurry`' are inverse bijections. -/
+@[simp]
+lemma curry'_uncurry' {X Y : C} [Closed X] (g : 𝟙_ C ⟶ (ihom X).obj Y) :
+    curry' (uncurry' g) = g := by
+  simp [curry', uncurry']
+
+/-- `curry'` and `uncurry`' are inverse bijections. -/
+@[simp]
+lemma uncurry'_curry' {X Y : C} [Closed X] (f : X ⟶ Y) :
+    uncurry' (curry' f) = f := by
+  simp [curry', uncurry']
+
+/-- The bijection `(X ⟶ Y) ≃ (𝟙_ C ⟶ (ihom X).obj Y)` in a monoidal closed category. -/
+@[simps]
+def curryHomEquiv' {X Y : C} [Closed X] :
+    (X ⟶ Y) ≃ (𝟙_ C ⟶ (ihom X).obj Y) where
+  toFun := curry'
+  invFun := uncurry'
+  left_inv _ := by simp
+  right_inv _ := by simp
+
+lemma curry'_injective {X Y : C} [Closed X] {f f' : X ⟶ Y} (h : curry' f = curry' f') :
+    f = f' :=
+  curryHomEquiv'.injective h
+
+lemma uncurry'_injective {X Y : C} [Closed X] {f f' : 𝟙_ C ⟶ (ihom X).obj Y}
+    (h : uncurry' f = uncurry' f') : f = f' :=
+  curryHomEquiv'.symm.injective h
+
+@[simp]
+lemma curry'_id (X : C) [Closed X] : curry' (𝟙 X) = id X := by
+  dsimp [curry']
+  rw [Category.comp_id]
+  rfl
+
+@[reassoc]
+lemma whiskerLeft_curry'_ihom_ev_app {X Y : C} [Closed X] (f : X ⟶ Y) :
+    X ◁ curry' f ≫ (ihom.ev X).app Y = (ρ_ _).hom ≫ f := by
+  dsimp [curry']
+  simp only [whiskerLeft_curry_ihom_ev_app]
+
+@[reassoc]
+lemma curry'_whiskerRight_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) :
+    curry' f ▷ _ ≫ comp X Y Z = (λ_ _).hom ≫ (pre f).app Z := by
+  rw [← cancel_epi (λ_ _).inv, Iso.inv_hom_id_assoc]
+  apply uncurry_injective
+  rw [uncurry_pre, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
+    compTranspose_eq, associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc,
+    whiskerLeft_curry'_ihom_ev_app, comp_whiskerRight_assoc, triangle_assoc_comp_right_assoc,
+    whiskerLeft_inv_hom_assoc]
+
+@[reassoc]
+lemma whiskerLeft_curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : Y ⟶ Z) :
+    _ ◁ curry' f ≫ comp X Y Z = (ρ_ _).hom ≫ (ihom X).map f := by
+  rw [← cancel_epi (ρ_ _).inv, Iso.inv_hom_id_assoc]
+  apply uncurry_injective
+  rw [uncurry_ihom_map, comp_eq, ← curry_natural_left, ← curry_natural_left, uncurry_curry,
+    compTranspose_eq, associator_inv_naturality_right_assoc, whisker_exchange_assoc]
+  dsimp
+  rw [whiskerLeft_curry'_ihom_ev_app, whiskerLeft_rightUnitor_inv,
+    MonoidalCategory.whiskerRight_id_assoc, Category.assoc,
+    Iso.inv_hom_id_assoc, Iso.hom_inv_id_assoc, Iso.inv_hom_id_assoc,]
+
+lemma curry'_ihom_map {X Y Z : C} [Closed X] (f : X ⟶ Y) (g : Y ⟶ Z) :
+    curry' f ≫ (ihom X).map g = curry' (f ≫ g) := by
+  simp only [curry', ← curry_natural_right, Category.assoc]
+
+lemma curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) (g : Y ⟶ Z) :
+    curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ curry' g) ≫ comp X Y Z := by
+  rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
+    Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
+    Iso.inv_hom_id_assoc, curry'_ihom_map]
+
+end OrdinaryEnriched
+
 end MonoidalClosed
 attribute [nolint simpNF] CategoryTheory.MonoidalClosed.homEquiv_apply_eq
   CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq