chore(CategoryTheory): namespace Mon, Grp, etc... (#30786)

YaelDillies · YaelDillies · commit 88367e02c417 · 2025-10-30T04:20:44.000Z
After this is done, we can finally rename `Mod_` to `Mod`.
diff --git a/Mathlib/CategoryTheory/Monoidal/Bimon_.lean b/Mathlib/CategoryTheory/Monoidal/Bimon_.lean
@@ -29,6 +29,7 @@ universe v₁ v₂ u₁ u₂ u
 
 open CategoryTheory MonoidalCategory
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory C]
 
 open scoped MonObj ComonObj
@@ -339,3 +340,4 @@ def mk' (X : C) [BimonObj X] : Bimon C where
       comul := .mk' (Δ : X ⟶ X ⊗ X) }
 
 end Bimon
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean
@@ -14,6 +14,7 @@ assert_not_exists Field
 
 open CategoryTheory MonoidalCategory Limits Opposite CartesianMonoidalCategory MonObj
 
+namespace CategoryTheory
 universe w v u
 variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X : C}
 
@@ -37,3 +38,4 @@ def CommGrpObj.ofRepresentableBy (F : Cᵒᵖ ⥤ CommGrpCat.{w})
 alias CommGrp_Class.ofRepresentableBy := CommGrpObj.ofRepresentableBy
 
 end CommGrp
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/CommMon_.lean
@@ -13,6 +13,7 @@ assert_not_exists MonoidWithZero
 
 open CategoryTheory MonoidalCategory Limits Opposite CartesianMonoidalCategory MonObj
 
+namespace CategoryTheory
 universe w v u
 variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X : C}
 
@@ -31,3 +32,5 @@ lemma IsCommMonObj.ofRepresentableBy (F : Cᵒᵖ ⥤ CommMonCat) (α : (F ⋙ f
 
 @[deprecated (since := "2025-09-14")]
 alias IsCommMon.ofRepresentableBy := IsCommMonObj.ofRepresentableBy
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean
@@ -19,6 +19,7 @@ universe v u
 
 noncomputable section
 
+namespace CategoryTheory
 variable (C : Type u) [Category.{v} C] [CartesianMonoidalCategory C]
 
 attribute [local simp] leftUnitor_hom rightUnitor_hom
@@ -71,3 +72,5 @@ to the category itself, via the forgetful functor.
   inverse := cartesianComon C
   unitIso := NatIso.ofComponents isoCartesianComon
   counitIso := NatIso.ofComponents (fun _ => .refl _)
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean
@@ -18,6 +18,7 @@ assert_not_exists Field
 
 open CategoryTheory MonoidalCategory Limits Opposite CartesianMonoidalCategory MonObj
 
+namespace CategoryTheory
 universe w v u
 variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
   {M G H X Y : C} [MonObj M] [GrpObj G] [GrpObj H]
@@ -69,7 +70,7 @@ abbrev Hom.group : Group (X ⟶ G) where
     _ = (f ≫ lift ι (𝟙 G)) ≫ μ := by simp
     _ = toUnit X ≫ η := by rw [Category.assoc]; simp
 
-scoped[MonObj] attribute [instance] Hom.group
+scoped[CategoryTheory.MonObj] attribute [instance] Hom.group
 
 lemma Hom.inv_def (f : X ⟶ G) : f⁻¹ = f ≫ ι := rfl
 
@@ -197,4 +198,6 @@ instance [BraidedCategory C] [IsCommMonObj G] {f : M ⟶ G} [IsMonHom f] : IsMon
 /-- 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
 
-scoped[MonObj] attribute [instance] Hom.commGroup
+scoped[CategoryTheory.MonObj] attribute [instance] Hom.commGroup
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mod_.lean
@@ -12,6 +12,7 @@ import Mathlib.CategoryTheory.Monoidal.Mod_
 
 open CategoryTheory MonoidalCategory CartesianMonoidalCategory
 
+namespace CategoryTheory
 universe v u
 variable {C : Type u} [Category.{v} C] [CartesianMonoidalCategory C]
 
@@ -29,3 +30,5 @@ attribute [local instance] ModObj.trivialAction in
 @[simps]
 def Mod_.trivialAction (M : Mon C) (X : C) : Mod_ C M.X where
   X := X
+
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
@@ -17,6 +17,7 @@ showing that it is fully faithful and its (essential) image is the representable
 
 open CategoryTheory MonoidalCategory Limits Opposite CartesianMonoidalCategory MonObj
 
+namespace CategoryTheory
 universe w v u
 variable {C D : Type*} [Category.{v} C] [CartesianMonoidalCategory C]
   [Category.{w} D] [CartesianMonoidalCategory D]
@@ -150,12 +151,12 @@ abbrev Hom.monoid : Monoid (X ⟶ M) where
       Category.comp_id, rightUnitor_hom]
     exact lift_fst _ _
 
-scoped[MonObj] attribute [instance] Hom.monoid
+scoped[CategoryTheory.MonObj] attribute [instance] Hom.monoid
 
 lemma Hom.one_def : (1 : X ⟶ M) = toUnit X ≫ η := rfl
 lemma Hom.mul_def (f₁ f₂ : X ⟶ M) : f₁ * f₂ = lift f₁ f₂ ≫ μ := rfl
 
-namespace CategoryTheory.Functor
+namespace Functor
 variable (F : C ⥤ D) [F.Monoidal]
 
 open scoped Obj
@@ -181,7 +182,7 @@ def FullyFaithful.homMulEquiv (hF : F.FullyFaithful) : (X ⟶ M) ≃* (F.obj X 
   __ := hF.homEquiv
   __ := F.homMonoidHom
 
-end CategoryTheory.Functor
+end Functor
 
 section BraidedCategory
 variable [BraidedCategory C]
@@ -190,7 +191,7 @@ 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
 
-scoped[MonObj] attribute [instance] Hom.commMonoid
+scoped[CategoryTheory.MonObj] attribute [instance] Hom.commMonoid
 
 end BraidedCategory
 
@@ -365,3 +366,4 @@ def mulEquivCongrRight (e : M ≅ N) [IsMonHom e.hom] (X : C) : (X ⟶ M) ≃* (
   ((yonedaMon.mapIso <| Mon.mkIso' e).app <| .op X).monCatIsoToMulEquiv
 
 end Hom
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean b/Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
@@ -15,6 +15,7 @@ universe v₁ v₂ v₃ u₁ u₂ u₃
 open CategoryTheory Category Limits MonoidalCategory CartesianMonoidalCategory Mon Grp CommMon
 open MonObj
 
+namespace CategoryTheory
 variable (C : Type u₁) [Category.{v₁} C] [CartesianMonoidalCategory.{v₁} C] [BraidedCategory C]
 
 /-- A commutative group object internal to a Cartesian monoidal category. -/
@@ -184,7 +185,6 @@ instance : HasInitial (CommGrp C) :=
 
 end CommGrp
 
-namespace CategoryTheory
 variable {C}
   {D : Type u₂} [Category.{v₂} D] [CartesianMonoidalCategory D] [BraidedCategory D]
   {E : Type u₃} [Category.{v₃} E] [CartesianMonoidalCategory E] [BraidedCategory E]
diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
@@ -14,6 +14,7 @@ universe v₁ v₂ v₃ u₁ u₂ u₃ u
 
 open CategoryTheory MonoidalCategory MonObj
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory.{v₁} C]
 
 variable (C) in
@@ -147,7 +148,6 @@ instance : HasInitial (CommMon C) :=
 
 end CommMon
 
-namespace CategoryTheory
 variable
   {D : Type u₂} [Category.{v₂} D] [MonoidalCategory D] [BraidedCategory D]
   {E : Type u₃} [Category.{v₃} E] [MonoidalCategory E] [BraidedCategory E]
@@ -271,11 +271,11 @@ def mapCommMon (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] [e.IsMonoid
   unitIso := mapCommMonIdIso.symm ≪≫ mapCommMonNatIso e.unitIso ≪≫ mapCommMonCompIso
   counitIso := mapCommMonCompIso.symm ≪≫ mapCommMonNatIso e.counitIso ≪≫ mapCommMonIdIso
 
-end CategoryTheory.Equivalence
+end Equivalence
 
 namespace CommMon
 
-open CategoryTheory.LaxBraidedFunctor
+open LaxBraidedFunctor
 
 namespace EquivLaxBraidedFunctorPUnit
 
@@ -355,3 +355,4 @@ def equivLaxBraidedFunctorPUnit : LaxBraidedFunctor (Discrete PUnit.{u + 1}) C 
   counitIso := counitIso C
 
 end CommMon
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Comon_.lean b/Mathlib/CategoryTheory/Monoidal/Comon_.lean
@@ -29,6 +29,7 @@ universe v₁ v₂ u₁ u₂ u
 
 open CategoryTheory MonoidalCategory
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
 
 /-- A comonoid object internal to a monoidal category.
@@ -387,7 +388,7 @@ open Functor.LaxMonoidal Functor.OplaxMonoidal
 
 end Comon
 
-namespace CategoryTheory.Functor
+namespace Functor
 
 variable {D : Type u₂} [Category.{v₂} D] [MonoidalCategory.{v₂} D]
 
@@ -444,9 +445,8 @@ def mapComon (F : C ⥤ D) [F.OplaxMonoidal] : Comon C ⥤ Comon D where
 -- TODO We haven't yet set up the category structure on `OplaxMonoidalFunctor C D`
 -- and so can't state `mapComonFunctor : OplaxMonoidalFunctor C D ⥤ Comon C ⥤ Comon D`.
 
-end CategoryTheory.Functor
+end Functor
 
-section
 variable [BraidedCategory.{v₁} C]
 
 /-- Predicate for a comonoid object to be commutative. -/
@@ -457,4 +457,4 @@ open scoped ComonObj
 
 attribute [reassoc (attr := simp)] IsCommComonObj.comul_comm
 
-end
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Grp_.lean b/Mathlib/CategoryTheory/Monoidal/Grp_.lean
@@ -22,10 +22,9 @@ universe v₁ v₂ v₃ u₁ u₂ u₃ u
 
 open CategoryTheory Category Limits MonoidalCategory CartesianMonoidalCategory Mon MonObj
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [CartesianMonoidalCategory.{v₁} C]
 
-section
-
 /-- A group object internal to a cartesian monoidal category. Also see the bundled `Grp`. -/
 class GrpObj (X : C) extends MonObj X where
   /-- The inverse in a group object -/
@@ -52,8 +51,6 @@ instance : GrpObj (𝟙_ C) where
 
 end GrpObj
 
-end
-
 variable (C) in
 /-- A group object in a Cartesian monoidal category. -/
 structure Grp where
@@ -426,7 +423,6 @@ instance instBraidedCategory : BraidedCategory (Grp C) :=
 
 end Grp
 
-namespace CategoryTheory
 variable
   {D : Type u₂} [Category.{v₂} D] [CartesianMonoidalCategory D]
   {E : Type u₃} [Category.{v₃} E] [CartesianMonoidalCategory E]
@@ -449,7 +445,7 @@ abbrev grpObjObj {G : C} [GrpObj G] : GrpObj (F.obj G) where
     simp [← Functor.map_id, Functor.Monoidal.lift_μ_assoc,
       Functor.Monoidal.toUnit_ε_assoc, ← Functor.map_comp]
 
-scoped[Obj] attribute [instance] CategoryTheory.Functor.grpObjObj
+scoped[CategoryTheory.Obj] attribute [instance] CategoryTheory.Functor.grpObjObj
 
 @[reassoc, simp] lemma obj.ι_def {G : C} [GrpObj G] : ι[F.obj G] =  F.map ι := rfl
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Hopf_.lean b/Mathlib/CategoryTheory/Monoidal/Hopf_.lean
@@ -22,6 +22,7 @@ universe v₁ v₂ u₁ u₂ u
 
 open CategoryTheory MonoidalCategory
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C] [BraidedCategory C]
 
 open scoped MonObj ComonObj
@@ -461,4 +462,4 @@ theorem antipode_antipode (A : C) [HopfObj A] (comm : (β_ _ _).hom ≫ μ[A] =
 
 end HopfObj
 
-end
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean
@@ -24,6 +24,7 @@ universe v u w
 
 noncomputable section
 
+namespace CategoryTheory
 namespace Mon
 
 variable {J : Type w} [SmallCategory J]
@@ -85,3 +86,4 @@ instance forget_preservesLimitsOfShape : PreservesLimitsOfShape J (Mon.forget C)
       (IsLimit.ofIsoLimit (limit.isLimit (F ⋙ Mon.forget C)) (forgetMapConeLimitConeIso F).symm)
 
 end Mon
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Mod_.lean b/Mathlib/CategoryTheory/Monoidal/Mod_.lean
@@ -14,6 +14,7 @@ universe v₁ v₂ u₁ u₂
 
 open CategoryTheory MonoidalCategory MonObj
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
   {D : Type u₂} [Category.{v₂} D] [MonoidalLeftAction C D]
 
@@ -42,9 +43,9 @@ class ModObj (X : D) where
 
 attribute [reassoc] ModObj.mul_smul' ModObj.one_smul'
 
-@[inherit_doc] scoped[MonObj] notation "γ" => ModObj.smul
-@[inherit_doc] scoped[MonObj] notation "γ["Y"]" => ModObj.smul (X := Y)
-@[inherit_doc] scoped[MonObj] notation "γ["N","Y"]" =>
+@[inherit_doc] scoped[CategoryTheory.MonObj] notation "γ" => ModObj.smul
+@[inherit_doc] scoped[CategoryTheory.MonObj] notation "γ["Y"]" => ModObj.smul (X := Y)
+@[inherit_doc] scoped[CategoryTheory.MonObj] notation "γ["N","Y"]" =>
   ModObj.smul (M := N) (X := Y)
 
 variable {M}
@@ -267,3 +268,4 @@ def comap {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] :
 end comap
 
 end Mod_
+end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
@@ -23,12 +23,26 @@ about morphisms from some (tensor) power of `M` to `M`, where `M` is a (commutat
 in a (braided) monoidal category.
 
 Please read the documentation in `Mathlib/Tactic/Attr/Register.lean` for full details.
+
+## TODO
+
+* Check that `Mon MonCat ≌ CommMonCat`, via the Eckmann-Hilton argument.
+  (You'll have to hook up the Cartesian monoidal structure on `MonCat` first,
+  available in https://github.com/leanprover-community/mathlib3/pull/3463)
+* More generally, check that `Mon (Mon C) ≌ CommMon C` when `C` is braided.
+* Check that `Mon TopCat ≌ [bundled topological monoids]`.
+* Check that `Mon AddCommGrpCat ≌ RingCat`.
+  (We've already got `Mon (ModuleCat R) ≌ AlgCat R`,
+  in `Mathlib/CategoryTheory/Monoidal/Internal/Module.lean`.)
+* Can you transport this monoidal structure to `RingCat` or `AlgCat R`?
+  How does it compare to the "native" one?
 -/
 
 universe w v₁ v₂ v₃ u₁ u₂ u₃ u
 
 open Function CategoryTheory MonoidalCategory Functor.LaxMonoidal Functor.OplaxMonoidal
 
+namespace CategoryTheory
 variable {C : Type u₁} [Category.{v₁} C] [MonoidalCategory.{v₁} C]
 
 /-- A monoid object internal to a monoidal category.
@@ -644,7 +658,6 @@ instance : SymmetricCategory (Mon C) where
 end Mon
 end SymmetricCategory
 
-namespace CategoryTheory
 variable
   {D : Type u₂} [Category.{v₂} D] [MonoidalCategory D]
   {E : Type u₃} [Category.{v₃} E] [MonoidalCategory E]
@@ -670,7 +683,7 @@ abbrev monObjObj : MonObj (F.obj X) where
 
 @[deprecated (since := "2025-09-09")] alias mon_ClassObj := monObjObj
 
-scoped[Obj] attribute [instance] CategoryTheory.Functor.monObjObj
+scoped[CategoryTheory.Obj] attribute [instance] CategoryTheory.Functor.monObjObj
 
 open scoped Obj
 
@@ -871,7 +884,7 @@ def mapMon (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] [e.IsMonoidal
   unitIso := mapMonIdIso.symm ≪≫ mapMonNatIso e.unitIso ≪≫ mapMonCompIso
   counitIso := mapMonCompIso.symm ≪≫ mapMonNatIso e.counitIso ≪≫ mapMonIdIso
 
-end CategoryTheory.Equivalence
+end Equivalence
 
 namespace Mon
 
@@ -1014,21 +1027,8 @@ instance [IsCommMonObj M] [IsCommMonObj N] : IsCommMonObj (M ⊗ N) where
   mul_comm := by
     simp [← IsIso.inv_comp_eq, tensorμ, ← associator_inv_naturality_left_assoc,
       ← associator_naturality_right_assoc, SymmetricCategory.braiding_swap_eq_inv_braiding M N,
-      ← tensorHom_def_assoc, -whiskerRight_tensor, -tensor_whiskerLeft,
-      MonObj.tensorObj.mul_def, ← whiskerLeft_comp_assoc, -whiskerLeft_comp]
+      ← tensorHom_def_assoc, -whiskerRight_tensor, -tensor_whiskerLeft, MonObj.tensorObj.mul_def,
+      ← MonoidalCategory.whiskerLeft_comp_assoc, -MonoidalCategory.whiskerLeft_comp]
 
 end SymmetricCategory
-
-/-!
-Projects:
-* Check that `Mon MonCat ≌ CommMonCat`, via the Eckmann-Hilton argument.
-  (You'll have to hook up the Cartesian monoidal structure on `MonCat` first,
-  available in https://github.com/leanprover-community/mathlib3/pull/3463)
-* More generally, check that `Mon (Mon C) ≌ CommMon C` when `C` is braided.
-* Check that `Mon TopCat ≌ [bundled topological monoids]`.
-* Check that `Mon AddCommGrpCat ≌ RingCat`.
-  (We've already got `Mon (ModuleCat R) ≌ AlgCat R`,
-  in `Mathlib/CategoryTheory/Monoidal/Internal/Module.lean`.)
-* Can you transport this monoidal structure to `RingCat` or `AlgCat R`?
-  How does it compare to the "native" one?
--/
+end CategoryTheory
