Commit 2022-10-16 11:47 4698e35c

View 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.

Estimated changes

added def Bimod.comp
added theorem Bimod.comp_hom'
added def Bimod.forget
added structure Bimod.hom
added def'
added theorem Bimod.id_hom'
added def Bimod.iso_of_iso
added theorem Bimod.pentagon_Bimod
added def Bimod.regular
added theorem Bimod.tensor_comp
added def Bimod.tensor_hom
added theorem Bimod.tensor_id
added theorem Bimod.triangle_Bimod
added structure Bimod