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(category_theory/monoidal): Drinfeld center #7186
Conversation
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
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 shortened some of the proofs, I still think they're not the shortest path but they might be closer!
Your shortened proofs are still not "pure rewriting proofs", in the sense that that they rewrite by cancellation lemmas which operate on both sides at once. But I don't object. :-) |
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.
Thanks 🎉
bors merge
# Half braidings and the Drinfeld center of a monoidal category We define `center C` to be pairs `⟨X, b⟩`, where `X : C` and `b` is a half-braiding on `X`. We show that `center C` is braided monoidal, and provide the monoidal functor `center.forget` from `center C` back to `C`. ## Future work Verifying the various axioms here is done by tedious rewriting. Using the `slice` tactic may make the proofs marginally more readable. More exciting, however, would be to make possible one of the following options: 1. Integration with homotopy.io / globular to give "picture proofs". 2. The monoidal coherence theorem, so we can ignore associators (after which most of these proofs are trivial; I'm unsure if the monoidal coherence theorem is even usable in dependent type theory). 3. Automating these proofs using `rewrite_search` or some relative. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Half braidings and the Drinfeld center of a monoidal category
We define
center C
to be pairs⟨X, b⟩
, whereX : C
andb
is a half-braiding onX
.We show that
center C
is braided monoidal,and provide the monoidal functor
center.forget
fromcenter C
back toC
.Future work
Verifying the various axioms here is done by tedious rewriting.
Using the
slice
tactic may make the proofs marginally more readable.More exciting, however, would be to make possible one of the following options:
(after which most of these proofs are trivial;
I'm unsure if the monoidal coherence theorem is even usable in dependent type theory).
rewrite_search
or some relative.