[Merged by Bors] - feat: tensor products of bialgebras #11977
Conversation
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
…/mathlib4 into bialgtensorproduct
…mmunity/mathlib4 into bialgtensorproduct
kbuzzard
added
awaiting-author
101damnations
removed
the
awaiting-author
|
Thanks! maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by kbuzzard. |
eric-wieser
added
the
awaiting-author
101damnations
removed
the
awaiting-author
|
|
||
| theorem coalgebra_rid_eq_algebra_rid_apply (x) : | ||
| Coalgebra.TensorProduct.rid R A x = Algebra.TensorProduct.rid R R A x := | ||
| congr($((TensorProduct.AlgebraTensorModule.rid_eq_rid R A).symm) x) |
There was a problem hiding this comment.
The fact that this isn't rfl makes me think that one of the other two definitions is suboptimal? Did you already investigate how easy this is to fix? A TODO: make this defeq, which would involve [...] or similar is enough for this PR, as is "note: not possible to make defeq because [...`]
There was a problem hiding this comment.
It's not rfl because I didn't make Coalgebra.TensorProduct.rid heterobasic like the RHS is. I guess that's another drawback of my categorical approach, it's probably not the most amenable to adding heterobasic definitions. I've added a TODO comment.
|
✌️ 101damnations can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
We define the data in the monoidal structure on bialgebras - e.g. the bialgebra instance on a tensor product of bialgebras, and the tensor product of two `BialgHom`s as a `BialgHom`. This is done by combining the corresponding API for coalgebras and algebras. Co-authored-by: Amelia Livingston <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Monoidal category structure on bialgebras, using the definitions in `Mathlib.RingTheory.Bialgebra.TensorProduct` added in #11977 Co-authored-by: Amelia Livingston <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
We define the data in the monoidal structure on bialgebras - e.g. the bialgebra instance on a tensor product of bialgebras, and the tensor product of two
BialgHoms as aBialgHom. This is done by combining the corresponding API for coalgebras and algebras.See #11974 and #11975 for explanation of the corresponding API for coalgebras.