feat(CategoryTheory/Monoidal): define Mon_ by using Mon_Class (#24646)

The main change is from
```lean
structure Mon_ where
  X : C
  one : 𝟙_ C ⟶ X
  mul : X ⊗ X ⟶ X
  one_mul : (one ▷ X) ≫ mul = (λ_ X).hom := by aesop_cat
  mul_one : (X ◁ one) ≫ mul = (ρ_ X).hom := by aesop_cat
  mul_assoc : (mul ▷ X) ≫ mul = (α_ X X X).hom ≫ (X ◁ mul) ≫ mul := by aesop_cat
```
to
```lean
structure Mon_ where
  X : C
  [mon : Mon_Class X]
```

- [ ] depends on: #24597

Author: yuma-mizuno

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -36,18 +36,21 @@ universe v u
 
 namespace CoalgCat
 
-open CategoryTheory MonoidalCategory
+open CategoryTheory MonoidalCategory Comon_Class
 
 variable {R : Type u} [CommRing R]
 
-/-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
-@[simps X counit comul] def toComonObj (X : CoalgCat R) : Comon_ (ModuleCat R) where
-  X := ModuleCat.of R X
+@[simps counit comul]
+noncomputable instance (X : CoalgCat R) : Comon_Class (ModuleCat.of R X) where
   counit := ModuleCat.ofHom Coalgebra.counit
   comul := ModuleCat.ofHom Coalgebra.comul
-  counit_comul := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
-  comul_counit := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
-  comul_assoc := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
+  counit_comul' := ModuleCat.hom_ext <| by simpa using Coalgebra.rTensor_counit_comp_comul
+  comul_counit' := ModuleCat.hom_ext <| by simpa using Coalgebra.lTensor_counit_comp_comul
+  comul_assoc' := ModuleCat.hom_ext <| by simp_rw [ModuleCat.of_coe]; exact Coalgebra.coassoc.symm
+
+/-- An `R`-coalgebra is a comonoid object in the category of `R`-modules. -/
+@[simps X]
+noncomputable def toComonObj (X : CoalgCat R) : Comon_ (ModuleCat R) := ⟨ModuleCat.of R X⟩
 
 variable (R) in
 /-- The natural functor from `R`-coalgebras to comonoid objects in the category of `R`-modules. -/
@@ -62,26 +65,26 @@ def toComon : CoalgCat R ⥤ Comon_ (ModuleCat R) where
 /-- A comonoid object in the category of `R`-modules has a natural comultiplication
 and counit. -/
 @[simps]
-noncomputable instance ofComonObjCoalgebraStruct (X : Comon_ (ModuleCat R)) :
-    CoalgebraStruct R X.X where
-  comul := X.comul.hom
-  counit := X.counit.hom
+noncomputable instance ofComonObjCoalgebraStruct (X : ModuleCat R) [Comon_Class X] :
+    CoalgebraStruct R X where
+  comul := Δ[X].hom
+  counit := ε[X].hom
 
 /-- A comonoid object in the category of `R`-modules has a natural `R`-coalgebra
 structure. -/
-def ofComonObj (X : Comon_ (ModuleCat R)) : CoalgCat R :=
-  { ModuleCat.of R X.X with
+noncomputable def ofComonObj (X : ModuleCat R) [Comon_Class X] : CoalgCat R :=
+  { ModuleCat.of R X with
     instCoalgebra :=
       { ofComonObjCoalgebraStruct X with
-        coassoc := ModuleCat.hom_ext_iff.mp X.comul_assoc.symm
-        rTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp X.counit_comul
-        lTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp X.comul_counit } }
+        coassoc := ModuleCat.hom_ext_iff.mp (comul_assoc X).symm
+        rTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp (counit_comul X)
+        lTensor_counit_comp_comul := ModuleCat.hom_ext_iff.mp (comul_counit X) } }
 
 variable (R)
 
 /-- The natural functor from comonoid objects in the category of `R`-modules to `R`-coalgebras. -/
-def ofComon : Comon_ (ModuleCat R) ⥤ CoalgCat R where
-  obj X := ofComonObj X
+noncomputable def ofComon : Comon_ (ModuleCat R) ⥤ CoalgCat R where
+  obj X := ofComonObj X.X
   map f :=
     { toCoalgHom' :=
       { f.hom.hom with
@@ -122,8 +125,10 @@ theorem tensorObj_comul (K L : CoalgCat R) :
       ∘ₗ TensorProduct.map Coalgebra.comul Coalgebra.comul := by
   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]
+  simp only [Comon_.monoidal_tensorObj_comon_comul, Equivalence.symm_inverse,
+    comonEquivalence_functor, toComon_obj, toComonObj_X, ModuleCat.of_coe, comul_def,
+    tensorμ_eq_tensorTensorTensorComm, ModuleCat.hom_comp, ModuleCat.hom_ofHom,
+    LinearEquiv.comp_toLinearMap_eq_iff]
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
@@ -158,9 +163,7 @@ theorem comul_tensorObj_tensorObj_right :
       (CoalgCat.of R N ⊗ CoalgCat.of R P) : CoalgCat R))
       = Coalgebra.comul (A := M ⊗[R] N ⊗[R] P) := by
   rw [ofComonObjCoalgebraStruct_comul]
-  dsimp
-  simp only [Comon_.monoidal_tensorObj_comul, toComonObj_comul]
-  rw [ofComonObjCoalgebraStruct_comul]
+  simp only [Comon_.monoidal_tensorObj_comon_comul, toComonObj]
   simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
     AlgebraTensorModule.tensorTensorTensorComm_eq]
   rfl
@@ -171,8 +174,7 @@ theorem comul_tensorObj_tensorObj_left :
       = Coalgebra.comul (A := (M ⊗[R] N) ⊗[R] P) := by
   rw [ofComonObjCoalgebraStruct_comul]
   dsimp
-  simp only [Comon_.monoidal_tensorObj_comul, toComonObj_comul]
-  rw [ofComonObjCoalgebraStruct_comul]
+  simp only [Comon_.monoidal_tensorObj_comon_comul, toComonObj]
   simp [tensorμ_eq_tensorTensorTensorComm, TensorProduct.comul_def,
     AlgebraTensorModule.tensorTensorTensorComm_eq]
   rfl

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -62,6 +62,8 @@ instance (F : C ⥤ₗ Type v) : PreservesFiniteLimits (inverseAux.obj F) where
 noncomputable def inverse : (C ⥤ₗ Type v) ⥤ (C ⥤ₗ AddCommGrp.{v}) :=
   ObjectProperty.lift _ inverseAux inferInstance
 
+open scoped Mon_Class
+
 attribute [-instance] Functor.LaxMonoidal.comp Functor.Monoidal.instComp in
 /-- Implementation, see `leftExactFunctorForgetEquivalence`.
 This is the complicated bit, where we show that forgetting the group structure in the image of
@@ -72,10 +74,14 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F
       (F ⋙ forget AddCommGrp).mapCommGrp.obj (Preadditive.commGrpEquivalence.functor.obj X) := by
   letI : (F ⋙ forget AddCommGrp).Braided := .ofChosenFiniteProducts _
   letI : F.Monoidal := .ofChosenFiniteProducts _
-  refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by aesop_cat) ?_
+  refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by
+    erw [Functor.mapCommGrp_obj_grp_one]
+    aesop_cat) ?_
   dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_coe, -forget_map]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
-  rw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrp) X X,
+  simp only [Category.id_comp]
+  erw [Functor.mapCommGrp_obj_grp_mul]
+  erw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrp) X X,
     Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
     Functor.Monoidal.μ_snd]
   aesop_cat

Mathlib/CategoryTheory/Monad/EquivMon.lean

@@ -25,7 +25,7 @@ A monad "is just" a monoid in the category of endofunctors.
 
 namespace CategoryTheory
 
-open Category
+open Category Mon_Class
 
 universe v u -- morphism levels before object levels. See note [category_theory universes].
 
@@ -35,13 +35,16 @@ namespace Monad
 
 attribute [local instance] endofunctorMonoidalCategory
 
+@[simps]
+instance (M : Monad C) : Mon_Class (M : C ⥤ C) where
+  one := M.η
+  mul := M.μ
+  mul_assoc' := by ext; simp [M.assoc]
+
 /-- To every `Monad C` we associated a monoid object in `C ⥤ C`. -/
 @[simps]
 def toMon (M : Monad C) : Mon_ (C ⥤ C) where
   X := (M : C ⥤ C)
-  one := M.η
-  mul := M.μ
-  mul_assoc := by ext; simp [M.assoc]
 
 variable (C) in
 /-- Passing from `Monad C` to `Mon_ (C ⥤ C)` is functorial. -/
@@ -51,17 +54,17 @@ def monadToMon : Monad C ⥤ Mon_ (C ⥤ C) where
   map f := { hom := f.toNatTrans }
 
 /-- To every monoid object in `C ⥤ C` we associate a `Monad C`. -/
-@[simps η μ]
+@[simps «η» «μ»]
 def ofMon (M : Mon_ (C ⥤ C)) : Monad C where
   toFunctor := M.X
-  η := M.one
-  μ := M.mul
+  «η» := η[M.X]
+  «μ» := μ[M.X]
   left_unit := fun X => by
-    simpa [-Mon_.mul_one] using congrArg (fun t ↦ t.app X) M.mul_one
+    simpa [-Mon_Class.mul_one] using congrArg (fun t ↦ t.app X) (mul_one M.X)
   right_unit := fun X => by
-    simpa [-Mon_.one_mul] using congrArg (fun t ↦ t.app X) M.one_mul
+    simpa [-Mon_Class.one_mul] using congrArg (fun t ↦ t.app X) (one_mul M.X)
   assoc := fun X => by
-    simpa [-Mon_.mul_assoc] using congrArg (fun t ↦ t.app X) M.mul_assoc
+    simpa [-Mon_Class.mul_assoc] using congrArg (fun t ↦ t.app X) (mul_assoc M.X)
 
 -- Porting note: `@[simps]` fails to generate `ofMon_obj`:
 @[simp] lemma ofMon_obj (M : Mon_ (C ⥤ C)) (X : C) : (ofMon M).obj X = M.X.obj X := rfl
@@ -75,9 +78,9 @@ def monToMonad : Mon_ (C ⥤ C) ⥤ Monad C where
   map {X Y} f :=
     { f.hom with
       app_η X := by
-        simpa [-Mon_.Hom.one_hom] using congrArg (fun t ↦ t.app X) f.one_hom
+        simpa [-IsMon_Hom.one_hom] using congrArg (fun t ↦ t.app X) f.one_hom
       app_μ Z := by
-        simpa [-Mon_.Hom.mul_hom] using congrArg (fun t ↦ t.app Z) f.mul_hom }
+        simpa [-IsMon_Hom.mul_hom] using congrArg (fun t ↦ t.app Z) f.mul_hom }
 
 /-- Oh, monads are just monoids in the category of endofunctors (equivalence of categories). -/
 @[simps]

Mathlib/CategoryTheory/Monoidal/Bimod.lean

@@ -16,7 +16,7 @@ universe v₁ v₂ u₁ u₂
 
 open CategoryTheory
 
-open CategoryTheory.MonoidalCategory
+open CategoryTheory.MonoidalCategory Mon_Class
 
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
 
@@ -78,17 +78,17 @@ structure Bimod (A B : Mon_ C) where
   X : C
   /-- The left action of this bimodule object -/
   actLeft : A.X ⊗ X ⟶ X
-  one_actLeft : (A.one ▷ X) ≫ actLeft = (λ_ X).hom := by aesop_cat
+  one_actLeft : η ▷ X ≫ actLeft = (λ_ X).hom := by aesop_cat
   left_assoc :
-    (A.mul ▷ X) ≫ actLeft = (α_ A.X A.X X).hom ≫ (A.X ◁ actLeft) ≫ actLeft := by aesop_cat
+    μ ▷ X ≫ actLeft = (α_ A.X A.X X).hom ≫ A.X ◁ actLeft ≫ actLeft := by aesop_cat
   /-- The right action of this bimodule object -/
   actRight : X ⊗ B.X ⟶ X
-  actRight_one : (X ◁ B.one) ≫ actRight = (ρ_ X).hom := by aesop_cat
+  actRight_one : X ◁ η ≫ actRight = (ρ_ X).hom := by aesop_cat
   right_assoc :
-    (X ◁ B.mul) ≫ actRight = (α_ X B.X B.X).inv ≫ (actRight ▷ B.X) ≫ actRight := by
+    X ◁ μ ≫ actRight = (α_ X B.X B.X).inv ≫ actRight ▷ B.X ≫ actRight := by
     aesop_cat
   middle_assoc :
-    (actLeft ▷ B.X) ≫ actRight = (α_ A.X X B.X).hom ≫ (A.X ◁ actRight) ≫ actLeft := by
+    actLeft ▷ B.X ≫ actRight = (α_ A.X X B.X).hom ≫ A.X ◁ actRight ≫ actLeft := by
     aesop_cat
 
 attribute [reassoc (attr := simp)] Bimod.one_actLeft Bimod.actRight_one Bimod.left_assoc
@@ -165,8 +165,8 @@ variable (A)
 @[simps]
 def regular : Bimod A A where
   X := A.X
-  actLeft := A.mul
-  actRight := A.mul
+  actLeft := μ
+  actRight := μ
 
 instance : Inhabited (Bimod A A) :=
   ⟨regular A⟩
@@ -218,7 +218,7 @@ theorem whiskerLeft_π_actLeft :
   erw [map_π_preserves_coequalizer_inv_colimMap (tensorLeft _)]
   simp only [Category.assoc]
 
-theorem one_act_left' : (R.one ▷ _) ≫ actLeft P Q = (λ_ _).hom := by
+theorem one_act_left' : (η ▷ _) ≫ actLeft P Q = (λ_ _).hom := by
   refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
   dsimp [X]
   -- Porting note: had to replace `rw` by `erw`
@@ -230,7 +230,7 @@ theorem one_act_left' : (R.one ▷ _) ≫ actLeft P Q = (λ_ _).hom := by
   monoidal
 
 theorem left_assoc' :
-    (R.mul ▷ _) ≫ actLeft P Q = (α_ R.X R.X _).hom ≫ (R.X ◁ actLeft P Q) ≫ actLeft P Q := by
+    (μ ▷ _) ≫ actLeft P Q = (α_ R.X R.X _).hom ≫ (R.X ◁ actLeft P Q) ≫ actLeft P Q := by
   refine (cancel_epi ((tensorLeft _).map (coequalizer.π _ _))).1 ?_
   dsimp [X]
   slice_lhs 1 2 => rw [whisker_exchange]
@@ -277,7 +277,7 @@ theorem π_tensor_id_actRight :
   erw [map_π_preserves_coequalizer_inv_colimMap (tensorRight _)]
   simp only [Category.assoc]
 
-theorem actRight_one' : (_ ◁ T.one) ≫ actRight P Q = (ρ_ _).hom := by
+theorem actRight_one' : (_ ◁ η) ≫ actRight P Q = (ρ_ _).hom := by
   refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
   dsimp [X]
   -- Porting note: had to replace `rw` by `erw`
@@ -288,7 +288,7 @@ theorem actRight_one' : (_ ◁ T.one) ≫ actRight P Q = (ρ_ _).hom := by
   simp
 
 theorem right_assoc' :
-    (_ ◁ T.mul) ≫ actRight P Q =
+    (_ ◁ μ) ≫ actRight P Q =
       (α_ _ T.X T.X).inv ≫ (actRight P Q ▷ T.X) ≫ actRight P Q := by
   refine (cancel_epi ((tensorRight _).map (coequalizer.π _ _))).1 ?_
   dsimp [X]
@@ -595,7 +595,7 @@ noncomputable def hom : TensorBimod.X (regular R) P ⟶ P.X :=
 
 /-- The underlying morphism of the inverse component of the left unitor isomorphism. -/
 noncomputable def inv : P.X ⟶ TensorBimod.X (regular R) P :=
-  (λ_ P.X).inv ≫ (R.one ▷ _) ≫ coequalizer.π _ _
+  (λ_ P.X).inv ≫ (η[R.X] ▷ _) ≫ coequalizer.π _ _
 
 theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   dsimp only [hom, inv, TensorBimod.X]
@@ -606,7 +606,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   slice_lhs 3 3 => rw [← Iso.inv_hom_id_assoc (α_ R.X R.X P.X) (R.X ◁ P.actLeft)]
   slice_lhs 4 6 => rw [← Category.assoc, ← coequalizer.condition]
   slice_lhs 2 3 => rw [associator_inv_naturality_left]
-  slice_lhs 3 4 => rw [← comp_whiskerRight, Mon_.one_mul]
+  slice_lhs 3 4 => rw [← comp_whiskerRight, Mon_Class.one_mul]
   slice_rhs 1 2 => rw [Category.comp_id]
   monoidal
 
@@ -650,7 +650,7 @@ noncomputable def hom : TensorBimod.X P (regular S) ⟶ P.X :=
 
 /-- The underlying morphism of the inverse component of the right unitor isomorphism. -/
 noncomputable def inv : P.X ⟶ TensorBimod.X P (regular S) :=
-  (ρ_ P.X).inv ≫ (_ ◁ S.one) ≫ coequalizer.π _ _
+  (ρ_ P.X).inv ≫ (_ ◁ η[S.X]) ≫ coequalizer.π _ _
 
 theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   dsimp only [hom, inv, TensorBimod.X]
@@ -660,7 +660,7 @@ theorem hom_inv_id : hom P ≫ inv P = 𝟙 _ := by
   slice_lhs 2 3 => rw [← whisker_exchange]
   slice_lhs 3 4 => rw [coequalizer.condition]
   slice_lhs 2 3 => rw [associator_naturality_right]
-  slice_lhs 3 4 => rw [← MonoidalCategory.whiskerLeft_comp, Mon_.mul_one]
+  slice_lhs 3 4 => rw [← MonoidalCategory.whiskerLeft_comp, Mon_Class.mul_one]
   slice_rhs 1 2 => rw [Category.comp_id]
   monoidal
 
@@ -765,7 +765,7 @@ theorem id_whiskerLeft_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 4 4 => rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.actLeft)]
   slice_rhs 5 7 => rw [← Category.assoc, ← coequalizer.condition]
   slice_rhs 3 4 => rw [associator_inv_naturality_left]
-  slice_rhs 4 5 => rw [← comp_whiskerRight, Mon_.one_mul]
+  slice_rhs 4 5 => rw [← comp_whiskerRight, Mon_Class.one_mul]
   have : (λ_ (X.X ⊗ N.X)).inv ≫ (α_ (𝟙_ C) X.X N.X).inv ≫ ((λ_ X.X).hom ▷ N.X) = 𝟙 _ := by
     monoidal
   slice_rhs 2 4 => rw [this]
@@ -819,7 +819,7 @@ theorem whiskerRight_id_bimod {X Y : Mon_ C} {M N : Bimod X Y} (f : M ⟶ N) :
   slice_rhs 3 4 => rw [← whisker_exchange]
   slice_rhs 4 5 => rw [coequalizer.condition]
   slice_rhs 3 4 => rw [associator_naturality_right]
-  slice_rhs 4 5 => rw [← MonoidalCategory.whiskerLeft_comp, Mon_.mul_one]
+  slice_rhs 4 5 => rw [← MonoidalCategory.whiskerLeft_comp, Mon_Class.mul_one]
   simp
 
 theorem whiskerRight_comp_bimod {W X Y Z : Mon_ C} {M M' : Bimod W X} (f : M ⟶ M') (N : Bimod X Y)