Commit 2026-03-26 22:21 126d4c16

View on Github →

feat(CategoryTheory/Monoidal): use to_additive for monoid objects (#37167) We apply the to_additive attribute to the declarations in the file Mathlib/CategoryTheory/Monoidal/Mon_.lean: this defines additive monoid objects in a monoidal category. This shall be used in #36913 in order to define ring objects.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added structure CategoryTheory.AddMon.Hom

added structure CategoryTheory.AddMon

modified def CategoryTheory.Adjunction.mapMon

modified theorem CategoryTheory.Functor.essImage_mapMon

modified theorem CategoryTheory.Functor.obj.η_def

modified theorem CategoryTheory.Functor.obj.μ_def

modified theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one

modified theorem CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul

modified theorem CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul

modified theorem CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul

modified theorem CategoryTheory.Mon.associator_hom_hom

modified theorem CategoryTheory.Mon.associator_inv_hom

modified theorem CategoryTheory.Mon.braiding_hom_hom

modified theorem CategoryTheory.Mon.braiding_inv_hom

modified theorem CategoryTheory.Mon.forget_δ

modified theorem CategoryTheory.Mon.forget_ε

modified theorem CategoryTheory.Mon.forget_η

modified theorem CategoryTheory.Mon.forget_μ

modified theorem CategoryTheory.Mon.leftUnitor_hom_hom

modified theorem CategoryTheory.Mon.leftUnitor_inv_hom

modified theorem CategoryTheory.Mon.rightUnitor_hom_hom

modified theorem CategoryTheory.Mon.rightUnitor_inv_hom

modified theorem CategoryTheory.Mon.tensorObj_mul

modified theorem CategoryTheory.Mon.tensorUnit_X

modified theorem CategoryTheory.Mon.tensorUnit_mul

modified theorem CategoryTheory.Mon.tensorUnit_one

modified theorem CategoryTheory.Mon.tensor_one

Modified Mathlib/Tactic/Translate/ToAdditive.lean