Commit 2026-04-03 08:22 61bc83fb

View on Github →

feat(CategoryTheory/Monoidal): use to_additive for group objects (#37263)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

added structure CategoryTheory.AddGrp

modified def CategoryTheory.GrpObj.tensorObj.Adjunction.mapGrp

modified def CategoryTheory.GrpObj.tensorObj.Equivalence.mapGrp

modified theorem CategoryTheory.GrpObj.tensorObj.Functor.essImage_mapGrp

modified theorem CategoryTheory.GrpObj.tensorObj.Functor.obj.ι_def

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.associator_hom_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.associator_inv_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.braiding_hom_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.braiding_inv_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.fst_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.leftUnitor_hom_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.leftUnitor_inv_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.lift_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.rightUnitor_hom_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.rightUnitor_inv_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.snd_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorObj_mul

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorObj_one

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorUnit_X

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorUnit_mul

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.tensorUnit_one

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.whiskerLeft_hom_hom

modified theorem CategoryTheory.GrpObj.tensorObj.Grp.whiskerRight_hom_hom