Commit 2025-05-09 20:40 ef5db8b8

View on Github →

feat: an equivalence of categories lifts to an equivalence of their group objects (#23912) And same for (comm) monoid objects. From Toric

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/CommGrp_.lean

Modified Mathlib/CategoryTheory/Monoidal/CommMon_.lean

added def CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided

added def CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj

added theorem CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε

added theorem CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ

added def CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.counitIso

added def CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon

added def CategoryTheory.Equivalence.CommMon_.EquivLaxBraidedFunctorPUnit.unitIso

added def CategoryTheory.Equivalence.CommMon_.equivLaxBraidedFunctorPUnit

added def CategoryTheory.Equivalence.CommMon_.mk'

modified def CategoryTheory.Functor.mapCommMon

deleted def CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided

deleted def CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj

deleted theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε

deleted theorem CommMon_.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ

deleted def CommMon_.EquivLaxBraidedFunctorPUnit.counitIso

deleted def CommMon_.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon

deleted def CommMon_.EquivLaxBraidedFunctorPUnit.unitIso

deleted def CommMon_.equivLaxBraidedFunctorPUnit

deleted def CommMon_.mk'

Modified Mathlib/CategoryTheory/Monoidal/Functor.lean

Modified Mathlib/CategoryTheory/Monoidal/Grp_.lean

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

added theorem CategoryTheory.Equivalence.IsCommMon.mul_comm

added def CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.counitIso

added def CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon

added def CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal

added def CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj

added theorem CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε

added theorem CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ

added def CategoryTheory.Equivalence.Mon_.EquivLaxMonoidalFunctorPUnit.unitIso

added theorem CategoryTheory.Equivalence.Mon_.Mon_tensor_mul_assoc

added theorem CategoryTheory.Equivalence.Mon_.Mon_tensor_mul_one

added theorem CategoryTheory.Equivalence.Mon_.Mon_tensor_one_mul

added theorem CategoryTheory.Equivalence.Mon_.associator_hom_hom

added theorem CategoryTheory.Equivalence.Mon_.associator_inv_hom

added def CategoryTheory.Equivalence.Mon_.equivLaxMonoidalFunctorPUnit

added theorem CategoryTheory.Equivalence.Mon_.forget_δ

added theorem CategoryTheory.Equivalence.Mon_.forget_ε

added theorem CategoryTheory.Equivalence.Mon_.forget_η

added theorem CategoryTheory.Equivalence.Mon_.forget_μ

added theorem CategoryTheory.Equivalence.Mon_.leftUnitor_hom_hom

added theorem CategoryTheory.Equivalence.Mon_.leftUnitor_inv_hom

added theorem CategoryTheory.Equivalence.Mon_.mul_associator

added theorem CategoryTheory.Equivalence.Mon_.mul_braiding

added theorem CategoryTheory.Equivalence.Mon_.mul_leftUnitor

added theorem CategoryTheory.Equivalence.Mon_.mul_rightUnitor

added theorem CategoryTheory.Equivalence.Mon_.one_associator

added theorem CategoryTheory.Equivalence.Mon_.one_braiding

added theorem CategoryTheory.Equivalence.Mon_.one_leftUnitor

added theorem CategoryTheory.Equivalence.Mon_.one_rightUnitor

added theorem CategoryTheory.Equivalence.Mon_.rightUnitor_hom_hom

added theorem CategoryTheory.Equivalence.Mon_.rightUnitor_inv_hom

added theorem CategoryTheory.Equivalence.Mon_.tensorObj_mul

added theorem CategoryTheory.Equivalence.Mon_.tensorObj_one

added theorem CategoryTheory.Equivalence.Mon_.tensorUnit_X

added theorem CategoryTheory.Equivalence.Mon_.tensorUnit_mul

added theorem CategoryTheory.Equivalence.Mon_.tensorUnit_one

added theorem CategoryTheory.Equivalence.Mon_.tensor_mul

added theorem CategoryTheory.Equivalence.Mon_.tensor_one

added theorem CategoryTheory.Equivalence.Mon_.whiskerLeft_hom

added theorem CategoryTheory.Equivalence.Mon_.whiskerRight_hom

modified def CategoryTheory.Functor.mapMon

deleted theorem IsCommMon.mul_comm

deleted def Mon_.EquivLaxMonoidalFunctorPUnit.counitIso

deleted def Mon_.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon

deleted def Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal

deleted def Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj

deleted theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε

deleted theorem Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ

deleted def Mon_.EquivLaxMonoidalFunctorPUnit.unitIso

deleted theorem Mon_.Mon_tensor_mul_assoc

deleted theorem Mon_.Mon_tensor_mul_one

deleted theorem Mon_.Mon_tensor_one_mul

deleted theorem Mon_.associator_hom_hom

deleted theorem Mon_.associator_inv_hom

deleted def Mon_.equivLaxMonoidalFunctorPUnit

deleted theorem Mon_.forget_δ

deleted theorem Mon_.forget_ε

deleted theorem Mon_.forget_η

deleted theorem Mon_.forget_μ

deleted theorem Mon_.leftUnitor_hom_hom

deleted theorem Mon_.leftUnitor_inv_hom

deleted theorem Mon_.mul_associator

deleted theorem Mon_.mul_braiding

deleted theorem Mon_.mul_leftUnitor

deleted theorem Mon_.mul_rightUnitor

deleted theorem Mon_.one_associator

deleted theorem Mon_.one_braiding

deleted theorem Mon_.one_leftUnitor

deleted theorem Mon_.one_rightUnitor

deleted theorem Mon_.rightUnitor_hom_hom

deleted theorem Mon_.rightUnitor_inv_hom

deleted theorem Mon_.tensorObj_mul

deleted theorem Mon_.tensorObj_one

deleted theorem Mon_.tensorUnit_X

deleted theorem Mon_.tensorUnit_mul

deleted theorem Mon_.tensorUnit_one

deleted theorem Mon_.tensor_mul

deleted theorem Mon_.tensor_one

deleted theorem Mon_.whiskerLeft_hom

deleted theorem Mon_.whiskerRight_hom