refactor(CategoryTheory/Monoidal): typeclasses Functor.LaxMonoidal, Functor.OplaxMonoidal and Functor.Monoidal

Mathlib.lean

@@ -1786,7 +1786,6 @@ import Mathlib.CategoryTheory.Monoidal.Free.Basic
 import Mathlib.CategoryTheory.Monoidal.Free.Coherence
 import Mathlib.CategoryTheory.Monoidal.Functor
 import Mathlib.CategoryTheory.Monoidal.FunctorCategory
-import Mathlib.CategoryTheory.Monoidal.Functorial
 import Mathlib.CategoryTheory.Monoidal.Hopf_
 import Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
 import Mathlib.CategoryTheory.Monoidal.Internal.Limits

Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

@@ -64,14 +64,8 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R
       leftUnitor_eq := fun _ => TensorProduct.ext' (fun _ _ => rfl)
       rightUnitor_eq := fun _ => TensorProduct.ext' (fun _ _ => rfl) }
 
-variable (R) in
 /-- `forget₂ (AlgebraCat R) (ModuleCat R)` as a monoidal functor. -/
-def toModuleCatMonoidalFunctor : MonoidalFunctor (AlgebraCat.{u} R) (ModuleCat.{u} R) := by
-  unfold instMonoidalCategory
-  exact Monoidal.fromInduced (forget₂ (AlgebraCat R) (ModuleCat R)) _
-
-instance : (toModuleCatMonoidalFunctor R).Faithful :=
-  forget₂_faithful _ _
+example : (forget₂ (AlgebraCat R) (ModuleCat R)).Monoidal := inferInstance
 
 end
 

Mathlib/Algebra/Category/AlgebraCat/Symmetric.lean

@@ -25,20 +25,13 @@ variable {R : Type u} [CommRing R]
 namespace AlgebraCat
 
 instance : BraidedCategory (AlgebraCat.{u} R) :=
-  braidedCategoryOfFaithful (toModuleCatMonoidalFunctor R)
+  braidedCategoryOfFaithful (forget₂ (AlgebraCat R) (ModuleCat R))
     (fun X Y => (Algebra.TensorProduct.comm R X Y).toAlgebraIso)
     (by aesop_cat)
 
-variable (R) in
-/-- `forget₂ (AlgebraCat R) (ModuleCat R)` as a braided functor. -/
-@[simps toMonoidalFunctor]
-def toModuleCatBraidedFunctor : BraidedFunctor (AlgebraCat.{u} R) (ModuleCat.{u} R) where
-  toMonoidalFunctor := toModuleCatMonoidalFunctor R
-
-instance : (toModuleCatBraidedFunctor R).Faithful :=
-  forget₂_faithful _ _
+instance : (forget₂ (AlgebraCat R) (ModuleCat R)).Braided where
 
 instance instSymmetricCategory : SymmetricCategory (AlgebraCat.{u} R) :=
-  symmetricCategoryOfFaithful (toModuleCatBraidedFunctor R)
+  symmetricCategoryOfFaithful (forget₂ (AlgebraCat R) (ModuleCat R))
 
 end AlgebraCat

Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean

@@ -118,7 +118,7 @@ theorem tensorObj_comul (K L : CoalgebraCat R) :
   rw [ofComonObjCoalgebraStruct_comul]
   dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj]
   simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X, ModuleCat.of_coe, toComonObj_comul,
-    tensor_μ_eq_tensorTensorTensorComm]
+    tensorμ_eq_tensorTensorTensorComm]
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
@@ -147,7 +147,7 @@ theorem comul_tensorObj :
   dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj,
     instCoalgebraStruct_comul]
   simp only [Comon_.monoidal_tensorObj_comul, toComonObj_X, of_carrier, of_isAddCommGroup,
-    of_isModule, toComonObj_comul, of_instCoalgebra, tensor_μ_eq_tensorTensorTensorComm]
+    of_isModule, toComonObj_comul, of_instCoalgebra, tensorμ_eq_tensorTensorTensorComm]
   rfl
 
 theorem comul_tensorObj_tensorObj_right :
@@ -163,7 +163,7 @@ theorem comul_tensorObj_tensorObj_right :
   dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj]
   simp only [instMonoidalCategoryStruct_tensorObj, ModuleCat.MonoidalCategory.tensorObj,
     ModuleCat.coe_of, Comon_.monoidal_tensorObj_comul, toComonObj_X, of_carrier, of_isAddCommGroup,
-    of_isModule, toComonObj_comul, of_instCoalgebra, tensor_μ_eq_tensorTensorTensorComm]
+    of_isModule, toComonObj_comul, of_instCoalgebra, tensorμ_eq_tensorTensorTensorComm]
   rfl
 
 theorem comul_tensorObj_tensorObj_left :
@@ -179,7 +179,7 @@ theorem comul_tensorObj_tensorObj_left :
   dsimp only [Equivalence.symm_inverse, comonEquivalence_functor, toComon_obj]
   simp only [instMonoidalCategoryStruct_tensorObj, ModuleCat.MonoidalCategory.tensorObj,
     ModuleCat.coe_of, Comon_.monoidal_tensorObj_comul, toComonObj_X, of_carrier, of_isAddCommGroup,
-    of_isModule, toComonObj_comul, of_instCoalgebra, tensor_μ_eq_tensorTensorTensorComm]
+    of_isModule, toComonObj_comul, of_instCoalgebra, tensorμ_eq_tensorTensorTensorComm]
   rfl
 
 theorem counit_tensorObj :

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -146,7 +146,7 @@ instance monoidalPredicate_module_finite :
   prop_id := Module.Finite.self R
   prop_tensor := @fun X Y _ _ => Module.Finite.tensorProduct R X Y
 
-instance : MonoidalCategory (FGModuleCat R) := by
+instance instMonoidalCategory : MonoidalCategory (FGModuleCat R) := by
   dsimp [FGModuleCat]
   infer_instance
 
@@ -167,24 +167,12 @@ instance : MonoidalLinear R (FGModuleCat R) := by
   dsimp [FGModuleCat]
   infer_instance
 
-/-- The forgetful functor `FGModuleCat R ⥤ Module R` as a monoidal functor. -/
-def forget₂Monoidal : MonoidalFunctor (FGModuleCat R) (ModuleCat.{u} R) :=
-  MonoidalCategory.fullMonoidalSubcategoryInclusion _
+/-- The forgetful functor `FGModuleCat R ⥤ Module R` is a monoidal functor. -/
+instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Monoidal :=
+  fullSubcategoryInclusionMonoidal _
 
-instance forget₂Monoidal_faithful : (forget₂Monoidal R).Faithful := by
-  dsimp [forget₂Monoidal]
-  -- Porting note (#11187): was `infer_instance`
-  exact FullSubcategory.faithful _
-
-instance forget₂Monoidal_additive : (forget₂Monoidal R).Additive := by
-  dsimp [forget₂Monoidal]
-  -- Porting note (#11187): was `infer_instance`
-  exact Functor.fullSubcategoryInclusion_additive _
-
-instance forget₂Monoidal_linear : (forget₂Monoidal R).Linear R := by
-  dsimp [forget₂Monoidal]
-  -- Porting note (#11187): was `infer_instance`
-  exact Functor.fullSubcategoryInclusionLinear _ _
+instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Additive where
+instance : (forget₂ (FGModuleCat.{u} R) (ModuleCat.{u} R)).Linear R where
 
 theorem Iso.conj_eq_conj {V W : FGModuleCat R} (i : V ≅ W) (f : End V) :
     Iso.conj i f = LinearEquiv.conj (isoToLinearEquiv i) f :=