New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - Feat: Add Yang-Baxter equation and the opposite braided monoidal category #10415
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
7ef83b3
to
aecb5ec
Compare
aecb5ec
to
1fa39b2
Compare
@@ -123,6 +128,30 @@ theorem braiding_naturality {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : | |||
rw [tensorHom_def' f g, tensorHom_def g f] | |||
simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc] | |||
|
|||
theorem yang_baxter (X Y Z : C) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is there some reasons why you put associators at the both ends in the RHS? I think this is one possible choice, but we also have other choices.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sorry, I meant LHS, not RHS.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I chose this way of writing it because it becomes an equality of maps X ⊗ Y ⊗ Z ⟶ Z ⊗ Y ⊗ X
, both the domain and codomain being fully right associated. Also because it's what was easiest for the proof of associativity in mopBraidedFunctor
. There are other choices we could make but I don't see a reason to prefer another
bb83ed6
to
b7015e4
Compare
bors d+ |
✌️ Shamrock-Frost can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
bors merge |
…gory (#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.
Pull request successfully merged into master. Build succeeded: |
…gory (#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.
…gory (#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.
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.