[Merged by Bors] - chore: Rename to Grp

[YaelDillies]

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.

---

A similar decision could be applied to ModuleCat and MonCat.

[joelriou]

The Cat suffix was added intentionally, see
https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#categories "Categories are suffixed with Cat"

[YaelDillies]

Yes I know. This is an alternative to that last resort solution.

[fpvandoorn]

Please reach a consensus about this renaming on Zulip first

[YaelDillies]

It seems like the consensus is that this is a good thing. @semorrison, can you confirm?

[urkud]

Could you link to Zulip discussion, please?

[YaelDillies]

See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention/near/354445098 and below.

[github-actions]

Import summary

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup	490	0	-490 (-100.00%)
Mathlib.Analysis.Normed.Group.SemiNormedGroupCat	1114	0	-1114 (-100.00%)

[github-actions]

PR summary d7c9e44165

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Category.GroupCat.EquivalenceGroupAddGroup	461	0	-461 (-100.00%)
Mathlib.Analysis.Normed.Group.SemiNormedGroupCat	1094	0	-1094 (-100.00%)

---

Declarations diff

+ AddCommGrp.coyonedaObjIsoForget
+ AddCommGrp.forget_corepresentable
+ AddGrp.coyonedaObjIsoForget
+ AddGrp.forget_corepresentable
+ CommGrp
+ CommGrp.coyonedaObjIsoForget
+ CommGrp.forget_corepresentable
+ CommGrp.forget_reflects_isos
+ CommGrp.forget₂CommMonAdj
+ Grp
+ Grp.coyonedaObjIsoForget
+ Grp.forget_corepresentable
+ Grp.forget_reflects_isos
+ Grp.forget₂MonAdj
+ GrpWithZero
+ MonoidHom.comp_id_commGrp
+ MonoidHom.comp_id_grp
+ MonoidHom.id_commGrp_comp
+ MonoidHom.id_grp_comp
+ MulEquiv.toCommGrpIso
+ MulEquiv.toGrpIso
+ MulEquiv.toSemigrpIso
+ SemiNormedGrp
+ SemiNormedGrp₁
+ Semigrp
+ Semigrp.forgetReflectsIsos
+ Semigrp.forget₂_full
+ forget_commGrp_preserves_epi
+ forget_commGrp_preserves_mono
+ forget_grp_preserves_epi
+ forget_grp_preserves_mono
+ forget₂_addCommGrp_additive
+ forget₂_addCommGrp_essSurj
+ hasForgetToAddCommGrp
+ instance (G : CommGrp) : CommGroup <| (forget CommGrp).obj G
+ instance (G : Grp) : Group G.α
+ instance (G H : CommGrp) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
+ instance (G H : Grp) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
+ instance (M : SemiNormedGrp) : SeminormedAddCommGroup M
+ instance (M : SemiNormedGrp₁) : SeminormedAddCommGroup M
+ instance (P Q : AddCommGrp) : AddCommGroup (P ⟶ Q)
+ instance (X : Grp) : Group X := X.str
+ instance (X : GrpWithZero) : GroupWithZero X
+ instance (X : Semigrp) : Semigroup X := X.str
+ instance (X Y : SemiNormedGrp₁) : Zero (X ⟶ Y)
+ instance : (forget AddCommGrp.{u}).IsRightAdjoint
+ instance : (forget Grp.{u}).IsRightAdjoint
+ instance : (forget₂ (ModuleCat.{v} R) AddCommGrp.{v}).ReflectsIsomorphisms
+ instance : (forget₂ CommGrp.{u} Grp.{u}).ReflectsIsomorphisms
+ instance : Abelian AddCommGrp.{u}
+ instance : Coe CommGrp.{u} CommMonCat.{u} where coe := (forget₂ CommGrp CommMonCat).obj
+ instance : Coe CommGrp.{u} Grp.{u} where coe := (forget₂ CommGrp Grp).obj
+ instance : Coe Grp.{u} MonCat.{u} where coe := (forget₂ Grp MonCat).obj
+ instance : CoeSort CommGrp Type*
+ instance : CoeSort Grp Type*
+ instance : CoeSort GrpWithZero Type*
+ instance : CoeSort SemiNormedGrp Type*
+ instance : CoeSort SemiNormedGrp₁ Type*
+ instance : CoeSort Semigrp Type*
+ instance : ConcreteCategory SemiNormedGrp := by
+ instance : ConcreteCategory.{u} SemiNormedGrp₁
+ instance : HasBinaryBiproducts AddCommGrp
+ instance : HasCokernels SemiNormedGrp.{u}
+ instance : HasCokernels SemiNormedGrp₁.{u}
+ instance : HasColimitsOfSize.{0, 0} (AddCommGrp.{u}) := hasColimitsOfSize.{u, 0, 0}
+ instance : HasColimitsOfSize.{u, u} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{v}
+ instance : HasColimitsOfSize.{u, v} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
+ instance : HasColimitsOfSize.{v, u} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
+ instance : HasColimitsOfSize.{v, v} (AddCommGrpMax.{u, v}) := hasColimitsOfSize.{u}
+ instance : HasFiniteBiproducts AddCommGrp
+ instance : HasForget₂ SemiNormedGrp₁ SemiNormedGrp
+ instance : HasZeroObject CommGrp
+ instance : HasZeroObject Grp
+ instance : Inhabited (Action AddCommGrp G)
+ instance : Inhabited CommGrp
+ instance : Inhabited Grp
+ instance : Inhabited GrpWithZero
+ instance : Inhabited SemiNormedGrp
+ instance : Inhabited SemiNormedGrp₁
+ instance : Inhabited Semigrp
+ instance : LargeCategory.{u} GrpWithZero
+ instance : LargeCategory.{u} SemiNormedGrp₁
+ instance : Limits.HasEqualizers.{u, u + 1} SemiNormedGrp
+ instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGrp
+ instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGrp₁
+ instance : Preadditive AddCommGrp
+ instance : Preadditive SemiNormedGrp.{u}
+ instance : PreservesColimit F (forget₂ _ AddCommGrp)
+ instance : Small.{u} (Functor.sections ((F ⋙ forget₂ Grp MonCat) ⋙ forget MonCat))
+ instance _root_.AddCommGrp.forgetPreservesLimits :
+ instance {M N : GrpWithZero} : FunLike (M ⟶ N) M N
+ instance {M N : SemiNormedGrp} : Zero (M ⟶ N)
+ instance {V W : SemiNormedGrp.{u}} : NNNorm (V ⟶ W)
+ instance {V W : SemiNormedGrp.{u}} : Norm (V ⟶ W)
+ instance {V W : SemiNormedGrp.{u}} : Sub (V ⟶ W)
+ instance {X Y : CommGrp} : CoeFun (X ⟶ Y) fun _ => X → Y
+ instance {X Y : Grp} : CoeFun (X ⟶ Y) fun _ => X → Y
+ mulEquivIsoSemigrpIso
+ semigrpIsoToMulEquiv
+ toAddCommGrp
+ toAddGrp
+ toCommGrp
+ toGrp
+ wellPowered_addCommGrp
- AddCommGroupCat.coyonedaObjIsoForget
- AddCommGroupCat.forget_corepresentable
- AddGroupCat.coyonedaObjIsoForget
- AddGroupCat.forget_corepresentable
- CommGroupCat
- CommGroupCat.coyonedaObjIsoForget
- CommGroupCat.forget_corepresentable
- CommGroupCat.forget_reflects_isos
- CommGroupCat.forget₂CommMonAdj
- GroupCat
- GroupCat.coyonedaObjIsoForget
- GroupCat.forget_corepresentable
- GroupCat.forget_reflects_isos
- GroupCat.forget₂MonAdj
- GroupWithZeroCat
- MonoidHom.comp_id_commGroupCat
- MonoidHom.comp_id_groupCat
- MonoidHom.id_commGroupCat_comp
- MonoidHom.id_groupCat_comp
- MulEquiv.toCommGroupCatIso
- MulEquiv.toGroupCatIso
- MulEquiv.toSemigroupCatIso
- SemiNormedGroupCat
- SemiNormedGroupCat₁
- SemigroupCat
- SemigroupCat.forgetReflectsIsos
- SemigroupCat.forget₂_full
- forget_commGroupCat_preserves_epi
- forget_commGroupCat_preserves_mono
- forget_groupCat_preserves_epi
- forget_groupCat_preserves_mono
- forget₂_addCommGroupCat_additive
- forget₂_addCommGroupCat_essSurj
- hasForgetToAddCommGroupCat
- instance (G : CommGroupCat) : CommGroup <| (forget CommGroupCat).obj G
- instance (G : GroupCat) : Group G.α
- instance (G H : CommGroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
- instance (G H : GroupCat) : One (G ⟶ H) := (inferInstance : One (MonoidHom G H))
- instance (M : SemiNormedGroupCat) : SeminormedAddCommGroup M
- instance (M : SemiNormedGroupCat₁) : SeminormedAddCommGroup M
- instance (P Q : AddCommGroupCat) : AddCommGroup (P ⟶ Q)
- instance (X : GroupCat) : Group X := X.str
- instance (X : GroupWithZeroCat) : GroupWithZero X
- instance (X : SemigroupCat) : Semigroup X := X.str
- instance (X Y : SemiNormedGroupCat₁) : Zero (X ⟶ Y)
- instance : (forget AddCommGroupCat.{u}).IsRightAdjoint
- instance : (forget GroupCat.{u}).IsRightAdjoint
- instance : (forget₂ (ModuleCat.{v} R) AddCommGroupCat.{v}).ReflectsIsomorphisms
- instance : (forget₂ CommGroupCat.{u} GroupCat.{u}).ReflectsIsomorphisms
- instance : Abelian AddCommGroupCat.{u}
- instance : Coe CommGroupCat.{u} CommMonCat.{u} where coe := (forget₂ CommGroupCat CommMonCat).obj
- instance : Coe CommGroupCat.{u} GroupCat.{u} where coe := (forget₂ CommGroupCat GroupCat).obj
- instance : Coe GroupCat.{u} MonCat.{u} where coe := (forget₂ GroupCat MonCat).obj
- instance : CoeSort CommGroupCat Type*
- instance : CoeSort GroupCat Type*
- instance : CoeSort GroupWithZeroCat Type*
- instance : CoeSort SemiNormedGroupCat Type*
- instance : CoeSort SemiNormedGroupCat₁ Type*
- instance : CoeSort SemigroupCat Type*
- instance : ConcreteCategory SemiNormedGroupCat := by
- instance : ConcreteCategory.{u} SemiNormedGroupCat₁
- instance : HasBinaryBiproducts AddCommGroupCat
- instance : HasCokernels SemiNormedGroupCat.{u}
- instance : HasCokernels SemiNormedGroupCat₁.{u}
- instance : HasColimitsOfSize.{0, 0} (AddCommGroupCat.{u}) := hasColimitsOfSize.{u, 0, 0}
- instance : HasColimitsOfSize.{u, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{v}
- instance : HasColimitsOfSize.{u, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasColimitsOfSize.{v, u} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasColimitsOfSize.{v, v} (AddCommGroupCatMax.{u, v}) := hasColimitsOfSize.{u}
- instance : HasFiniteBiproducts AddCommGroupCat
- instance : HasForget₂ SemiNormedGroupCat₁ SemiNormedGroupCat
- instance : HasZeroObject CommGroupCat
- instance : HasZeroObject GroupCat
- instance : Inhabited (Action AddCommGroupCat G)
- instance : Inhabited CommGroupCat
- instance : Inhabited GroupCat
- instance : Inhabited GroupWithZeroCat
- instance : Inhabited SemiNormedGroupCat
- instance : Inhabited SemiNormedGroupCat₁
- instance : Inhabited SemigroupCat
- instance : LargeCategory.{u} GroupWithZeroCat
- instance : LargeCategory.{u} SemiNormedGroupCat₁
- instance : Limits.HasEqualizers.{u, u + 1} SemiNormedGroupCat
- instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGroupCat
- instance : Limits.HasZeroMorphisms.{u, u + 1} SemiNormedGroupCat₁
- instance : Preadditive AddCommGroupCat
- instance : Preadditive SemiNormedGroupCat.{u}
- instance : PreservesColimit F (forget₂ _ AddCommGroupCat)
- instance : Small.{u} (Functor.sections ((F ⋙ forget₂ GroupCat MonCat) ⋙ forget MonCat))
- instance _root_.AddCommGroupCat.forgetPreservesLimits :
- instance {M N : GroupWithZeroCat} : FunLike (M ⟶ N) M N
- instance {M N : SemiNormedGroupCat} : Zero (M ⟶ N)
- instance {V W : SemiNormedGroupCat.{u}} : NNNorm (V ⟶ W)
- instance {V W : SemiNormedGroupCat.{u}} : Norm (V ⟶ W)
- instance {V W : SemiNormedGroupCat.{u}} : Sub (V ⟶ W)
- instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y
- instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y
- mulEquivIsoSemigroupCatIso
- semigroupCatIsoToMulEquiv
- toAddCommGroupCat
- toAddGroupCat
- toCommGroupCat
- toGroupCat
- wellPowered_addCommGroupCat
-+-+ adj
-+-+ comp_def
-+-+ concreteCategory
-+-+ enoughInjectives
-+-+ forgetPreservesLimits
-+-+ free
-+-+ hasColimitsOfShape
-+-+ hasColimitsOfSize
-+-+ hasLimits
-+-+ hasLimitsOfShape
-+-+ hasLimitsOfSize
-+-+ one_apply
-+-+ uliftFunctor
-+-+-+ colimit
-+-+-+ ext
-+-+-+-+ instFunLike
-+-+-+--++ coe_of
-+-+--++ isZero_of_subsingleton
-+-+--++ ofUnique
-+-+--++-+-+ of
-+--++ forget_map
-+--++--++ coe_comp
-+--++--++ coe_id
--++ cokernelCocone
--++ cokernelLift
--++ hasZeroObject
--++ toAddMonoidHomClass
--++ zero_apply

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[semorrison]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style