bump to nightly-2023-03-21-14

mathlib commit leanprover-community/mathlib@290a7ba

Mathbin/Algebra/Category/Group/Adjunctions.lean

@@ -165,16 +165,16 @@ end Abelianization
 
 /-- The functor taking a monoid to its subgroup of units. -/
 @[simps]
-def Mon.units : Mon.{u} ⥤ GroupCat.{u}
+def MonCat.units : MonCat.{u} ⥤ GroupCat.{u}
     where
   obj R := GroupCat.of Rˣ
   map R S f := GroupCat.ofHom <| Units.map f
   map_id' X := MonoidHom.ext fun x => Units.ext rfl
   map_comp' X Y Z f g := MonoidHom.ext fun x => Units.ext rfl
-#align Mon.units Mon.units
+#align Mon.units MonCat.units
 
 /-- The forgetful-units adjunction between `Group` and `Mon`. -/
-def GroupCat.forget₂MonAdj : forget₂ GroupCat Mon ⊣ Mon.units.{u}
+def GroupCat.forget₂MonAdj : forget₂ GroupCat MonCat ⊣ MonCat.units.{u}
     where
   homEquiv X Y :=
     { toFun := fun f => MonoidHom.toHomUnits f
@@ -191,21 +191,21 @@ def GroupCat.forget₂MonAdj : forget₂ GroupCat Mon ⊣ Mon.units.{u}
   homEquiv_counit X Y f := MonoidHom.ext fun _ => rfl
 #align Group.forget₂_Mon_adj GroupCat.forget₂MonAdj
 
-instance : IsRightAdjoint Mon.units.{u} :=
+instance : IsRightAdjoint MonCat.units.{u} :=
   ⟨_, GroupCat.forget₂MonAdj⟩
 
 /-- The functor taking a monoid to its subgroup of units. -/
 @[simps]
-def CommMon.units : CommMon.{u} ⥤ CommGroupCat.{u}
+def CommMonCat.units : CommMonCat.{u} ⥤ CommGroupCat.{u}
     where
   obj R := CommGroupCat.of Rˣ
   map R S f := CommGroupCat.ofHom <| Units.map f
   map_id' X := MonoidHom.ext fun x => Units.ext rfl
   map_comp' X Y Z f g := MonoidHom.ext fun x => Units.ext rfl
-#align CommMon.units CommMon.units
+#align CommMon.units CommMonCat.units
 
 /-- The forgetful-units adjunction between `CommGroup` and `CommMon`. -/
-def CommGroupCat.forget₂CommMonAdj : forget₂ CommGroupCat CommMon ⊣ CommMon.units.{u}
+def CommGroupCat.forget₂CommMonAdj : forget₂ CommGroupCat CommMonCat ⊣ CommMonCat.units.{u}
     where
   homEquiv X Y :=
     { toFun := fun f => MonoidHom.toHomUnits f
@@ -222,6 +222,6 @@ def CommGroupCat.forget₂CommMonAdj : forget₂ CommGroupCat CommMon ⊣ CommMo
   homEquiv_counit X Y f := MonoidHom.ext fun _ => rfl
 #align CommGroup.forget₂_CommMon_adj CommGroupCat.forget₂CommMonAdj
 
-instance : IsRightAdjoint CommMon.units.{u} :=
+instance : IsRightAdjoint CommMonCat.units.{u} :=
   ⟨_, CommGroupCat.forget₂CommMonAdj⟩
 

Mathbin/Algebra/Category/Group/Basic.lean

@@ -112,13 +112,13 @@ theorem ext (G H : GroupCat) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x)
 #align AddGroup.ext AddGroupCat.ext
 
 @[to_additive has_forget_to_AddMon]
-instance hasForgetToMon : HasForget₂ GroupCat Mon :=
+instance hasForgetToMon : HasForget₂ GroupCat MonCat :=
   BundledHom.forget₂ _ _
 #align Group.has_forget_to_Mon GroupCat.hasForgetToMon
 #align AddGroup.has_forget_to_AddMon AddGroupCat.hasForgetToAddMon
 
 @[to_additive]
-instance : Coe GroupCat.{u} Mon.{u} where coe := (forget₂ GroupCat Mon).obj
+instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
 
 end GroupCat
 
@@ -224,13 +224,13 @@ instance hasForgetToGroup : HasForget₂ CommGroupCat GroupCat :=
 instance : Coe CommGroupCat.{u} GroupCat.{u} where coe := (forget₂ CommGroupCat GroupCat).obj
 
 @[to_additive has_forget_to_AddCommMon]
-instance hasForgetToCommMon : HasForget₂ CommGroupCat CommMon :=
-  InducedCategory.hasForget₂ fun G : CommGroupCat => CommMon.of G
+instance hasForgetToCommMon : HasForget₂ CommGroupCat CommMonCat :=
+  InducedCategory.hasForget₂ fun G : CommGroupCat => CommMonCat.of G
 #align CommGroup.has_forget_to_CommMon CommGroupCat.hasForgetToCommMon
 #align AddCommGroup.has_forget_to_AddCommMon AddCommGroupCat.hasForgetToAddCommMon
 
 @[to_additive]
-instance : Coe CommGroupCat.{u} CommMon.{u} where coe := (forget₂ CommGroupCat CommMon).obj
+instance : Coe CommGroupCat.{u} CommMonCat.{u} where coe := (forget₂ CommGroupCat CommMonCat).obj
 
 end CommGroupCat
 

Mathbin/Algebra/Category/Group/FilteredColimits.lean

@@ -43,7 +43,7 @@ namespace GroupCat.FilteredColimits
 
 section
 
-open Mon.FilteredColimits (colimit_one_eq colimit_mul_mk_eq)
+open MonCat.FilteredColimits (colimit_one_eq colimit_mul_mk_eq)
 
 -- We use parameters here, mainly so we can have the abbreviations `G` and `G.mk` below, without
 -- passing around `F` all the time.
@@ -54,8 +54,8 @@ In the following, we will show that this has the structure of a group.
 -/
 @[to_additive
       "The colimit of `F ⋙ forget₂ AddGroup AddMon` in the category `AddMon`.\nIn the following, we will show that this has the structure of an additive group."]
-abbrev g : Mon :=
-  Mon.FilteredColimits.colimit (F ⋙ forget₂ GroupCat Mon.{max v u})
+abbrev g : MonCat :=
+  MonCat.FilteredColimits.colimit (F ⋙ forget₂ GroupCat MonCat.{max v u})
 #align Group.filtered_colimits.G GroupCat.FilteredColimits.g
 #align AddGroup.filtered_colimits.G AddGroupCat.FilteredColimits.g
 
@@ -118,8 +118,8 @@ instance colimitGroup : Group G :=
       apply Quot.inductionOn x; clear x; intro x
       cases' x with j x
       erw [colimit_inv_mk_eq,
-        colimit_mul_mk_eq (F ⋙ forget₂ GroupCat Mon.{max v u}) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
-        colimit_one_eq (F ⋙ forget₂ GroupCat Mon.{max v u}) j]
+        colimit_mul_mk_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j),
+        colimit_one_eq (F ⋙ forget₂ GroupCat MonCat.{max v u}) j]
       dsimp
       simp only [CategoryTheory.Functor.map_id, id_apply, mul_left_inv] }
 #align Group.filtered_colimits.colimit_group GroupCat.FilteredColimits.colimitGroup
@@ -136,7 +136,7 @@ def colimit : GroupCat :=
 @[to_additive "The cocone over the proposed colimit additive group."]
 def colimitCocone : cocone F where
   pt := colimit
-  ι := { (Mon.FilteredColimits.colimitCocone (F ⋙ forget₂ GroupCat Mon.{max v u})).ι with }
+  ι := { (MonCat.FilteredColimits.colimitCocone (F ⋙ forget₂ GroupCat MonCat.{max v u})).ι with }
 #align Group.filtered_colimits.colimit_cocone GroupCat.FilteredColimits.colimitCocone
 #align AddGroup.filtered_colimits.colimit_cocone AddGroupCat.FilteredColimits.colimitCocone
 
@@ -145,8 +145,8 @@ def colimitCocone : cocone F where
 def colimitCoconeIsColimit : IsColimit colimit_cocone
     where
   desc t :=
-    Mon.FilteredColimits.colimitDesc (F ⋙ forget₂ GroupCat Mon.{max v u})
-      ((forget₂ GroupCat Mon).mapCocone t)
+    MonCat.FilteredColimits.colimitDesc (F ⋙ forget₂ GroupCat MonCat.{max v u})
+      ((forget₂ GroupCat MonCat).mapCocone t)
   fac t j :=
     MonoidHom.coe_inj <|
       (Types.colimitCoconeIsColimit (F ⋙ forget GroupCat)).fac ((forget GroupCat).mapCocone t) j
@@ -158,18 +158,19 @@ def colimitCoconeIsColimit : IsColimit colimit_cocone
 #align AddGroup.filtered_colimits.colimit_cocone_is_colimit AddGroupCat.FilteredColimits.colimitCoconeIsColimit
 
 @[to_additive forget₂_AddMon_preserves_filtered_colimits]
-instance forget₂MonPreservesFilteredColimits : PreservesFilteredColimits (forget₂ GroupCat Mon.{u})
+instance forget₂MonPreservesFilteredColimits :
+    PreservesFilteredColimits (forget₂ GroupCat MonCat.{u})
     where PreservesFilteredColimits J _ _ :=
     {
       PreservesColimit := fun F =>
         preserves_colimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
-          (Mon.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ GroupCat Mon.{u})) }
+          (MonCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ GroupCat MonCat.{u})) }
 #align Group.filtered_colimits.forget₂_Mon_preserves_filtered_colimits GroupCat.FilteredColimits.forget₂MonPreservesFilteredColimits
 #align AddGroup.filtered_colimits.forget₂_AddMon_preserves_filtered_colimits AddGroupCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits
 
 @[to_additive]
 instance forgetPreservesFilteredColimits : PreservesFilteredColimits (forget GroupCat.{u}) :=
-  Limits.compPreservesFilteredColimits (forget₂ GroupCat Mon) (forget Mon.{u})
+  Limits.compPreservesFilteredColimits (forget₂ GroupCat MonCat) (forget MonCat.{u})
 #align Group.filtered_colimits.forget_preserves_filtered_colimits GroupCat.FilteredColimits.forgetPreservesFilteredColimits
 #align AddGroup.filtered_colimits.forget_preserves_filtered_colimits AddGroupCat.FilteredColimits.forgetPreservesFilteredColimits
 
@@ -198,7 +199,8 @@ abbrev g : GroupCat :=
 @[to_additive]
 instance colimitCommGroup : CommGroup G :=
   { G.Group,
-    CommMon.FilteredColimits.colimitCommMonoid (F ⋙ forget₂ CommGroupCat CommMon.{max v u}) with }
+    CommMonCat.FilteredColimits.colimitCommMonoid
+      (F ⋙ forget₂ CommGroupCat CommMonCat.{max v u}) with }
 #align CommGroup.filtered_colimits.colimit_comm_group CommGroupCat.FilteredColimits.colimitCommGroup
 #align AddCommGroup.filtered_colimits.colimit_add_comm_group AddCommGroupCat.FilteredColimits.colimitAddCommGroup
 

Mathbin/Algebra/Category/Group/Limits.lean

@@ -49,9 +49,9 @@ instance groupObj (F : J ⥤ GroupCat.{max v u}) (j) : Group ((F ⋙ forget Grou
       "The flat sections of a functor into `AddGroup` form an additive subgroup of all sections."]
 def sectionsSubgroup (F : J ⥤ GroupCat) : Subgroup (∀ j, F.obj j) :=
   {
-    Mon.sectionsSubmonoid
+    MonCat.sectionsSubmonoid
       (F ⋙ forget₂ GroupCat
-          Mon) with
+          MonCat) with
     carrier := (F ⋙ forget GroupCat).sections
     inv_mem' := fun a ah j j' f =>
       by
@@ -77,17 +77,18 @@ the existing limit. -/
 @[to_additive
       "We show that the forgetful functor `AddGroup ⥤ AddMon` creates limits.\n\nAll we need to do is notice that the limit point has an `add_group` instance available, and then\nreuse the existing limit."]
 instance Forget₂.createsLimit (F : J ⥤ GroupCat.{max v u}) :
-    CreatesLimit F (forget₂ GroupCat.{max v u} Mon.{max v u}) :=
+    CreatesLimit F (forget₂ GroupCat.{max v u} MonCat.{max v u}) :=
   createsLimitOfReflectsIso fun c' t =>
     { liftedCone :=
         { pt := GroupCat.of (Types.limitCone (F ⋙ forget GroupCat)).pt
           π :=
-            { app := Mon.limitπMonoidHom (F ⋙ forget₂ GroupCat Mon.{max v u})
+            { app := MonCat.limitπMonoidHom (F ⋙ forget₂ GroupCat MonCat.{max v u})
               naturality' :=
-                (Mon.HasLimits.limitCone (F ⋙ forget₂ GroupCat Mon.{max v u})).π.naturality } }
-      validLift := by apply is_limit.unique_up_to_iso (Mon.HasLimits.limitConeIsLimit _) t
+                (MonCat.HasLimits.limitCone
+                      (F ⋙ forget₂ GroupCat MonCat.{max v u})).π.naturality } }
+      validLift := by apply is_limit.unique_up_to_iso (MonCat.HasLimits.limitConeIsLimit _) t
       makesLimit :=
-        IsLimit.ofFaithful (forget₂ GroupCat Mon.{max v u}) (Mon.HasLimits.limitConeIsLimit _)
+        IsLimit.ofFaithful (forget₂ GroupCat MonCat.{max v u}) (MonCat.HasLimits.limitConeIsLimit _)
           (fun s => _) fun s => rfl }
 #align Group.forget₂.creates_limit GroupCat.Forget₂.createsLimit
 #align AddGroup.forget₂.creates_limit AddGroupCat.Forget₂.createsLimit
@@ -98,7 +99,7 @@ instance Forget₂.createsLimit (F : J ⥤ GroupCat.{max v u}) :
 @[to_additive
       "A choice of limit cone for a functor into `Group`.\n(Generally, you'll just want to use `limit F`.)"]
 def limitCone (F : J ⥤ GroupCat.{max v u}) : Cone F :=
-  liftLimit (limit.isLimit (F ⋙ forget₂ GroupCat Mon.{max v u}))
+  liftLimit (limit.isLimit (F ⋙ forget₂ GroupCat MonCat.{max v u}))
 #align Group.limit_cone GroupCat.limitCone
 #align AddGroup.limit_cone AddGroupCat.limitCone
 
@@ -116,7 +117,7 @@ def limitConeIsLimit (F : J ⥤ GroupCat.{max v u}) : IsLimit (limitCone F) :=
 @[to_additive "The category of additive groups has all limits."]
 instance hasLimitsOfSize : HasLimitsOfSize.{v, v} GroupCat.{max v u}
     where HasLimitsOfShape J 𝒥 :=
-    { HasLimit := fun F => has_limit_of_created F (forget₂ GroupCat Mon.{max v u}) }
+    { HasLimit := fun F => has_limit_of_created F (forget₂ GroupCat MonCat.{max v u}) }
 #align Group.has_limits_of_size GroupCat.hasLimitsOfSize
 #align AddGroup.has_limits_of_size AddGroupCat.hasLimitsOfSize
 
@@ -133,13 +134,13 @@ This means the underlying monoid of a limit can be computed as a limit in the ca
 @[to_additive AddGroupCat.forget₂AddMonPreservesLimits
       "The forgetful functor from additive groups\nto additive monoids preserves all limits.\n\nThis means the underlying additive monoid of a limit can be computed as a limit in the category of\nadditive monoids."]
 instance forget₂MonPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ GroupCat Mon.{max v u})
+    PreservesLimitsOfSize.{v, v} (forget₂ GroupCat MonCat.{max v u})
     where PreservesLimitsOfShape J 𝒥 := { PreservesLimit := fun F => by infer_instance }
 #align Group.forget₂_Mon_preserves_limits_of_size GroupCat.forget₂MonPreservesLimitsOfSize
 #align AddGroup.forget₂_AddMon_preserves_limits AddGroupCat.forget₂AddMonPreservesLimits
 
 @[to_additive]
-instance forget₂MonPreservesLimits : PreservesLimits (forget₂ GroupCat Mon.{u}) :=
+instance forget₂MonPreservesLimits : PreservesLimits (forget₂ GroupCat MonCat.{u}) :=
   GroupCat.forget₂MonPreservesLimitsOfSize.{u, u}
 #align Group.forget₂_Mon_preserves_limits GroupCat.forget₂MonPreservesLimits
 #align AddGroup.forget₂_Mon_preserves_limits AddGroupCat.forget₂MonPreservesLimits
@@ -151,7 +152,9 @@ This means the underlying type of a limit can be computed as a limit in the cate
       "The forgetful functor from additive groups to types preserves all limits.\n\nThis means the underlying type of a limit can be computed as a limit in the category of types."]
 instance forgetPreservesLimitsOfSize : PreservesLimitsOfSize.{v, v} (forget GroupCat.{max v u})
     where PreservesLimitsOfShape J 𝒥 :=
-    { PreservesLimit := fun F => limits.comp_preserves_limit (forget₂ GroupCat Mon) (forget Mon) }
+    {
+      PreservesLimit := fun F =>
+        limits.comp_preserves_limit (forget₂ GroupCat MonCat) (forget MonCat) }
 #align Group.forget_preserves_limits_of_size GroupCat.forgetPreservesLimitsOfSize
 #align AddGroup.forget_preserves_limits_of_size AddGroupCat.forgetPreservesLimitsOfSize
 
@@ -196,13 +199,13 @@ instance Forget₂.createsLimit (F : J ⥤ CommGroupCat.{max v u}) :
         { pt := CommGroupCat.of (Types.limitCone (F ⋙ forget CommGroupCat)).pt
           π :=
             { app :=
-                Mon.limitπMonoidHom
-                  (F ⋙ forget₂ CommGroupCat GroupCat.{max v u} ⋙ forget₂ GroupCat Mon.{max v u})
-              naturality' := (Mon.HasLimits.limitCone _).π.naturality } }
+                MonCat.limitπMonoidHom
+                  (F ⋙ forget₂ CommGroupCat GroupCat.{max v u} ⋙ forget₂ GroupCat MonCat.{max v u})
+              naturality' := (MonCat.HasLimits.limitCone _).π.naturality } }
       validLift := by apply is_limit.unique_up_to_iso (GroupCat.limitConeIsLimit _) t
       makesLimit :=
-        IsLimit.ofFaithful (forget₂ _ GroupCat.{max v u} ⋙ forget₂ _ Mon.{max v u})
-          (by apply Mon.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }
+        IsLimit.ofFaithful (forget₂ _ GroupCat.{max v u} ⋙ forget₂ _ MonCat.{max v u})
+          (by apply MonCat.HasLimits.limitConeIsLimit _) (fun s => _) fun s => rfl }
 #align CommGroup.forget₂.creates_limit CommGroupCat.Forget₂.createsLimit
 #align AddCommGroup.forget₂.creates_limit AddCommGroupCat.Forget₂.createsLimit
 
@@ -263,8 +266,8 @@ instance forget₂GroupPreservesLimits : PreservesLimits (forget₂ CommGroupCat
 @[to_additive AddCommGroupCat.forget₂AddCommMonPreservesLimitsAux
       "An auxiliary declaration to speed up typechecking."]
 def forget₂CommMonPreservesLimitsAux (F : J ⥤ CommGroupCat.{max v u}) :
-    IsLimit ((forget₂ CommGroupCat CommMon).mapCone (limitCone F)) :=
-  CommMon.limitConeIsLimit (F ⋙ forget₂ CommGroupCat CommMon)
+    IsLimit ((forget₂ CommGroupCat CommMonCat).mapCone (limitCone F)) :=
+  CommMonCat.limitConeIsLimit (F ⋙ forget₂ CommGroupCat CommMonCat)
 #align CommGroup.forget₂_CommMon_preserves_limits_aux CommGroupCat.forget₂CommMonPreservesLimitsAux
 #align AddCommGroup.forget₂_AddCommMon_preserves_limits_aux AddCommGroupCat.forget₂AddCommMonPreservesLimitsAux
 
@@ -275,7 +278,7 @@ in the category of commutative monoids.)
 @[to_additive AddCommGroupCat.forget₂AddCommMonPreservesLimits
       "The forgetful functor from additive commutative groups to additive commutative monoids preserves\nall limits. (That is, the underlying additive commutative monoids could have been computed instead\nas limits in the category of additive commutative monoids.)"]
 instance forget₂CommMonPreservesLimitsOfSize :
-    PreservesLimitsOfSize.{v, v} (forget₂ CommGroupCat CommMon.{max v u})
+    PreservesLimitsOfSize.{v, v} (forget₂ CommGroupCat CommMonCat.{max v u})
     where PreservesLimitsOfShape J 𝒥 :=
     {
       PreservesLimit := fun F =>

Mathbin/Algebra/Category/GroupWithZero.lean

@@ -63,7 +63,7 @@ instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed
       map := fun X Y f => ⟨f, f.map_zero', f.map_one'⟩ }
 #align GroupWithZero.has_forget_to_Bipointed GroupWithZeroCat.hasForgetToBipointed
 
-instance hasForgetToMon : HasForget₂ GroupWithZeroCat Mon
+instance hasForgetToMon : HasForget₂ GroupWithZeroCat MonCat
     where forget₂ :=
     { obj := fun X => ⟨X⟩
       map := fun X Y => MonoidWithZeroHom.toMonoidHom }

Mathbin/Algebra/Category/Module/FilteredColimits.lean

@@ -39,7 +39,7 @@ open CategoryTheory.Limits
 open CategoryTheory.IsFiltered renaming max → max'
 
 -- avoid name collision with `_root_.max`.
-open AddMon.FilteredColimits (colimit_zero_eq colimit_add_mk_eq)
+open AddMonCat.FilteredColimits (colimit_zero_eq colimit_add_mk_eq)
 
 namespace ModuleCat.FilteredColimits
 

Mathbin/Algebra/Category/Mon/Adjunctions.lean

@@ -33,17 +33,17 @@ open CategoryTheory
 /-- The functor of adjoining a neutral element `one` to a semigroup.
  -/
 @[to_additive "The functor of adjoining a neutral element `zero` to a semigroup", simps]
-def adjoinOne : SemigroupCat.{u} ⥤ Mon.{u}
+def adjoinOne : SemigroupCat.{u} ⥤ MonCat.{u}
     where
-  obj S := Mon.of (WithOne S)
+  obj S := MonCat.of (WithOne S)
   map X Y := WithOne.map
   map_id' X := WithOne.map_id
   map_comp' X Y Z := WithOne.map_comp
 #align adjoin_one adjoinOne
 #align adjoin_zero adjoinZero
 
 @[to_additive hasForgetToAddSemigroup]
-instance hasForgetToSemigroup : HasForget₂ Mon SemigroupCat
+instance hasForgetToSemigroup : HasForget₂ MonCat SemigroupCat
     where forget₂ :=
     { obj := fun M => SemigroupCat.of M
       map := fun M N => MonoidHom.toMulHom }
@@ -52,7 +52,7 @@ instance hasForgetToSemigroup : HasForget₂ Mon SemigroupCat
 
 /-- The adjoin_one-forgetful adjunction from `Semigroup` to `Mon`.-/
 @[to_additive "The adjoin_one-forgetful adjunction from `AddSemigroup` to `AddMon`"]
-def adjoinOneAdj : adjoinOne ⊣ forget₂ Mon.{u} SemigroupCat.{u} :=
+def adjoinOneAdj : adjoinOne ⊣ forget₂ MonCat.{u} SemigroupCat.{u} :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun S M => WithOne.lift.symm
       homEquiv_naturality_left_symm := by
@@ -67,8 +67,9 @@ def adjoinOneAdj : adjoinOne ⊣ forget₂ Mon.{u} SemigroupCat.{u} :=
 #align adjoin_zero_adj adjoinZeroAdj
 
 /-- The free functor `Type u ⥤ Mon` sending a type `X` to the free monoid on `X`. -/
-def free : Type u ⥤ Mon.{u} where
-  obj α := Mon.of (FreeMonoid α)
+def free : Type u ⥤ MonCat.{u}
+    where
+  obj α := MonCat.of (FreeMonoid α)
   map X Y := FreeMonoid.map
   map_id' := by
     intros
@@ -81,7 +82,7 @@ def free : Type u ⥤ Mon.{u} where
 #align free free
 
 /-- The free-forgetful adjunction for monoids. -/
-def adj : free ⊣ forget Mon.{u} :=
+def adj : free ⊣ forget MonCat.{u} :=
   Adjunction.mkOfHomEquiv
     { homEquiv := fun X G => FreeMonoid.lift.symm
       homEquiv_naturality_left_symm := fun X Y G f g =>
@@ -90,6 +91,6 @@ def adj : free ⊣ forget Mon.{u} :=
         rfl }
 #align adj adj
 
-instance : IsRightAdjoint (forget Mon.{u}) :=
+instance : IsRightAdjoint (forget MonCat.{u}) :=
   ⟨_, adj⟩