-
Notifications
You must be signed in to change notification settings - Fork 297
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(representation_theory/Rep): describe monoidal closed structure #18148
Conversation
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.
This PR seems to be quite some achievement! It seems to me that the long simp blocks are just a feature of category theory in Lean sometimes. I think that it would be helpful if you added either some comments or docstrings or both, because there's a lot going on here and it seems to be known to the experts how these things work, but not to me :-)
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by kbuzzard. |
bors merge |
…18148) The monoidal closed structure on `Rep k G` defines an internal hom of representations; we show this agrees with `representation.lin_hom`. Moreover, the maps defining the hom-set bijection come from the tensor-hom adjunction for $k$-modules.
Pull request successfully merged into master. Build succeeded: |
The monoidal closed structure on$k$ -modules.
Rep k G
defines an internal hom of representations; we show this agrees withrepresentation.lin_hom
. Moreover, the maps defining the hom-set bijection come from the tensor-hom adjunction for