feat: commutative monoids are internal monoids (#29765)

From Toric

Author: YaelDillies

Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.Algebra.Category.Grp.Limits
+import Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_
 import Mathlib.CategoryTheory.Monoidal.Grp_
 
 /-!
@@ -188,15 +189,60 @@ lemma GrpObj.one_inv : η[G] ≫ ι = η := by simp [GrpObj.inv_eq_inv, GrpObj.c
 
 @[deprecated (since := "2025-09-13")] alias Grp_Class.inv_eq_inv := GrpObj.inv_eq_inv
 
-instance [BraidedCategory C] [IsCommMonObj G] : IsMonHom ι[G] where
+variable [BraidedCategory C]
+
+instance [IsCommMonObj G] : IsMonHom ι[G] where
   one_hom := by simp [one_eq_one, ← Hom.inv_def]
   mul_hom := by simp [GrpObj.mul_inv_rev]
 
 attribute [local simp] Hom.inv_def in
-instance [BraidedCategory C] [IsCommMonObj G] {f : M ⟶ G} [IsMonHom f] : IsMonHom f⁻¹ where
+instance [IsCommMonObj G] {f : M ⟶ G} [IsMonHom f] : IsMonHom f⁻¹ where
+
+namespace Grp
+variable {G H : Grp C} [IsCommMonObj H.X]
+
+instance : MonObj H where
+  one := η[H.toMon]
+  mul := μ[H.toMon]
+  one_mul := MonObj.one_mul H.toMon
+  mul_one := MonObj.mul_one H.toMon
+  mul_assoc := MonObj.mul_assoc H.toMon
+
+@[simp] lemma hom_one (H : Grp C) [IsCommMonObj H.X] : η[H].hom = η[H.X] := rfl
+@[simp] lemma hom_mul (H : Grp C) [IsCommMonObj H.X] : μ[H].hom = μ[H.X] := rfl
+
+namespace Hom
+
+@[simp] lemma hom_one : (1 : G ⟶ H).hom = 1 := rfl
+@[simp] lemma hom_mul (f g : G ⟶ H) : (f * g).hom = f.hom * g.hom := rfl
+@[simp] lemma hom_pow (f : G ⟶ H) (n : ℕ) : (f ^ n).hom = f.hom ^ n := Mon.Hom.hom_pow ..
+
+end Hom
+
+attribute [local simp] mul_eq_mul GrpObj.inv_eq_inv comp_mul in
+/-- A commutative group object is a group object in the category of group objects. -/
+instance : GrpObj H where inv := .mk ι[H.X]
+
+namespace Hom
+
+@[simp] lemma hom_inv (f : G ⟶ H) : f⁻¹.hom = f.hom⁻¹ := rfl
+@[simp] lemma hom_div (f g : G ⟶ H) : (f / g).hom = f.hom / g.hom := rfl
+@[simp] lemma hom_zpow (f : G ⟶ H) (n : ℤ) : (f ^ n).hom = f.hom ^ n := by cases n <;> simp
+
+end Hom
+
+attribute [local simp] mul_eq_mul comp_mul mul_comm mul_div_mul_comm in
+/-- A commutative group object is a commutative group object in the category of group objects. -/
+instance : IsCommMonObj H where
+
+instance [IsCommMonObj G.X] (f : G ⟶ H) : IsMonHom f where
+  one_hom := by ext; simp [Grp.instMonObj]
+  mul_hom := by ext; simp [Grp.instMonObj]
+
+end Grp
 
 /-- If `G` is a commutative group object, then `Hom(X, G)` has a commutative group structure. -/
-abbrev Hom.commGroup [BraidedCategory C] [IsCommMonObj G] : CommGroup (X ⟶ G) where
+abbrev Hom.commGroup [IsCommMonObj G] : CommGroup (X ⟶ G) where
 
 scoped[CategoryTheory.MonObj] attribute [instance] Hom.commGroup
 

Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean

@@ -64,8 +64,7 @@ end MonObj
 namespace Mon
 variable [BraidedCategory C]
 
-attribute [local simp] tensorObj.one_def tensorObj.mul_def
-
+attribute [local simp] tensorObj.one_def tensorObj.mul_def in
 instance : CartesianMonoidalCategory (Mon C) where
   isTerminalTensorUnit := .ofUniqueHom (fun M ↦ ⟨toUnit _⟩) fun M f ↦ by ext; exact toUnit_unique ..
   fst M N := .mk (fst M.X N.X)
@@ -76,12 +75,25 @@ instance : CartesianMonoidalCategory (Mon C) where
   fst_def M N := by ext; simp [fst_def]; congr
   snd_def M N := by ext; simp [snd_def]; congr
 
-variable {M N₁ N₂ : Mon C}
+variable {M N N₁ N₂ : Mon C}
 
 @[simp] lemma lift_hom (f : M ⟶ N₁) (g : M ⟶ N₂) : (lift f g).hom = lift f.hom g.hom := rfl
 @[simp] lemma fst_hom (M N : Mon C) : (fst M N).hom = fst M.X N.X := rfl
 @[simp] lemma snd_hom (M N : Mon C) : (snd M N).hom = snd M.X N.X := rfl
 
+/-! ### Comm monoid objects are internal monoid objects -/
+
+/-- A commutative monoid object is a monoid object in the category of monoid objects. -/
+instance [IsCommMonObj M.X] : MonObj M where
+  one := .mk η[M.X]
+  mul := .mk μ[M.X]
+
+@[simp] lemma hom_one (M : Mon C) [IsCommMonObj M.X] : η[M].hom = η[M.X] := rfl
+@[simp] lemma hom_mul (M : Mon C) [IsCommMonObj M.X] : μ[M].hom = μ[M.X] := rfl
+
+/-- A commutative monoid object is a commutative monoid object in the category of monoid objects. -/
+instance [IsCommMonObj M.X] : IsCommMonObj M where
+
 end Mon
 
 variable (X) in
@@ -188,6 +200,16 @@ variable [BraidedCategory C]
 abbrev Hom.commMonoid [IsCommMonObj M] : CommMonoid (X ⟶ M) where
   mul_comm f g := by simpa [-IsCommMonObj.mul_comm] using lift g f ≫= IsCommMonObj.mul_comm M
 
+namespace Mon.Hom
+variable {M N : Mon C} [IsCommMonObj N.X]
+
+@[simp] lemma hom_one : (1 : M ⟶ N).hom = 1 := rfl
+@[simp] lemma hom_mul (f g : M ⟶ N) : (f * g).hom = f.hom * g.hom := rfl
+@[simp] lemma hom_pow (f : M ⟶ N) (n : ℕ) : (f ^ n).hom = f.hom ^ n := by
+  induction n <;> simp [pow_succ, *]
+
+end Mon.Hom
+
 scoped[CategoryTheory.MonObj] attribute [instance] Hom.commMonoid
 
 end BraidedCategory

Mathlib/CategoryTheory/Monoidal/Grp_.lean

@@ -65,8 +65,8 @@ attribute [instance] Grp.grp
 namespace Grp
 
 /-- A group object is a monoid object. -/
-@[simps X]
-def toMon (A : Grp C) : Mon C := ⟨A.X⟩
+@[simps -isSimp X]
+abbrev toMon (A : Grp C) : Mon C := ⟨A.X⟩
 
 @[deprecated (since := "2025-09-15")] alias toMon_ := toMon