The category of bimodule objects over a pair of monoid objects. #
- X : C
- actLeft : CategoryTheory.MonoidalCategory.tensorObj A.X s.X ⟶ s.X
- one_actLeft : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.one (CategoryTheory.CategoryStruct.id s.X)) s.actLeft = (CategoryTheory.MonoidalCategory.leftUnitor s.X).hom
- left_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.mul (CategoryTheory.CategoryStruct.id s.X)) s.actLeft = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X s.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) s.actLeft) s.actLeft)
- actRight : CategoryTheory.MonoidalCategory.tensorObj s.X B.X ⟶ s.X
- actRight_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id s.X) B.one) s.actRight = (CategoryTheory.MonoidalCategory.rightUnitor s.X).hom
- right_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id s.X) B.mul) s.actRight = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator s.X B.X B.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.actRight (CategoryTheory.CategoryStruct.id B.X)) s.actRight)
- middle_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.actLeft (CategoryTheory.CategoryStruct.id B.X)) s.actRight = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X s.X B.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) s.actRight) s.actLeft)
A bimodule object for a pair of monoid objects, all internal to some monoidal category.
Instances For
- hom : M.X ⟶ N.X
- left_act_hom : CategoryTheory.CategoryStruct.comp M.actLeft s.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) s.hom) N.actLeft
- right_act_hom : CategoryTheory.CategoryStruct.comp M.actRight s.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.hom (CategoryTheory.CategoryStruct.id B.X)) N.actRight
A morphism of bimodule objects.
Instances For
The identity morphism on a bimodule object.
Instances For
Composition of bimodule object morphisms.
Instances For
Construct an isomorphism of bimodules by giving an isomorphism between the underlying objects and checking compatibility with left and right actions only in the forward direction.
Instances For
A monoid object as a bimodule over itself.
Instances For
The forgetful functor from bimodule objects to the ambient category.
Instances For
The underlying object of the tensor product of two bimodules.
Instances For
Left action for the tensor product of two bimodules.
Instances For
Right action for the tensor product of two bimodules.
Instances For
Tensor product of two bimodule objects as a bimodule object.
Instances For
Tensor product of two morphisms of bimodule objects.
Instances For
An auxiliary morphism for the definition of the underlying morphism of the forward component of the associator isomorphism.
Instances For
The underlying morphism of the forward component of the associator isomorphism.
Instances For
An auxiliary morphism for the definition of the underlying morphism of the inverse component of the associator isomorphism.
Instances For
The underlying morphism of the inverse component of the associator isomorphism.
Instances For
The underlying morphism of the forward component of the left unitor isomorphism.
Instances For
The underlying morphism of the inverse component of the left unitor isomorphism.
Instances For
The underlying morphism of the forward component of the right unitor isomorphism.
Instances For
The underlying morphism of the inverse component of the right unitor isomorphism.
Instances For
The associator as a bimodule isomorphism.
Instances For
The left unitor as a bimodule isomorphism.
Instances For
The right unitor as a bimodule isomorphism.
Instances For
The bicategory of algebras (monoids) and bimodules, all internal to some monoidal category.