Commit 2022-10-16 11:47 4698e35cView on Github →
feat(category_theory/monoidal): define the bicategory of algebras and bimodules internal to some monoidal category (#14402)
We generalise the well-known construction of the 2-category of rings, bimodules, and intertwiners. Given a monoidal category
C that has coequalizers and in which left and right tensor products preserve colimits, we define a bicategory whose
- objects are monoids in C;
- 1-morphisms are bimodules;
- 2-morphisms are bimodule homomorphisms. The composition of 1-morphisms is given by the tensor product of bimodules over the middle monoid.