feat(category_theory/closed/functor_category): the functor category f…

…rom a groupoid to a monoidal closed category is monoidal closed (#15643)




Co-authored-by: antoinelab01 <66086247+antoinelab01@users.noreply.github.com>

src/category_theory/closed/functor_category.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2022 Antoine Labelle. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Antoine Labelle
+-/
+import category_theory.closed.monoidal
+import category_theory.monoidal.functor_category
+
+/-!
+# Functors from a groupoid into a monoidal closed category form a monoidal closed category.
+
+(Using the pointwise monoidal structure on the functor category.)
+-/
+
+noncomputable theory
+
+open category_theory
+open category_theory.monoidal_category
+open category_theory.monoidal_closed
+
+namespace category_theory.functor
+
+variables {C D : Type*} [groupoid D] [category C] [monoidal_category C] [monoidal_closed C]
+
+/-- Auxiliary definition for `category_theory.monoidal_closed.functor_closed`.
+The internal hom functor `F ⟶[C] -` -/
+@[simps] def closed_ihom (F : D ⥤ C) : (D ⥤ C) ⥤ (D ⥤ C) :=
+((whiskering_right₂ D Cᵒᵖ C C).obj internal_hom).obj (groupoid.inv_functor D ⋙ F.op)
+
+/-- Auxiliary definition for `category_theory.monoidal_closed.functor_closed`.
+The unit for the adjunction `(tensor_left F) ⊣ (ihom F)`. -/
+@[simps]
+def closed_unit (F : D ⥤ C) : 𝟭 (D ⥤ C) ⟶ (tensor_left F) ⋙ (closed_ihom F) :=
+{ app := λ G,
+  { app := λ X, (ihom.coev (F.obj X)).app (G.obj X),
+    naturality' := begin
+      intros X Y f,
+      dsimp,
+      simp only [ihom.coev_naturality, closed_ihom_obj_map, monoidal.tensor_obj_map],
+      dsimp,
+      rw [coev_app_comp_pre_app_assoc, ←functor.map_comp],
+      simp,
+    end } }
+
+/-- Auxiliary definition for `category_theory.monoidal_closed.functor_closed`.
+The counit for the adjunction `(tensor_left F) ⊣ (ihom F)`. -/
+@[simps]
+def closed_counit (F : D ⥤ C) : (closed_ihom F) ⋙ (tensor_left F) ⟶ 𝟭 (D ⥤ C) :=
+{ app := λ G,
+  { app := λ X, (ihom.ev (F.obj X)).app (G.obj X),
+    naturality' := begin
+      intros X Y f,
+      dsimp,
+      simp only [closed_ihom_obj_map, pre_comm_ihom_map],
+      rw [←tensor_id_comp_id_tensor, id_tensor_comp],
+      simp,
+    end } }
+
+/-- If `C` is a monoidal closed category and `D` is groupoid, then every functor `F : D ⥤ C` is
+closed in the functor category `F : D ⥤ C` with the pointwise monoidal structure. -/
+@[simps] instance closed (F : D ⥤ C) : closed F :=
+{ is_adj :=
+  { right := closed_ihom F,
+    adj := adjunction.mk_of_unit_counit
+    { unit := closed_unit F,
+      counit := closed_counit F } } }
+
+/-- If `C` is a monoidal closed category and `D` is groupoid, then the functor category `D ⥤ C`,
+with the pointwise monoidal structure, is monoidal closed. -/
+@[simps] instance monoidal_closed : monoidal_closed (D ⥤ C) :=
+{ closed' := by apply_instance }
+
+end category_theory.functor

src/category_theory/closed/monoidal.lean

@@ -206,15 +206,18 @@ variables {A B} [closed B]
 def pre (f : B ⟶ A) : ihom A ⟶ ihom B :=
 transfer_nat_trans_self (ihom.adjunction _) (ihom.adjunction _) ((tensoring_left C).map f)
 
+@[simp, reassoc]
 lemma id_tensor_pre_app_comp_ev (f : B ⟶ A) (X : C) :
   (𝟙 B ⊗ ((pre f).app X)) ≫ (ihom.ev B).app X =
     (f ⊗ (𝟙 (A ⟶[C] X))) ≫ (ihom.ev A).app X :=
 transfer_nat_trans_self_counit _ _ ((tensoring_left C).map f) X
 
+@[simp]
 lemma uncurry_pre (f : B ⟶ A) (X : C) :
   monoidal_closed.uncurry ((pre f).app X) = (f ⊗ 𝟙 _) ≫ (ihom.ev A).app X :=
 by rw [uncurry_eq, id_tensor_pre_app_comp_ev]
 
+@[simp, reassoc]
 lemma 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 ⊗ (𝟙 _)) :=
@@ -230,9 +233,14 @@ lemma pre_map {A₁ A₂ A₃ : C} [closed A₁] [closed A₂] [closed A₃]
   pre (f ≫ g) = pre g ≫ pre f :=
 by rw [pre, pre, pre, transfer_nat_trans_self_comp, (tensoring_left C).map_comp]
 
+lemma pre_comm_ihom_map {W X Y Z : C} [closed W] [closed X]
+  (f : W ⟶ X) (g : Y ⟶ Z) :
+  (pre f).app Y ≫ (ihom W).map g = (ihom X).map g ≫ (pre f).app Z := by simp
+
 end pre
 
 /-- The internal hom functor given by the monoidal closed structure. -/
+@[simps]
 def internal_hom [monoidal_closed C] : Cᵒᵖ ⥤ C ⥤ C :=
 { obj := λ X, ihom X.unop,
   map := λ X Y f, pre f.unop }

src/category_theory/groupoid.lean

@@ -83,6 +83,13 @@ def groupoid.iso_equiv_hom : (X ≅ Y) ≃ (X ⟶ Y) :=
   left_inv := λ i, iso.ext rfl,
   right_inv := λ f, rfl }
 
+variables (C)
+
+/-- The functor from a groupoid `C` to its opposite sending every morphism to its inverse. -/
+@[simps] noncomputable def groupoid.inv_functor : C ⥤ Cᵒᵖ :=
+{ obj := opposite.op,
+  map := λ {X Y} f, (inv f).op }
+
 end
 
 section