chore: namespace and tidy MonCat/GroupCat adjunctions (#12948)

Author: kim-em

Mathlib/Algebra/Category/GroupCat/Adjunctions.lean

@@ -130,28 +130,20 @@ def adj : free ⊣ forget GroupCat.{u} :=
 instance : (forget GroupCat.{u}).IsRightAdjoint  :=
   ⟨_, ⟨adj⟩⟩
 
-end GroupCat
-
 section Abelianization
 
 /-- The abelianization functor `Group ⥤ CommGroup` sending a group `G` to its abelianization `Gᵃᵇ`.
  -/
 def abelianize : GroupCat.{u} ⥤ CommGroupCat.{u} where
-  obj G :=
-    { α := Abelianization G
-      str := by infer_instance }
-  map f :=
-    Abelianization.lift
-      { toFun := fun x => Abelianization.of (f x)
-        map_one' := by simp
-        map_mul' := by simp }
+  obj G := CommGroupCat.of (Abelianization G)
+  map f := Abelianization.lift (Abelianization.of.comp f)
   map_id := by
-    intros; simp only [MonoidHom.mk_coe, coe_id]
+    intros; simp only [coe_id]
     apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr; rfl
   map_comp := by
-    intros; simp only [coe_comp];
+    intros; simp only [coe_comp]
     apply (Equiv.apply_eq_iff_eq_symm_apply Abelianization.lift).mpr; rfl
-#align abelianize abelianize
+#align abelianize GroupCat.abelianize
 
 /-- The abelianization-forgetful adjuction from `Group` to `CommGroup`. -/
 def abelianizeAdj : abelianize ⊣ forget₂ CommGroupCat.{u} GroupCat.{u} :=
@@ -166,10 +158,12 @@ def abelianizeAdj : abelianize ⊣ forget₂ CommGroupCat.{u} GroupCat.{u} :=
         apply Abelianization.lift.unique
         intros
         apply Abelianization.lift.of }
-#align abelianize_adj abelianizeAdj
+#align abelianize_adj GroupCat.abelianizeAdj
 
 end Abelianization
 
+end GroupCat
+
 /-- The functor taking a monoid to its subgroup of units. -/
 @[simps]
 def MonCat.units : MonCat.{u} ⥤ GroupCat.{u} where

Mathlib/Algebra/Category/MonCat/Adjunctions.lean

@@ -27,6 +27,8 @@ universe u
 
 open CategoryTheory
 
+namespace MonCat
+
 /-- The functor of adjoining a neutral element `one` to a semigroup.
  -/
 @[to_additive (attr := simps) "The functor of adjoining a neutral element `zero` to a semigroup"]
@@ -35,18 +37,18 @@ def adjoinOne : SemigroupCat.{u} ⥤ MonCat.{u} where
   map := WithOne.map
   map_id _ := WithOne.map_id
   map_comp := WithOne.map_comp
-#align adjoin_one adjoinOne
-#align adjoin_zero adjoinZero
+#align adjoin_one MonCat.adjoinOne
+#align adjoin_zero AddMonCat.adjoinZero
 
 @[to_additive]
 instance hasForgetToSemigroup : HasForget₂ MonCat SemigroupCat where
   forget₂ :=
     { obj := fun M => SemigroupCat.of M
       map := MonoidHom.toMulHom }
 set_option linter.uppercaseLean3 false in
-#align has_forget_to_Semigroup hasForgetToSemigroup
+#align has_forget_to_Semigroup MonCat.hasForgetToSemigroup
 set_option linter.uppercaseLean3 false in
-#align has_forget_to_AddSemigroup hasForgetToAddSemigroup
+#align has_forget_to_AddSemigroup AddMonCat.hasForgetToAddSemigroup
 
 /-- The `adjoinOne`-forgetful adjunction from `SemigroupCat` to `MonCat`. -/
 @[to_additive "The `adjoinZero`-forgetful adjunction from `AddSemigroupCat` to `AddMonCat`"]
@@ -62,23 +64,25 @@ def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} SemigroupCat.{u} :=
         · rfl
         · simp
           rfl }
-#align adjoin_one_adj adjoinOneAdj
-#align adjoin_zero_adj adjoinZeroAdj
+#align adjoin_one_adj MonCat.adjoinOneAdj
+#align adjoin_zero_adj AddMonCat.adjoinZeroAdj
 
 /-- The free functor `Type u ⥤ MonCat` sending a type `X` to the free monoid on `X`. -/
 def free : Type u ⥤ MonCat.{u} where
   obj α := MonCat.of (FreeMonoid α)
   map := FreeMonoid.map
   map_id _ := FreeMonoid.hom_eq (fun _ => rfl)
   map_comp _ _ := FreeMonoid.hom_eq (fun _ => rfl)
-#align free free
+#align free MonCat.free
 
 /-- The free-forgetful adjunction for monoids. -/
 def adj : free ⊣ forget MonCat.{u} :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun X G => FreeMonoid.lift.symm
       homEquiv_naturality_left_symm := fun _ _ => FreeMonoid.hom_eq (fun _ => rfl) }
-#align adj adj
+#align adj MonCat.adj
 
 instance : (forget MonCat.{u}).IsRightAdjoint :=
   ⟨_, ⟨adj⟩⟩
+
+end MonCat