Commit 2025-10-12 18:01 2ffecf4f

View on Github →

chore: rename Grp to GrpCat (#30191) This frees up the name for Grp_ to be renamed to Grp. We leave no deprecation since the name will be reused instantly. Zulip

Estimated changes

deleted def AddCommGrp.adj
deleted def AddCommGrp.free
deleted theorem AddCommGrp.free_map_coe
deleted theorem AddCommGrp.free_obj_coe
modified def CommMonCat.units
deleted def Grp.abelianize
deleted def Grp.abelianizeAdj
deleted def Grp.adj
deleted def Grp.forget₂MonAdj
deleted def Grp.free
added def GrpCat.adj
added def GrpCat.free
modified def MonCat.units
deleted structure AddCommGrp.Hom
deleted def AddCommGrp.asHom
deleted theorem AddCommGrp.int_hom_ext
deleted structure AddCommGrp
added structure AddCommGrpCat.Hom
added structure AddCommGrpCat
deleted structure AddGrp.Hom
deleted structure AddGrp
added structure AddGrpCat.Hom
added structure AddGrpCat
deleted structure CommGrp.Hom
deleted theorem CommGrp.coe_comp
deleted theorem CommGrp.coe_id
deleted theorem CommGrp.coe_of
deleted theorem CommGrp.comp_apply
deleted theorem CommGrp.ext
deleted theorem CommGrp.forget_map
deleted theorem CommGrp.hom_comp
deleted theorem CommGrp.hom_ext
deleted theorem CommGrp.hom_id
deleted theorem CommGrp.hom_inv_apply
deleted theorem CommGrp.hom_ofHom
deleted theorem CommGrp.id_apply
deleted theorem CommGrp.inv_hom_apply
deleted theorem CommGrp.ofHom_apply
deleted theorem CommGrp.ofHom_comp
deleted theorem CommGrp.ofHom_hom
deleted theorem CommGrp.ofHom_id
deleted theorem CommGrp.ofHom_injective
deleted theorem CommGrp.one_apply
deleted structure CommGrp
added structure CommGrpCat.Hom
added theorem CommGrpCat.coe_comp
added theorem CommGrpCat.coe_id
added theorem CommGrpCat.coe_of
added theorem CommGrpCat.comp_apply
added theorem CommGrpCat.ext
added theorem CommGrpCat.forget_map
added theorem CommGrpCat.hom_comp
added theorem CommGrpCat.hom_ext
added theorem CommGrpCat.hom_id
added theorem CommGrpCat.hom_ofHom
added theorem CommGrpCat.id_apply
added theorem CommGrpCat.ofHom_apply
added theorem CommGrpCat.ofHom_comp
added theorem CommGrpCat.ofHom_hom
added theorem CommGrpCat.ofHom_id
added theorem CommGrpCat.one_apply
added structure CommGrpCat
deleted def Grp.Hom.Simps.hom
deleted structure Grp.Hom
deleted theorem Grp.coe_comp
deleted theorem Grp.coe_id
deleted theorem Grp.coe_of
deleted theorem Grp.comp_apply
deleted theorem Grp.ext
deleted theorem Grp.forget_map
deleted theorem Grp.forget₂_map_ofHom
deleted theorem Grp.hom_comp
deleted theorem Grp.hom_ext
deleted theorem Grp.hom_id
deleted theorem Grp.hom_inv_apply
deleted theorem Grp.hom_ofHom
deleted theorem Grp.id_apply
deleted theorem Grp.inv_hom_apply
deleted theorem Grp.ofHom_apply
deleted theorem Grp.ofHom_comp
deleted theorem Grp.ofHom_hom
deleted theorem Grp.ofHom_id
deleted theorem Grp.ofHom_injective
deleted theorem Grp.one_apply
deleted def Grp.uliftFunctor
deleted structure Grp
added structure GrpCat.Hom
added theorem GrpCat.coe_comp
added theorem GrpCat.coe_id
added theorem GrpCat.coe_of
added theorem GrpCat.comp_apply
added theorem GrpCat.ext
added theorem GrpCat.forget_map
added theorem GrpCat.hom_comp
added theorem GrpCat.hom_ext
added theorem GrpCat.hom_id
added theorem GrpCat.hom_inv_apply
added theorem GrpCat.hom_ofHom
added theorem GrpCat.id_apply
added theorem GrpCat.inv_hom_apply
added theorem GrpCat.ofHom_apply
added theorem GrpCat.ofHom_comp
added theorem GrpCat.ofHom_hom
added theorem GrpCat.ofHom_id
added theorem GrpCat.ofHom_injective
added theorem GrpCat.one_apply
added structure GrpCat
modified theorem MonoidHom.comp_id_commGrp
modified theorem MonoidHom.comp_id_grp
modified theorem MonoidHom.id_commGrp_comp
modified theorem MonoidHom.id_grp_comp
modified def MulEquiv.toCommGrpIso
modified def MulEquiv.toGrpIso
modified def mulEquivIsoGroupIso
deleted theorem AddCommGrp.tensorObj_eq
deleted theorem AddGrp.tensorObj_eq
deleted theorem AddGrp.μ_forget_apply
added theorem AddGrpCat.tensorObj_eq
deleted theorem CommGrp.tensorObj_eq
deleted theorem CommGrp.μ_forget_apply
deleted theorem Grp.tensorObj_eq
deleted theorem Grp.μ_forget_apply
added theorem GrpCat.tensorObj_eq
added theorem GrpCat.μ_forget_apply
deleted theorem AddGrp.epi_iff_surjective
deleted theorem Grp.epi_iff_range_eq_top
deleted theorem Grp.epi_iff_surjective
deleted theorem Grp.ker_eq_bot_of_mono
deleted theorem Grp.mono_iff_injective
deleted theorem Grp.mono_iff_ker_eq_bot
deleted theorem Grp.surjective_of_epi
deleted def AddGrp.toGrp
added def AddGrpCat.toGrp
deleted def Grp.toAddGrp
added def GrpCat.toAddGrp
deleted theorem AddCommGrp.image.fac
deleted theorem AddCommGrp.image.lift_fac
deleted def AddCommGrp.image.ι
deleted def AddCommGrp.image
deleted def AddCommGrp.isFinite
deleted theorem AddCommGrp.hom_add
deleted theorem AddCommGrp.hom_add_apply
deleted theorem AddCommGrp.hom_neg
deleted theorem AddCommGrp.hom_nsmul
deleted theorem AddCommGrp.hom_sub
deleted theorem AddCommGrp.hom_zero
deleted theorem AddCommGrp.hom_zsmul
added theorem AddCommGrpCat.hom_add
added theorem AddCommGrpCat.hom_neg
added theorem AddCommGrpCat.hom_sub
added theorem AddCommGrpCat.hom_zero
deleted def CommGrp.coyoneda
modified def ModuleCat.mkOfSMul'
modified def ModuleCat.smul
modified def yonedaGrp
modified def yonedaGrpObj