Commit 2025-09-14 10:28 b667bcd9

View on Github →

chore: rename Grp_Class to GrpObj (#29623) This is a follow-up to #28406.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/CommGrp_.lean

added def CommGrpObj.ofRepresentableBy

deleted def CommGrp_Class.ofRepresentableBy

Modified Mathlib/CategoryTheory/Monoidal/Cartesian/Grp_.lean

added theorem GrpObj.comp_div

added theorem GrpObj.comp_inv

added theorem GrpObj.comp_zpow

added theorem GrpObj.div_comp

added theorem GrpObj.inv_comp

added theorem GrpObj.inv_eq_inv

added def GrpObj.ofRepresentableBy

added theorem GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy

added theorem GrpObj.zpow_comp

deleted theorem Grp_Class.comp_div

deleted theorem Grp_Class.comp_inv

deleted theorem Grp_Class.comp_zpow

deleted theorem Grp_Class.div_comp

deleted theorem Grp_Class.inv_comp

deleted theorem Grp_Class.inv_eq_inv

deleted def Grp_Class.ofRepresentableBy

deleted theorem Grp_Class.ofRepresentableBy_yonedaGrpObjRepresentableBy

deleted theorem Grp_Class.zpow_comp

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

modified def CommGrp_.mkIso'

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added theorem GrpObj.eq_lift_inv_left

added theorem GrpObj.eq_lift_inv_right

added theorem GrpObj.ext

added theorem GrpObj.inv_comp_inv

added theorem GrpObj.inv_hom

added theorem GrpObj.inv_inv

added theorem GrpObj.isPullback

added theorem GrpObj.lift_comp_inv_left

added theorem GrpObj.lift_comp_inv_right

added theorem GrpObj.lift_inv_comp_left

added theorem GrpObj.lift_inv_comp_right

added theorem GrpObj.lift_inv_left_eq

added theorem GrpObj.lift_inv_right_eq

added theorem GrpObj.lift_left_mul_ext

added def GrpObj.mulRight

added theorem GrpObj.mulRight_one

added theorem GrpObj.mul_inv

added theorem GrpObj.mul_inv_rev

added theorem GrpObj.tensorHom_inv_inv_mul

added def GrpObj.tensorObj.CategoryTheory.Adjunction.mapGrp

added def GrpObj.tensorObj.CategoryTheory.Equivalence.mapGrp

added theorem GrpObj.tensorObj.CategoryTheory.Functor.comp_mapGrp_mul

added theorem GrpObj.tensorObj.CategoryTheory.Functor.comp_mapGrp_one

added theorem GrpObj.tensorObj.CategoryTheory.Functor.essImage_mapGrp

added def GrpObj.tensorObj.CategoryTheory.Functor.mapGrp

added def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpCompIso

added def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpIdIso

added def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpNatIso

added def GrpObj.tensorObj.CategoryTheory.Functor.mapGrpNatTrans

added theorem GrpObj.tensorObj.CategoryTheory.Functor.mapGrp_id_mul

added theorem GrpObj.tensorObj.CategoryTheory.Functor.mapGrp_id_one

added def GrpObj.tensorObj.Grp_.forget

added def GrpObj.tensorObj.Grp_.forget₂Mon_

added theorem GrpObj.tensorObj.Grp_.forget₂Mon_comp_forget

added theorem GrpObj.tensorObj.Grp_.forget₂Mon_map_hom

added theorem GrpObj.tensorObj.Grp_.forget₂Mon_obj_mul

added theorem GrpObj.tensorObj.Grp_.forget₂Mon_obj_one

added def GrpObj.tensorObj.Grp_.fullyFaithfulForget₂Mon_

added def GrpObj.tensorObj.Grp_.mkIso'

added theorem GrpObj.toMonObj_injective

deleted theorem Grp_Class.eq_lift_inv_left

deleted theorem Grp_Class.eq_lift_inv_right

deleted theorem Grp_Class.ext

deleted theorem Grp_Class.inv_comp_inv

deleted theorem Grp_Class.inv_hom

deleted theorem Grp_Class.inv_inv

deleted theorem Grp_Class.isPullback

deleted theorem Grp_Class.lift_comp_inv_left

deleted theorem Grp_Class.lift_comp_inv_right

deleted theorem Grp_Class.lift_inv_comp_left

deleted theorem Grp_Class.lift_inv_comp_right

deleted theorem Grp_Class.lift_inv_left_eq

deleted theorem Grp_Class.lift_inv_right_eq

deleted theorem Grp_Class.lift_left_mul_ext

deleted def Grp_Class.mulRight

deleted theorem Grp_Class.mulRight_one

deleted theorem Grp_Class.mul_inv

deleted theorem Grp_Class.mul_inv_rev

deleted theorem Grp_Class.tensorHom_inv_inv_mul

deleted def Grp_Class.tensorObj.CategoryTheory.Adjunction.mapGrp

deleted def Grp_Class.tensorObj.CategoryTheory.Equivalence.mapGrp

deleted theorem Grp_Class.tensorObj.CategoryTheory.Functor.comp_mapGrp_mul

deleted theorem Grp_Class.tensorObj.CategoryTheory.Functor.comp_mapGrp_one

deleted theorem Grp_Class.tensorObj.CategoryTheory.Functor.essImage_mapGrp

deleted def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrp

deleted def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpCompIso

deleted def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpIdIso

deleted def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpNatIso

deleted def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpNatTrans

deleted theorem Grp_Class.tensorObj.CategoryTheory.Functor.mapGrp_id_mul

deleted theorem Grp_Class.tensorObj.CategoryTheory.Functor.mapGrp_id_one

deleted def Grp_Class.tensorObj.Grp_.forget

deleted def Grp_Class.tensorObj.Grp_.forget₂Mon_

deleted theorem Grp_Class.tensorObj.Grp_.forget₂Mon_comp_forget

deleted theorem Grp_Class.tensorObj.Grp_.forget₂Mon_map_hom

deleted theorem Grp_Class.tensorObj.Grp_.forget₂Mon_obj_mul

deleted theorem Grp_Class.tensorObj.Grp_.forget₂Mon_obj_one

deleted def Grp_Class.tensorObj.Grp_.fullyFaithfulForget₂Mon_

deleted def Grp_Class.tensorObj.Grp_.mkIso'

deleted theorem Grp_Class.toMonObj_injective

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Internal/Types/Grp_.lean

Modified Mathlib/CategoryTheory/Preadditive/CommGrp_.lean