Commit 2025-08-30 20:09 6398d185

View on Github →

feat: tensor product of group objects (#29134) ... and similarly for commutative monoid objects. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

deleted def CategoryTheory.Adjunction.mapGrp

deleted def CategoryTheory.Equivalence.mapGrp

deleted def CategoryTheory.Functor.FullyFaithful.grp_Class

deleted theorem CategoryTheory.Functor.comp_mapGrp_mul

deleted theorem CategoryTheory.Functor.comp_mapGrp_one

deleted def CategoryTheory.Functor.mapGrp

deleted def CategoryTheory.Functor.mapGrpCompIso

deleted def CategoryTheory.Functor.mapGrpIdIso

deleted def CategoryTheory.Functor.mapGrpNatIso

deleted def CategoryTheory.Functor.mapGrpNatTrans

deleted theorem CategoryTheory.Functor.mapGrp_id_mul

deleted theorem CategoryTheory.Functor.mapGrp_id_one

deleted def Grp_.forget

deleted def Grp_.forget₂Mon_

deleted theorem Grp_.forget₂Mon_comp_forget

deleted theorem Grp_.forget₂Mon_map_hom

deleted theorem Grp_.forget₂Mon_obj_mul

deleted theorem Grp_.forget₂Mon_obj_one

deleted def Grp_.fullyFaithfulForget₂Mon_

deleted def Grp_.mkIso'

modified theorem Grp_Class.ext

added def Grp_Class.tensorObj.CategoryTheory.Adjunction.mapGrp

added def Grp_Class.tensorObj.CategoryTheory.Equivalence.mapGrp

added def Grp_Class.tensorObj.CategoryTheory.Functor.FullyFaithful.grp_Class

added theorem Grp_Class.tensorObj.CategoryTheory.Functor.comp_mapGrp_mul

added theorem Grp_Class.tensorObj.CategoryTheory.Functor.comp_mapGrp_one

added def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrp

added def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpCompIso

added def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpIdIso

added def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpNatIso

added def Grp_Class.tensorObj.CategoryTheory.Functor.mapGrpNatTrans

added theorem Grp_Class.tensorObj.CategoryTheory.Functor.mapGrp_id_mul

added theorem Grp_Class.tensorObj.CategoryTheory.Functor.mapGrp_id_one

added def Grp_Class.tensorObj.Grp_.forget

added def Grp_Class.tensorObj.Grp_.forget₂Mon_

added theorem Grp_Class.tensorObj.Grp_.forget₂Mon_comp_forget

added theorem Grp_Class.tensorObj.Grp_.forget₂Mon_map_hom

added theorem Grp_Class.tensorObj.Grp_.forget₂Mon_obj_mul

added theorem Grp_Class.tensorObj.Grp_.forget₂Mon_obj_one

added def Grp_Class.tensorObj.Grp_.fullyFaithfulForget₂Mon_

added def Grp_Class.tensorObj.Grp_.mkIso'

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean