chore: Rename to Grp (#3731)

This is a proposal to rename what was in mathlib `Group` and in mathlib4 `GroupCat` to its literature name `Grp`. This has the advantage not to conflict with `group` that has been capitalised to `Group` and to be shorter.

Mathlib.lean

@@ -56,25 +56,25 @@ import Mathlib.Algebra.Category.BoolRing
 import Mathlib.Algebra.Category.CoalgebraCat.Basic
 import Mathlib.Algebra.Category.FGModuleCat.Basic
 import Mathlib.Algebra.Category.FGModuleCat.Limits
-import Mathlib.Algebra.Category.GroupCat.Abelian
-import Mathlib.Algebra.Category.GroupCat.Adjunctions
-import Mathlib.Algebra.Category.GroupCat.Basic
-import Mathlib.Algebra.Category.GroupCat.Biproducts
-import Mathlib.Algebra.Category.GroupCat.Colimits
-import Mathlib.Algebra.Category.GroupCat.EnoughInjectives
-import Mathlib.Algebra.Category.GroupCat.EpiMono
-import Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup
-import Mathlib.Algebra.Category.GroupCat.FilteredColimits
-import Mathlib.Algebra.Category.GroupCat.ForgetCorepresentable
-import Mathlib.Algebra.Category.GroupCat.Images
-import Mathlib.Algebra.Category.GroupCat.Injective
-import Mathlib.Algebra.Category.GroupCat.Kernels
-import Mathlib.Algebra.Category.GroupCat.Limits
-import Mathlib.Algebra.Category.GroupCat.Preadditive
-import Mathlib.Algebra.Category.GroupCat.Subobject
-import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
-import Mathlib.Algebra.Category.GroupCat.Zero
-import Mathlib.Algebra.Category.GroupWithZeroCat
+import Mathlib.Algebra.Category.Grp.Abelian
+import Mathlib.Algebra.Category.Grp.Adjunctions
+import Mathlib.Algebra.Category.Grp.Basic
+import Mathlib.Algebra.Category.Grp.Biproducts
+import Mathlib.Algebra.Category.Grp.Colimits
+import Mathlib.Algebra.Category.Grp.EnoughInjectives
+import Mathlib.Algebra.Category.Grp.EpiMono
+import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
+import Mathlib.Algebra.Category.Grp.FilteredColimits
+import Mathlib.Algebra.Category.Grp.ForgetCorepresentable
+import Mathlib.Algebra.Category.Grp.Images
+import Mathlib.Algebra.Category.Grp.Injective
+import Mathlib.Algebra.Category.Grp.Kernels
+import Mathlib.Algebra.Category.Grp.Limits
+import Mathlib.Algebra.Category.Grp.Preadditive
+import Mathlib.Algebra.Category.Grp.Subobject
+import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
+import Mathlib.Algebra.Category.Grp.Zero
+import Mathlib.Algebra.Category.GrpWithZero
 import Mathlib.Algebra.Category.ModuleCat.Abelian
 import Mathlib.Algebra.Category.ModuleCat.Adjunctions
 import Mathlib.Algebra.Category.ModuleCat.Algebra
@@ -122,7 +122,7 @@ import Mathlib.Algebra.Category.Ring.Constructions
 import Mathlib.Algebra.Category.Ring.FilteredColimits
 import Mathlib.Algebra.Category.Ring.Instances
 import Mathlib.Algebra.Category.Ring.Limits
-import Mathlib.Algebra.Category.SemigroupCat.Basic
+import Mathlib.Algebra.Category.Semigrp.Basic
 import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.Basic
 import Mathlib.Algebra.CharP.CharAndCard
@@ -1041,9 +1041,9 @@ import Mathlib.Analysis.Normed.Group.InfiniteSum
 import Mathlib.Analysis.Normed.Group.Lemmas
 import Mathlib.Analysis.Normed.Group.Pointwise
 import Mathlib.Analysis.Normed.Group.Quotient
-import Mathlib.Analysis.Normed.Group.SemiNormedGroupCat
-import Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Completion
-import Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Kernels
+import Mathlib.Analysis.Normed.Group.SemiNormedGrp
+import Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
+import Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
 import Mathlib.Analysis.Normed.Group.Seminorm
 import Mathlib.Analysis.Normed.Group.Tannery
 import Mathlib.Analysis.Normed.Group.ZeroAtInfty

Mathlib/Algebra/Category/GroupCat/Abelian.lean → Mathlib/Algebra/Category/Grp/Abelian.lean

@@ -3,11 +3,11 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
-import Mathlib.Algebra.Category.GroupCat.Colimits
-import Mathlib.Algebra.Category.GroupCat.FilteredColimits
-import Mathlib.Algebra.Category.GroupCat.Kernels
-import Mathlib.Algebra.Category.GroupCat.Limits
-import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
+import Mathlib.Algebra.Category.Grp.Colimits
+import Mathlib.Algebra.Category.Grp.FilteredColimits
+import Mathlib.Algebra.Category.Grp.Kernels
+import Mathlib.Algebra.Category.Grp.Limits
+import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
 import Mathlib.Algebra.Category.ModuleCat.Abelian
 import Mathlib.CategoryTheory.Abelian.FunctorCategory
 import Mathlib.CategoryTheory.Limits.ConcreteCategory
@@ -24,26 +24,26 @@ universe u
 
 noncomputable section
 
-namespace AddCommGroupCat
+namespace AddCommGrp
 
-variable {X Y Z : AddCommGroupCat.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
+variable {X Y Z : AddCommGrp.{u}} (f : X ⟶ Y) (g : Y ⟶ Z)
 
 /-- In the category of abelian groups, every monomorphism is normal. -/
 def normalMono (_ : Mono f) : NormalMono f :=
-  equivalenceReflectsNormalMono (forget₂ (ModuleCat.{u} ℤ) AddCommGroupCat.{u}).inv <|
+  equivalenceReflectsNormalMono (forget₂ (ModuleCat.{u} ℤ) AddCommGrp.{u}).inv <|
     ModuleCat.normalMono _ inferInstance
 set_option linter.uppercaseLean3 false in
-#align AddCommGroup.normal_mono AddCommGroupCat.normalMono
+#align AddCommGroup.normal_mono AddCommGrp.normalMono
 
 /-- In the category of abelian groups, every epimorphism is normal. -/
 def normalEpi (_ : Epi f) : NormalEpi f :=
-  equivalenceReflectsNormalEpi (forget₂ (ModuleCat.{u} ℤ) AddCommGroupCat.{u}).inv <|
+  equivalenceReflectsNormalEpi (forget₂ (ModuleCat.{u} ℤ) AddCommGrp.{u}).inv <|
     ModuleCat.normalEpi _ inferInstance
 set_option linter.uppercaseLean3 false in
-#align AddCommGroup.normal_epi AddCommGroupCat.normalEpi
+#align AddCommGroup.normal_epi AddCommGrp.normalEpi
 
 /-- The category of abelian groups is abelian. -/
-instance : Abelian AddCommGroupCat.{u} where
+instance : Abelian AddCommGrp.{u} where
   has_finite_products := ⟨HasFiniteProducts.out⟩
   normalMonoOfMono := normalMono
   normalEpiOfEpi := normalEpi
@@ -58,7 +58,7 @@ theorem exact_iff : Exact f g ↔ f.range = g.ker := by
 
 /-- The category of abelian groups satisfies Grothedieck's Axiom AB5. -/
 instance {J : Type u} [SmallCategory J] [IsFiltered J] :
-    PreservesFiniteLimits <| colim (J := J) (C := AddCommGroupCat.{u}) := by
+    PreservesFiniteLimits <| colim (J := J) (C := AddCommGrp.{u}) := by
   refine Functor.preservesFiniteLimitsOfMapExact _
     fun F G H η γ h => (exact_iff _ _).mpr (le_antisymm ?_ ?_)
   all_goals replace h : ∀ j : J, Exact (η.app j) (γ.app j) :=
@@ -77,4 +77,4 @@ instance {J : Type u} [SmallCategory J] [IsFiltered J] :
     erw [← comp_apply, colimit.ι_map, comp_apply, ht]
     exact colimit.w_apply G e₁ y
 
-end AddCommGroupCat
+end AddCommGrp