Commit 2024-02-16 19:21 56349361

View on Github →

Feat: Add Yang-Baxter equation and the opposite braided monoidal category (#10415) This PR adds some basics about monoidal opposite categories and their relation to the original category, as well as the Yang-Baxter equation for braided monoidal categories. It should be easy to define an action of the braid group on an object of a braided monoidal category from this.

Estimated changes

Modified Mathlib/CategoryTheory/CommSq.lean

added theorem CategoryTheory.CommSq.vert_inv

Modified Mathlib/CategoryTheory/Monoidal/Braided.lean

added theorem CategoryTheory.BraidedCategory.braiding_inv_naturality

added theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_left

added theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_right

added theorem CategoryTheory.BraidedCategory.hexagon_forward_inv

added theorem CategoryTheory.BraidedCategory.hexagon_forward_iso

added theorem CategoryTheory.BraidedCategory.hexagon_reverse_inv

added theorem CategoryTheory.BraidedCategory.hexagon_reverse_iso

added theorem CategoryTheory.BraidedCategory.yang_baxter'

added theorem CategoryTheory.BraidedCategory.yang_baxter

added theorem CategoryTheory.BraidedCategory.yang_baxter_iso

added def CategoryTheory.MonoidalOpposite.mopBraidedFunctor

added theorem CategoryTheory.MonoidalOpposite.mop_braiding

added theorem CategoryTheory.MonoidalOpposite.mop_hom_braiding

added theorem CategoryTheory.MonoidalOpposite.mop_inv_braiding

added def CategoryTheory.MonoidalOpposite.unmopBraidedFunctor

added theorem CategoryTheory.MonoidalOpposite.unmop_braiding

added theorem CategoryTheory.MonoidalOpposite.unmop_hom_braiding

added theorem CategoryTheory.MonoidalOpposite.unmop_inv_braiding

added theorem CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding

added def CategoryTheory.SymmetricCategory.equivReverseBraiding

added theorem CategoryTheory.SymmetricCategory.reverseBraiding_eq

added theorem CategoryTheory.op_braiding

added theorem CategoryTheory.op_hom_braiding

added theorem CategoryTheory.op_inv_braiding

added def CategoryTheory.reverseBraiding

added theorem CategoryTheory.unop_braiding

added theorem CategoryTheory.unop_hom_braiding

added theorem CategoryTheory.unop_inv_braiding

Modified Mathlib/CategoryTheory/Monoidal/Category.lean

added theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_refl

added theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_symm

added theorem CategoryTheory.MonoidalCategory.whiskerLeftIso_trans

added theorem CategoryTheory.MonoidalCategory.whiskerRightIso_refl

added theorem CategoryTheory.MonoidalCategory.whiskerRightIso_symm

added theorem CategoryTheory.MonoidalCategory.whiskerRightIso_trans

Modified Mathlib/CategoryTheory/Monoidal/Opposite.lean

modified def CategoryTheory.Iso.mop

added def CategoryTheory.Iso.unmop

added def CategoryTheory.MonoidalOpposite.mopMopEquivalence

added theorem CategoryTheory.MonoidalOpposite.mop_inj_iff

added theorem CategoryTheory.MonoidalOpposite.mop_injective

deleted theorem CategoryTheory.MonoidalOpposite.op_inj_iff

deleted theorem CategoryTheory.MonoidalOpposite.op_injective

added def CategoryTheory.MonoidalOpposite.tensorIso

added def CategoryTheory.MonoidalOpposite.tensorLeftIso

added def CategoryTheory.MonoidalOpposite.tensorLeftMopIso

added def CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso

added def CategoryTheory.MonoidalOpposite.tensorRightIso

added def CategoryTheory.MonoidalOpposite.tensorRightMopIso

added def CategoryTheory.MonoidalOpposite.tensorRightUnmopIso

added def CategoryTheory.MonoidalOpposite.underlyingEquiv

added theorem CategoryTheory.MonoidalOpposite.unmop_inj_iff

added theorem CategoryTheory.MonoidalOpposite.unmop_injective

deleted theorem CategoryTheory.MonoidalOpposite.unop_inj_iff

deleted theorem CategoryTheory.MonoidalOpposite.unop_injective

added def CategoryTheory.mopFunctor

added theorem CategoryTheory.mop_associator

added theorem CategoryTheory.mop_hom_associator

added theorem CategoryTheory.mop_hom_leftUnitor

added theorem CategoryTheory.mop_hom_rightUnitor

deleted theorem CategoryTheory.mop_inj

added theorem CategoryTheory.mop_inv_associator

added theorem CategoryTheory.mop_inv_leftUnitor

added theorem CategoryTheory.mop_inv_rightUnitor

added theorem CategoryTheory.mop_leftUnitor

added theorem CategoryTheory.mop_rightUnitor

added theorem CategoryTheory.mop_tensorHom

modified theorem CategoryTheory.mop_tensorObj

modified theorem CategoryTheory.mop_tensorUnit

deleted theorem CategoryTheory.mop_unmop

added theorem CategoryTheory.mop_whiskerLeft

added theorem CategoryTheory.mop_whiskerRight

added theorem CategoryTheory.op_associator

added theorem CategoryTheory.op_hom_associator

added theorem CategoryTheory.op_hom_leftUnitor

added theorem CategoryTheory.op_hom_rightUnitor

added theorem CategoryTheory.op_inv_associator

added theorem CategoryTheory.op_inv_leftUnitor

added theorem CategoryTheory.op_inv_rightUnitor

added theorem CategoryTheory.op_leftUnitor

added theorem CategoryTheory.op_rightUnitor

added theorem CategoryTheory.op_tensorHom

modified theorem CategoryTheory.op_tensorObj

modified theorem CategoryTheory.op_tensorUnit

added theorem CategoryTheory.op_whiskerLeft

added theorem CategoryTheory.op_whiskerRight

added def CategoryTheory.unmopFunctor

added theorem CategoryTheory.unmop_associator

added theorem CategoryTheory.unmop_hom_associator

added theorem CategoryTheory.unmop_hom_leftUnitor

added theorem CategoryTheory.unmop_hom_rightUnitor

deleted theorem CategoryTheory.unmop_inj

added theorem CategoryTheory.unmop_inv_associator

added theorem CategoryTheory.unmop_inv_leftUnitor

added theorem CategoryTheory.unmop_inv_rightUnitor

added theorem CategoryTheory.unmop_leftUnitor

deleted theorem CategoryTheory.unmop_mop

added theorem CategoryTheory.unmop_rightUnitor

added theorem CategoryTheory.unmop_tensorHom

added theorem CategoryTheory.unmop_tensorObj

added theorem CategoryTheory.unmop_tensorUnit

added theorem CategoryTheory.unmop_whiskerLeft

added theorem CategoryTheory.unmop_whiskerRight

added theorem CategoryTheory.unop_associator

added theorem CategoryTheory.unop_hom_associator

added theorem CategoryTheory.unop_hom_leftUnitor

added theorem CategoryTheory.unop_hom_rightUnitor

added theorem CategoryTheory.unop_inv_associator

added theorem CategoryTheory.unop_inv_leftUnitor

added theorem CategoryTheory.unop_inv_rightUnitor

added theorem CategoryTheory.unop_leftUnitor

added theorem CategoryTheory.unop_rightUnitor

added theorem CategoryTheory.unop_tensorHom

added theorem CategoryTheory.unop_tensorObj

added theorem CategoryTheory.unop_tensorUnit

added theorem CategoryTheory.unop_whiskerLeft

added theorem CategoryTheory.unop_whiskerRight

added theorem Quiver.Hom.mop_inj

added theorem Quiver.Hom.mop_unmop

added theorem Quiver.Hom.unmop_inj

added theorem Quiver.Hom.unmop_mop

Modified docs/references.bib