The category of bimodule objects over a pair of monoid objects.

theorem id_tensor_π_preserves_coequalizer_inv_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Y) (h : CategoryTheory.MonoidalCategory.tensorObj Z Y ⟶ W) (wh : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g) h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv (CategoryTheory.Limits.coequalizer.desc h wh)) = h

theorem id_tensor_π_preserves_coequalizer_inv_colimMap_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X ⟶ Y) (g : X ⟶ Y) (f' : X' ⟶ Y') (g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategory.tensorObj Z X ⟶ X') (q : CategoryTheory.MonoidalCategory.tensorObj Z Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g) q = CategoryTheory.CategoryStruct.comp p g') (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.Limits.coequalizer.π f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorLeft Z) f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g) f' g' p q wf wg)) (CategoryTheory.Limits.coequalizer.desc h wh))) = CategoryTheory.CategoryStruct.comp q h

theorem π_tensor_id_preserves_coequalizer_inv_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W : C} {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : X ⟶ Y) (h : CategoryTheory.MonoidalCategory.tensorObj Y Z ⟶ W) (wh : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z)) h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv (CategoryTheory.Limits.coequalizer.desc h wh)) = h

theorem π_tensor_id_preserves_coequalizer_inv_colimMap_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X ⟶ Y) (g : X ⟶ Y) (f' : X' ⟶ Y') (g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategory.tensorObj X Z ⟶ X') (q : CategoryTheory.MonoidalCategory.tensorObj Y Z ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z)) q = CategoryTheory.CategoryStruct.comp p g') (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.coequalizer.π f g) (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z)) f' g' p q wf wg)) (CategoryTheory.Limits.coequalizer.desc h wh))) = CategoryTheory.CategoryStruct.comp q h

structure Bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) (B : Mon_ C) : Type (max u₁ v₁)

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

@[simp]

theorem Bimod.one_actLeft_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.one (CategoryTheory.CategoryStruct.id self.X)) (CategoryTheory.CategoryStruct.comp self.actLeft h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor self.X).hom h

@[simp]

theorem Bimod.right_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id self.X) B.mul) (CategoryTheory.CategoryStruct.comp self.actRight h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator self.X B.X B.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.actRight (CategoryTheory.CategoryStruct.id B.X)) (CategoryTheory.CategoryStruct.comp self.actRight h))

@[simp]

theorem Bimod.middle_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.actLeft (CategoryTheory.CategoryStruct.id B.X)) (CategoryTheory.CategoryStruct.comp self.actRight h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X self.X B.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) self.actRight) (CategoryTheory.CategoryStruct.comp self.actLeft h))

@[simp]

theorem Bimod.actRight_one_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id self.X) B.one) (CategoryTheory.CategoryStruct.comp self.actRight h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor self.X).hom h

@[simp]

theorem Bimod.left_assoc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (self : Bimod A B) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom A.mul (CategoryTheory.CategoryStruct.id self.X)) (CategoryTheory.CategoryStruct.comp self.actLeft h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) self.actLeft) (CategoryTheory.CategoryStruct.comp self.actLeft h))

theorem Bimod.Hom.ext {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {A B : Mon_ C} {M N : Bimod A B} (x y : Bimod.Hom M N), x.hom = y.hom → x = y

theorem Bimod.Hom.ext_iff {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {A B : Mon_ C} {M N : Bimod A B} (x y : Bimod.Hom M N), x = y ↔ x.hom = y.hom

structure Bimod.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (M : Bimod A B) (N : Bimod A B) : Type v₁

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

@[simp]

theorem Bimod.Hom.left_act_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} (self : Bimod.Hom M N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.actLeft (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A.X) self.hom) (CategoryTheory.CategoryStruct.comp N.actLeft h)

@[simp]

theorem Bimod.Hom.right_act_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} (self : Bimod.Hom M N) {Z : C} (h : N.X ⟶ Z) : CategoryTheory.CategoryStruct.comp M.actRight (CategoryTheory.CategoryStruct.comp self.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom self.hom (CategoryTheory.CategoryStruct.id B.X)) (CategoryTheory.CategoryStruct.comp N.actRight h)

@[simp]

theorem Bimod.id'_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (M : Bimod A B) : (Bimod.id' M).hom = CategoryTheory.CategoryStruct.id M.X

def Bimod.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (M : Bimod A B) : Bimod.Hom M M

The identity morphism on a bimodule object.

instance Bimod.homInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (M : Bimod A B) : Inhabited (Bimod.Hom M M)

@[simp]

theorem Bimod.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} {O : Bimod A B} (f : Bimod.Hom M N) (g : Bimod.Hom N O) : (Bimod.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def Bimod.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} {O : Bimod A B} (f : Bimod.Hom M N) (g : Bimod.Hom N O) : Bimod.Hom M O

Composition of bimodule object morphisms.

instance Bimod.instCategoryBimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} : CategoryTheory.Category.{v₁, max u₁ v₁} (Bimod A B)

theorem Bimod.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} (f : M ⟶ N) (g : M ⟶ N) (h : f.hom = g.hom) : f = g

@[simp]

theorem Bimod.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (M : Bimod A B) : (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X

@[simp]

theorem Bimod.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} {K : Bimod A B} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

@[simp]

theorem Bimod.isoOfIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Mon_ C} {Y : Mon_ C} {P : Bimod X Y} {Q : Bimod X Y} (f : P.X ≅ Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X.X) f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom (CategoryTheory.CategoryStruct.id Y.X)) Q.actRight) : (Bimod.isoOfIso f f_left_act_hom f_right_act_hom).inv.hom = f.inv

@[simp]

theorem Bimod.isoOfIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Mon_ C} {Y : Mon_ C} {P : Bimod X Y} {Q : Bimod X Y} (f : P.X ≅ Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X.X) f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom (CategoryTheory.CategoryStruct.id Y.X)) Q.actRight) : (Bimod.isoOfIso f f_left_act_hom f_right_act_hom).hom.hom = f.hom

def Bimod.isoOfIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Mon_ C} {Y : Mon_ C} {P : Bimod X Y} {Q : Bimod X Y} (f : P.X ≅ Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X.X) f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f.hom (CategoryTheory.CategoryStruct.id Y.X)) Q.actRight) : P ≅ Q

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.

@[simp]

theorem Bimod.regular_actLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Bimod.regular A).actLeft = A.mul

@[simp]

theorem Bimod.regular_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Bimod.regular A).X = A.X

@[simp]

theorem Bimod.regular_actRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : (Bimod.regular A).actRight = A.mul

def Bimod.regular {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Bimod A A

A monoid object as a bimodule over itself.

instance Bimod.instInhabitedBimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) : Inhabited (Bimod A A)

def Bimod.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) {B : Mon_ C} : CategoryTheory.Functor (Bimod A B) C

The forgetful functor from bimodule objects to the ambient category.

noncomputable def Bimod.TensorBimod.X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) : C

The underlying object of the tensor product of two bimodules.

noncomputable def Bimod.TensorBimod.actLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.MonoidalCategory.tensorObj R.X (Bimod.TensorBimod.X P Q) ⟶ Bimod.TensorBimod.X P Q

Left action for the tensor product of two bimodules.

theorem Bimod.TensorBimod.id_tensor_π_actLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id R.X) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategory.tensorHom P.actRight (CategoryTheory.CategoryStruct.id Q.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id P.X) Q.actLeft)))) (Bimod.TensorBimod.actLeft P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator R.X P.X Q.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom P.actLeft (CategoryTheory.CategoryStruct.id Q.X)) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategory.tensorHom P.actRight (CategoryTheory.CategoryStruct.id Q.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id P.X) Q.actLeft))))

theorem Bimod.TensorBimod.one_act_left' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom R.one (CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P Q))) (Bimod.TensorBimod.actLeft P Q) = (CategoryTheory.MonoidalCategory.leftUnitor (Bimod.TensorBimod.X P Q)).hom

theorem Bimod.TensorBimod.left_assoc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom R.mul (CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P Q))) (Bimod.TensorBimod.actLeft P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator R.X R.X (Bimod.TensorBimod.X P Q)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id R.X) (Bimod.TensorBimod.actLeft P Q)) (Bimod.TensorBimod.actLeft P Q))

noncomputable def Bimod.TensorBimod.actRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.MonoidalCategory.tensorObj (Bimod.TensorBimod.X P Q) T.X ⟶ Bimod.TensorBimod.X P Q

Right action for the tensor product of two bimodules.

theorem Bimod.TensorBimod.π_tensor_id_actRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategory.tensorHom P.actRight (CategoryTheory.CategoryStruct.id Q.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id P.X) Q.actLeft))) (CategoryTheory.CategoryStruct.id T.X)) (Bimod.TensorBimod.actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator P.X Q.X T.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id P.X) Q.actRight) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategory.tensorHom P.actRight (CategoryTheory.CategoryStruct.id Q.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id P.X) Q.actLeft))))

theorem Bimod.TensorBimod.actRight_one' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P Q)) T.one) (Bimod.TensorBimod.actRight P Q) = (CategoryTheory.MonoidalCategory.rightUnitor (Bimod.TensorBimod.X P Q)).hom

theorem Bimod.TensorBimod.right_assoc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P Q)) T.mul) (Bimod.TensorBimod.actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (Bimod.TensorBimod.X P Q) T.X T.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (Bimod.TensorBimod.actRight P Q) (CategoryTheory.CategoryStruct.id T.X)) (Bimod.TensorBimod.actRight P Q))

theorem Bimod.TensorBimod.middle_assoc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} (P : Bimod R S) (Q : Bimod S T) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (Bimod.TensorBimod.actLeft P Q) (CategoryTheory.CategoryStruct.id T.X)) (Bimod.TensorBimod.actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator R.X (Bimod.TensorBimod.X P Q) T.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id R.X) (Bimod.TensorBimod.actRight P Q)) (Bimod.TensorBimod.actLeft P Q))

@[simp]

theorem Bimod.tensorBimod_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) : (Bimod.tensorBimod M N).X = Bimod.TensorBimod.X M N

@[simp]

theorem Bimod.tensorBimod_actLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) : (Bimod.tensorBimod M N).actLeft = Bimod.TensorBimod.actLeft M N

@[simp]

theorem Bimod.tensorBimod_actRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) : (Bimod.tensorBimod M N).actRight = Bimod.TensorBimod.actRight M N

noncomputable def Bimod.tensorBimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) : Bimod X Z

Tensor product of two bimodule objects as a bimodule object.

@[simp]

theorem Bimod.tensorHom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M₁ : Bimod X Y} {M₂ : Bimod X Y} {N₁ : Bimod Y Z} {N₂ : Bimod Y Z} (f : M₁ ⟶ M₂) (g : N₁ ⟶ N₂) : (Bimod.tensorHom f g).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategory.tensorHom M₁.actRight (CategoryTheory.CategoryStruct.id N₁.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M₁.X Y.X N₁.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M₁.X) N₁.actLeft)) (CategoryTheory.MonoidalCategory.tensorHom M₂.actRight (CategoryTheory.CategoryStruct.id N₂.X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M₂.X Y.X N₂.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M₂.X) N₂.actLeft)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f.hom (CategoryTheory.CategoryStruct.id Y.X)) g.hom) (CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom M₁.actRight (CategoryTheory.CategoryStruct.id N₁.X)) (CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f.hom (CategoryTheory.CategoryStruct.id Y.X)) g.hom) (CategoryTheory.MonoidalCategory.tensorHom M₂.actRight (CategoryTheory.CategoryStruct.id N₂.X))) (_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M₁.X Y.X N₁.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M₁.X) N₁.actLeft)) (CategoryTheory.MonoidalCategory.tensorHom f.hom g.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f.hom (CategoryTheory.CategoryStruct.id Y.X)) g.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator M₂.X Y.X N₂.X).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M₂.X) N₂.actLeft))))

noncomputable def Bimod.tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M₁ : Bimod X Y} {M₂ : Bimod X Y} {N₁ : Bimod Y Z} {N₂ : Bimod Y Z} (f : M₁ ⟶ M₂) (g : N₁ ⟶ N₂) : Bimod.tensorBimod M₁ N₁ ⟶ Bimod.tensorBimod M₂ N₂

Tensor product of two morphisms of bimodule objects.

theorem Bimod.tensor_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M : Bimod X Y} {N : Bimod Y Z} : Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (Bimod.tensorBimod M N)

theorem Bimod.tensor_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M₁ : Bimod X Y} {M₂ : Bimod X Y} {M₃ : Bimod X Y} {N₁ : Bimod Y Z} {N₂ : Bimod Y Z} {N₃ : Bimod Y Z} (f₁ : M₁ ⟶ M₂) (f₂ : M₂ ⟶ M₃) (g₁ : N₁ ⟶ N₂) (g₂ : N₂ ⟶ N₃) : Bimod.tensorHom (CategoryTheory.CategoryStruct.comp f₁ f₂) (CategoryTheory.CategoryStruct.comp g₁ g₂) = CategoryTheory.CategoryStruct.comp (Bimod.tensorHom f₁ g₁) (Bimod.tensorHom f₂ g₂)

noncomputable def Bimod.AssociatorBimod.homAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.MonoidalCategory.tensorObj (Bimod.tensorBimod P Q).X L.X ⟶ (Bimod.tensorBimod P (Bimod.tensorBimod Q L)).X

An auxiliary morphism for the definition of the underlying morphism of the forward component of the associator isomorphism.

noncomputable def Bimod.AssociatorBimod.hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : (Bimod.tensorBimod (Bimod.tensorBimod P Q) L).X ⟶ (Bimod.tensorBimod P (Bimod.tensorBimod Q L)).X

The underlying morphism of the forward component of the associator isomorphism.

theorem Bimod.AssociatorBimod.hom_left_act_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (Bimod.tensorBimod (Bimod.tensorBimod P Q) L).actLeft (Bimod.AssociatorBimod.hom P Q L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id R.X) (Bimod.AssociatorBimod.hom P Q L)) (Bimod.tensorBimod P (Bimod.tensorBimod Q L)).actLeft

theorem Bimod.AssociatorBimod.hom_right_act_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (Bimod.tensorBimod (Bimod.tensorBimod P Q) L).actRight (Bimod.AssociatorBimod.hom P Q L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (Bimod.AssociatorBimod.hom P Q L) (CategoryTheory.CategoryStruct.id U.X)) (Bimod.tensorBimod P (Bimod.tensorBimod Q L)).actRight

noncomputable def Bimod.AssociatorBimod.invAux {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.MonoidalCategory.tensorObj P.X (Bimod.tensorBimod Q L).X ⟶ (Bimod.tensorBimod (Bimod.tensorBimod P Q) L).X

An auxiliary morphism for the definition of the underlying morphism of the inverse component of the associator isomorphism.

noncomputable def Bimod.AssociatorBimod.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : (Bimod.tensorBimod P (Bimod.tensorBimod Q L)).X ⟶ (Bimod.tensorBimod (Bimod.tensorBimod P Q) L).X

The underlying morphism of the inverse component of the associator isomorphism.

theorem Bimod.AssociatorBimod.hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (Bimod.AssociatorBimod.hom P Q L) (Bimod.AssociatorBimod.inv P Q L) = CategoryTheory.CategoryStruct.id (Bimod.tensorBimod (Bimod.tensorBimod P Q) L).X

theorem Bimod.AssociatorBimod.inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {R : Mon_ C} {S : Mon_ C} {T : Mon_ C} {U : Mon_ C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (Bimod.AssociatorBimod.inv P Q L) (Bimod.AssociatorBimod.hom P Q L) = CategoryTheory.CategoryStruct.id (Bimod.tensorBimod P (Bimod.tensorBimod Q L)).X

noncomputable def Bimod.LeftUnitorBimod.hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : Bimod.TensorBimod.X (Bimod.regular R) P ⟶ P.X

The underlying morphism of the forward component of the left unitor isomorphism.

noncomputable def Bimod.LeftUnitorBimod.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : P.X ⟶ Bimod.TensorBimod.X (Bimod.regular R) P

The underlying morphism of the inverse component of the left unitor isomorphism.

theorem Bimod.LeftUnitorBimod.hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.LeftUnitorBimod.hom P) (Bimod.LeftUnitorBimod.inv P) = CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X (Bimod.regular R) P)

theorem Bimod.LeftUnitorBimod.inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.LeftUnitorBimod.inv P) (Bimod.LeftUnitorBimod.hom P) = CategoryTheory.CategoryStruct.id P.X

theorem Bimod.LeftUnitorBimod.hom_left_act_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (Bimod.tensorBimod (Bimod.regular R) P).actLeft (Bimod.LeftUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id R.X) (Bimod.LeftUnitorBimod.hom P)) P.actLeft

theorem Bimod.LeftUnitorBimod.hom_right_act_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (Bimod.tensorBimod (Bimod.regular R) P).actRight (Bimod.LeftUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (Bimod.LeftUnitorBimod.hom P) (CategoryTheory.CategoryStruct.id S.X)) P.actRight

noncomputable def Bimod.RightUnitorBimod.hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : Bimod.TensorBimod.X P (Bimod.regular S) ⟶ P.X

The underlying morphism of the forward component of the right unitor isomorphism.

noncomputable def Bimod.RightUnitorBimod.inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : P.X ⟶ Bimod.TensorBimod.X P (Bimod.regular S)

The underlying morphism of the inverse component of the right unitor isomorphism.

theorem Bimod.RightUnitorBimod.hom_inv_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.RightUnitorBimod.hom P) (Bimod.RightUnitorBimod.inv P) = CategoryTheory.CategoryStruct.id (Bimod.TensorBimod.X P (Bimod.regular S))

theorem Bimod.RightUnitorBimod.inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (Bimod.RightUnitorBimod.inv P) (Bimod.RightUnitorBimod.hom P) = CategoryTheory.CategoryStruct.id P.X

theorem Bimod.RightUnitorBimod.hom_left_act_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (Bimod.tensorBimod P (Bimod.regular S)).actLeft (Bimod.RightUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id R.X) (Bimod.RightUnitorBimod.hom P)) P.actLeft

theorem Bimod.RightUnitorBimod.hom_right_act_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R : Mon_ C} {S : Mon_ C} (P : Bimod R S) [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.CategoryStruct.comp (Bimod.tensorBimod P (Bimod.regular S)).actRight (Bimod.RightUnitorBimod.hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (Bimod.RightUnitorBimod.hom P) (CategoryTheory.CategoryStruct.id S.X)) P.actRight

noncomputable def Bimod.associatorBimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W : Mon_ C} {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (L : Bimod W X) (M : Bimod X Y) (N : Bimod Y Z) : Bimod.tensorBimod (Bimod.tensorBimod L M) N ≅ Bimod.tensorBimod L (Bimod.tensorBimod M N)

The associator as a bimodule isomorphism.

noncomputable def Bimod.leftUnitorBimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} (M : Bimod X Y) : Bimod.tensorBimod (Bimod.regular X) M ≅ M

The left unitor as a bimodule isomorphism.

noncomputable def Bimod.rightUnitorBimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} (M : Bimod X Y) : Bimod.tensorBimod M (Bimod.regular Y) ≅ M

The right unitor as a bimodule isomorphism.

theorem Bimod.whisker_left_comp_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod X Y) {N : Bimod Y Z} {P : Bimod Y Z} {Q : Bimod Y Z} (f : N ⟶ P) (g : P ⟶ Q) : Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) f) (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) g)

theorem Bimod.id_whisker_left_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {M : Bimod X Y} {N : Bimod X Y} (f : M ⟶ N) : Bimod.tensorHom (CategoryTheory.CategoryStruct.id (Bimod.regular X)) f = CategoryTheory.CategoryStruct.comp (Bimod.leftUnitorBimod M).hom (CategoryTheory.CategoryStruct.comp f (Bimod.leftUnitorBimod N).inv)

theorem Bimod.comp_whisker_left_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W : Mon_ C} {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod W X) (N : Bimod X Y) {P : Bimod Y Z} {P' : Bimod Y Z} (f : P ⟶ P') : Bimod.tensorHom (CategoryTheory.CategoryStruct.id (Bimod.tensorBimod M N)) f = CategoryTheory.CategoryStruct.comp (Bimod.associatorBimod M N P).hom (CategoryTheory.CategoryStruct.comp (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) (Bimod.tensorHom (CategoryTheory.CategoryStruct.id N) f)) (Bimod.associatorBimod M N P').inv)

theorem Bimod.comp_whisker_right_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M : Bimod X Y} {N : Bimod X Y} {P : Bimod X Y} (f : M ⟶ N) (g : N ⟶ P) (Q : Bimod Y Z) : Bimod.tensorHom (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id Q) = CategoryTheory.CategoryStruct.comp (Bimod.tensorHom f (CategoryTheory.CategoryStruct.id Q)) (Bimod.tensorHom g (CategoryTheory.CategoryStruct.id Q))

theorem Bimod.whisker_right_id_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {M : Bimod X Y} {N : Bimod X Y} (f : M ⟶ N) : Bimod.tensorHom f (CategoryTheory.CategoryStruct.id (Bimod.regular Y)) = CategoryTheory.CategoryStruct.comp (Bimod.rightUnitorBimod M).hom (CategoryTheory.CategoryStruct.comp f (Bimod.rightUnitorBimod N).inv)

theorem Bimod.whisker_right_comp_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W : Mon_ C} {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M : Bimod W X} {M' : Bimod W X} (f : M ⟶ M') (N : Bimod X Y) (P : Bimod Y Z) : Bimod.tensorHom f (CategoryTheory.CategoryStruct.id (Bimod.tensorBimod N P)) = CategoryTheory.CategoryStruct.comp (Bimod.associatorBimod M N P).inv (CategoryTheory.CategoryStruct.comp (Bimod.tensorHom (Bimod.tensorHom f (CategoryTheory.CategoryStruct.id N)) (CategoryTheory.CategoryStruct.id P)) (Bimod.associatorBimod M' N P).hom)

theorem Bimod.whisker_assoc_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {W : Mon_ C} {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod W X) {N : Bimod X Y} {N' : Bimod X Y} (f : N ⟶ N') (P : Bimod Y Z) : Bimod.tensorHom (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) f) (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.comp (Bimod.associatorBimod M N P).hom (CategoryTheory.CategoryStruct.comp (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) (Bimod.tensorHom f (CategoryTheory.CategoryStruct.id P))) (Bimod.associatorBimod M N' P).inv)

theorem Bimod.whisker_exchange_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} {M : Bimod X Y} {N : Bimod X Y} {P : Bimod Y Z} {Q : Bimod Y Z} (f : M ⟶ N) (g : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) g) (Bimod.tensorHom f (CategoryTheory.CategoryStruct.id Q)) = CategoryTheory.CategoryStruct.comp (Bimod.tensorHom f (CategoryTheory.CategoryStruct.id P)) (Bimod.tensorHom (CategoryTheory.CategoryStruct.id N) g)

theorem Bimod.pentagon_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {V : Mon_ C} {W : Mon_ C} {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z) : CategoryTheory.CategoryStruct.comp (Bimod.tensorHom (Bimod.associatorBimod M N P).hom (CategoryTheory.CategoryStruct.id Q)) (CategoryTheory.CategoryStruct.comp (Bimod.associatorBimod M (Bimod.tensorBimod N P) Q).hom (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) (Bimod.associatorBimod N P Q).hom)) = CategoryTheory.CategoryStruct.comp (Bimod.associatorBimod (Bimod.tensorBimod M N) P Q).hom (Bimod.associatorBimod M N (Bimod.tensorBimod P Q)).hom

theorem Bimod.triangle_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod X Y) (N : Bimod Y Z) : CategoryTheory.CategoryStruct.comp (Bimod.associatorBimod M (Bimod.regular Y) N).hom (Bimod.tensorHom (CategoryTheory.CategoryStruct.id M) (Bimod.leftUnitorBimod N).hom) = Bimod.tensorHom (Bimod.rightUnitorBimod M).hom (CategoryTheory.CategoryStruct.id N)

noncomputable def Bimod.monBicategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] : CategoryTheory.Bicategory (Mon_ C)

The bicategory of algebras (monoids) and bimodules, all internal to some monoidal category.