Commit 2025-10-03 14:29 f962fa30

View on Github →

chore(CategoryTheory/Monoidal/Mon): reorder (#30157) Move the BraidedCategory (Mon_ C) instance earlier in the file. Indeed I think it makes more sense like this (defining MonClass, then Mon, then Functor.mapMon). This is necessary for the material in #29136 to be placed in a relatively non-silly order within the file.

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Mon_.lean

deleted theorem CategoryTheory.Equivalence.Mon.associator_hom_hom

deleted theorem CategoryTheory.Equivalence.Mon.associator_inv_hom

deleted theorem CategoryTheory.Equivalence.Mon.braiding_hom_hom

deleted theorem CategoryTheory.Equivalence.Mon.braiding_inv_hom

deleted theorem CategoryTheory.Equivalence.Mon.forget_δ

deleted theorem CategoryTheory.Equivalence.Mon.forget_ε

deleted theorem CategoryTheory.Equivalence.Mon.forget_η

deleted theorem CategoryTheory.Equivalence.Mon.forget_μ

deleted theorem CategoryTheory.Equivalence.Mon.leftUnitor_hom_hom

deleted theorem CategoryTheory.Equivalence.Mon.leftUnitor_inv_hom

deleted theorem CategoryTheory.Equivalence.Mon.rightUnitor_hom_hom

deleted theorem CategoryTheory.Equivalence.Mon.rightUnitor_inv_hom

deleted theorem CategoryTheory.Equivalence.Mon.tensorObj_mul

deleted theorem CategoryTheory.Equivalence.Mon.tensorObj_one

deleted theorem CategoryTheory.Equivalence.Mon.tensorUnit_X

deleted theorem CategoryTheory.Equivalence.Mon.tensorUnit_mul

deleted theorem CategoryTheory.Equivalence.Mon.tensorUnit_one

deleted theorem CategoryTheory.Equivalence.Mon.tensor_mul

deleted theorem CategoryTheory.Equivalence.Mon.tensor_one

deleted theorem CategoryTheory.Equivalence.Mon.whiskerLeft_hom

deleted theorem CategoryTheory.Equivalence.Mon.whiskerRight_hom

deleted theorem CategoryTheory.Equivalence.MonObj.Mon_tensor_mul_assoc

deleted theorem CategoryTheory.Equivalence.MonObj.Mon_tensor_mul_one

deleted theorem CategoryTheory.Equivalence.MonObj.Mon_tensor_one_mul

deleted theorem CategoryTheory.Equivalence.MonObj.mul_associator

deleted theorem CategoryTheory.Equivalence.MonObj.mul_braiding

deleted theorem CategoryTheory.Equivalence.MonObj.mul_leftUnitor

deleted theorem CategoryTheory.Equivalence.MonObj.mul_rightUnitor

deleted theorem CategoryTheory.Equivalence.MonObj.one_associator

deleted theorem CategoryTheory.Equivalence.MonObj.one_braiding

deleted theorem CategoryTheory.Equivalence.MonObj.one_leftUnitor

deleted theorem CategoryTheory.Equivalence.MonObj.one_rightUnitor

added theorem Mon.associator_hom_hom

added theorem Mon.associator_inv_hom

added theorem Mon.braiding_hom_hom

added theorem Mon.braiding_inv_hom

added theorem Mon.forget_δ

added theorem Mon.forget_ε

added theorem Mon.forget_η

added theorem Mon.forget_μ

added theorem Mon.leftUnitor_hom_hom

added theorem Mon.leftUnitor_inv_hom

added theorem Mon.rightUnitor_hom_hom

added theorem Mon.rightUnitor_inv_hom

added theorem Mon.tensorObj_mul

added theorem Mon.tensorObj_one

added theorem Mon.tensorUnit_X

added theorem Mon.tensorUnit_mul

added theorem Mon.tensorUnit_one

added theorem Mon.tensor_mul

added theorem Mon.tensor_one

added theorem Mon.whiskerLeft_hom

added theorem Mon.whiskerRight_hom

added theorem MonObj.Mon_tensor_mul_assoc

added theorem MonObj.Mon_tensor_mul_one

added theorem MonObj.Mon_tensor_one_mul

added theorem MonObj.mul_associator

added theorem MonObj.mul_braiding

added theorem MonObj.mul_leftUnitor

added theorem MonObj.mul_rightUnitor

added theorem MonObj.one_associator

added theorem MonObj.one_braiding

added theorem MonObj.one_leftUnitor

added theorem MonObj.one_rightUnitor