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 X Y Z : C} (f g : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ W) (wh : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z g) h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 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 Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj Z X ⟶ X') (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 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.MonoidalCategoryStruct.whiskerLeft 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.MonoidalCategoryStruct.whiskerLeft Z f) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 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 X Y Z : C} (f g : X ⟶ Y) (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ W) (wh : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) 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 Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ X') (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g 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.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) 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.MonoidalCategoryStruct.whiskerRight f Z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight g 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 B : CategoryTheory.Mon C) : Type (max u₁ v₁)

A bimodule object for a pair of monoid objects, all internal to some monoidal category.

• X : C

  The underlying monoidal category

• actLeft : CategoryTheory.MonoidalCategoryStruct.tensorObj A.X self.X ⟶ self.X

  The left action of this bimodule object

• one_actLeft : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one self.X) self.actLeft = (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom
• left_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul self.X) self.actLeft = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.actLeft) self.actLeft)
• actRight : CategoryTheory.MonoidalCategoryStruct.tensorObj self.X B.X ⟶ self.X

  The right action of this bimodule object

• actRight_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.one) self.actRight = (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom
• right_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.mul) self.actRight = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X B.X B.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.actRight B.X) self.actRight)
• middle_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.actLeft B.X) self.actRight = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X self.X B.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.actRight) self.actLeft)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A morphism of bimodule objects.

• hom : M.X ⟶ N.X

  The morphism between M's monoidal category and N's monoidal category

• left_act_hom : CategoryTheory.CategoryStruct.comp M.actLeft self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X self.hom) N.actLeft
• right_act_hom : CategoryTheory.CategoryStruct.comp M.actRight self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.hom B.X) N.actRight

theorem Bimod.Hom.ext_iff {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {A B : CategoryTheory.Mon C} {M N : Bimod A B} {x y : M.Hom N} : x = y ↔ x.hom = y.hom

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

@[simp]

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

@[simp]

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

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

The identity morphism on a bimodule object.

@[simp]

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

@[implicit_reducible]

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

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

Composition of bimodule object morphisms.

@[simp]

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

@[implicit_reducible]

instance Bimod.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.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 B : CategoryTheory.Mon C} {M N : Bimod A B} (f g : M ⟶ N) (h : f.hom = g.hom) : f = g

theorem Bimod.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Mon C} {M N : Bimod A B} {f g : M ⟶ N} : f = g ↔ f.hom = g.hom

@[simp]

theorem Bimod.id_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.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 B : CategoryTheory.Mon C} {M N K : Bimod A B} (f : M ⟶ N) (g : N ⟶ K) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

def Bimod.isoOfIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Mon C} {P Q : Bimod X Y} (f : P.X ≅ Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom 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.isoOfIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Mon C} {P Q : Bimod X Y} (f : P.X ≅ Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.X f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) Q.actRight) : (isoOfIso f f_left_act_hom f_right_act_hom).hom.hom = f.hom

@[simp]

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

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

A monoid object as a bimodule over itself.

@[simp]

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

def Bimod.forget {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : CategoryTheory.Mon C) {B : CategoryTheory.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 S T : CategoryTheory.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 S T : CategoryTheory.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.MonoidalCategoryStruct.tensorObj R.X (X P Q) ⟶ X P Q

Left action for the tensor product of two bimodules.

theorem Bimod.TensorBimod.whiskerLeft_π_actLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerLeft R.X (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))) (actLeft P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X P.X Q.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actLeft Q.X) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 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 S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one (X P Q)) (actLeft P Q) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (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 S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul (X P Q)) (actLeft P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X R.X (X P Q)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (actLeft P Q)) (actLeft P Q))

noncomputable def Bimod.TensorBimod.actRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.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.MonoidalCategoryStruct.tensorObj (X P Q) T.X ⟶ 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 S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft))) T.X) (actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X Q.X T.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actRight) (CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X S.X Q.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft 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 S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerLeft (X P Q) CategoryTheory.MonObj.one) (actRight P Q) = (CategoryTheory.MonoidalCategoryStruct.rightUnitor (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 S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerLeft (X P Q) CategoryTheory.MonObj.mul) (actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (X P Q) T.X T.X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (actRight P Q) T.X) (actRight P Q))

theorem Bimod.TensorBimod.middle_assoc' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S T : CategoryTheory.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.MonoidalCategoryStruct.whiskerRight (actLeft P Q) T.X) (actRight P Q) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator R.X (X P Q) T.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (actRight P Q)) (actLeft P Q))

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 Y Z : CategoryTheory.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.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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : (M.tensorBimod N).X = TensorBimod.X 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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : (M.tensorBimod N).actRight = TensorBimod.actRight 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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : (M.tensorBimod N).actLeft = TensorBimod.actLeft M N

noncomputable def Bimod.whiskerLeft {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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂) : M.tensorBimod N₁ ⟶ M.tensorBimod N₂

Left whiskering for morphisms of bimodule objects.

@[simp]

theorem Bimod.whiskerLeft_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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N₁ N₂ : Bimod Y Z} (f : N₁ ⟶ N₂) : (M.whiskerLeft f).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₁.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₁.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₁.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight M.actRight N₂.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M.X Y.X N₂.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X N₂.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M.X Y.X) f.hom) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.X f.hom) ⋯ ⋯)

noncomputable def Bimod.whiskerRight {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 Y Z : CategoryTheory.Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z) : M₁.tensorBimod N ⟶ M₂.tensorBimod N

Right whiskering for morphisms of bimodule objects.

@[simp]

theorem Bimod.whiskerRight_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 Y Z : CategoryTheory.Mon C} {M₁ M₂ : Bimod X Y} (f : M₁ ⟶ M₂) (N : Bimod Y Z) : (whiskerRight f N).hom = CategoryTheory.Limits.colimMap (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₁.actRight N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₁.X Y.X N.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁.X N.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight M₂.actRight N.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₂.X Y.X N.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₂.X N.actLeft)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Y.X) N.X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom N.X) ⋯ ⋯)

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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.MonoidalCategoryStruct.tensorObj (P.tensorBimod Q).X L.X ⟶ (P.tensorBimod (Q.tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : ((P.tensorBimod Q).tensorBimod L).X ⟶ (P.tensorBimod (Q.tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp ((P.tensorBimod Q).tensorBimod L).actLeft (hom P Q L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (hom P Q L)) (P.tensorBimod (Q.tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp ((P.tensorBimod Q).tensorBimod L).actRight (hom P Q L) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hom P Q L) U.X) (P.tensorBimod (Q.tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.MonoidalCategoryStruct.tensorObj P.X (Q.tensorBimod L).X ⟶ ((P.tensorBimod Q).tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : (P.tensorBimod (Q.tensorBimod L)).X ⟶ ((P.tensorBimod Q).tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (hom P Q L) (inv P Q L) = CategoryTheory.CategoryStruct.id ((P.tensorBimod Q).tensorBimod 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 S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U) : CategoryTheory.CategoryStruct.comp (inv P Q L) (hom P Q L) = CategoryTheory.CategoryStruct.id (P.tensorBimod (Q.tensorBimod L)).X

noncomputable def Bimod.LeftUnitorBimod.hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : TensorBimod.X (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 S : CategoryTheory.Mon C} (P : Bimod R S) : P.X ⟶ TensorBimod.X (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 S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (hom P) (inv P) = CategoryTheory.CategoryStruct.id (TensorBimod.X (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 S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (inv P) (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 S : CategoryTheory.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 ((regular R).tensorBimod P).actLeft (hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (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 S : CategoryTheory.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 ((regular R).tensorBimod P).actRight (hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hom P) 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 S : CategoryTheory.Mon C} (P : Bimod R S) : TensorBimod.X P (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 S : CategoryTheory.Mon C} (P : Bimod R S) : P.X ⟶ TensorBimod.X P (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 S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (hom P) (inv P) = CategoryTheory.CategoryStruct.id (TensorBimod.X P (regular S))

theorem Bimod.RightUnitorBimod.inv_hom_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S) : CategoryTheory.CategoryStruct.comp (inv P) (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 S : CategoryTheory.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 (P.tensorBimod (regular S)).actLeft (hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (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 S : CategoryTheory.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 (P.tensorBimod (regular S)).actRight (hom P) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (hom P) 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 X Y Z : CategoryTheory.Mon C} (L : Bimod W X) (M : Bimod X Y) (N : Bimod Y Z) : (L.tensorBimod M).tensorBimod N ≅ L.tensorBimod (M.tensorBimod 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 Y : CategoryTheory.Mon C} (M : Bimod X Y) : (regular X).tensorBimod 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 Y : CategoryTheory.Mon C} (M : Bimod X Y) : M.tensorBimod (regular Y) ≅ M

The right unitor as a bimodule isomorphism.

theorem Bimod.whiskerLeft_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 Y Z : CategoryTheory.Mon C} {M : Bimod X Y} {N : Bimod Y Z} : M.whiskerLeft (CategoryTheory.CategoryStruct.id N) = CategoryTheory.CategoryStruct.id (M.tensorBimod N)

theorem Bimod.id_whiskerRight_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 Y Z : CategoryTheory.Mon C} {M : Bimod X Y} {N : Bimod Y Z} : whiskerRight (CategoryTheory.CategoryStruct.id M) N = CategoryTheory.CategoryStruct.id (M.tensorBimod N)

theorem Bimod.whiskerLeft_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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) {N P Q : Bimod Y Z} (f : N ⟶ P) (g : P ⟶ Q) : M.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (M.whiskerLeft f) (M.whiskerLeft g)

theorem Bimod.id_whiskerLeft_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 Y : CategoryTheory.Mon C} {M N : Bimod X Y} (f : M ⟶ N) : (regular X).whiskerLeft f = CategoryTheory.CategoryStruct.comp M.leftUnitorBimod.hom (CategoryTheory.CategoryStruct.comp f N.leftUnitorBimod.inv)

theorem Bimod.comp_whiskerLeft_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 X Y Z : CategoryTheory.Mon C} (M : Bimod W X) (N : Bimod X Y) {P P' : Bimod Y Z} (f : P ⟶ P') : (M.tensorBimod N).whiskerLeft f = CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).hom (CategoryTheory.CategoryStruct.comp (M.whiskerLeft (N.whiskerLeft f)) (M.associatorBimod N P').inv)

theorem Bimod.comp_whiskerRight_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 Y Z : CategoryTheory.Mon C} {M N P : Bimod X Y} (f : M ⟶ N) (g : N ⟶ P) (Q : Bimod Y Z) : whiskerRight (CategoryTheory.CategoryStruct.comp f g) Q = CategoryTheory.CategoryStruct.comp (whiskerRight f Q) (whiskerRight g Q)

theorem Bimod.whiskerRight_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 Y : CategoryTheory.Mon C} {M N : Bimod X Y} (f : M ⟶ N) : whiskerRight f (regular Y) = CategoryTheory.CategoryStruct.comp M.rightUnitorBimod.hom (CategoryTheory.CategoryStruct.comp f N.rightUnitorBimod.inv)

theorem Bimod.whiskerRight_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 X Y Z : CategoryTheory.Mon C} {M M' : Bimod W X} (f : M ⟶ M') (N : Bimod X Y) (P : Bimod Y Z) : whiskerRight f (N.tensorBimod P) = CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).inv (CategoryTheory.CategoryStruct.comp (whiskerRight (whiskerRight f N) P) (M'.associatorBimod 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 X Y Z : CategoryTheory.Mon C} (M : Bimod W X) {N N' : Bimod X Y} (f : N ⟶ N') (P : Bimod Y Z) : whiskerRight (M.whiskerLeft f) P = CategoryTheory.CategoryStruct.comp (M.associatorBimod N P).hom (CategoryTheory.CategoryStruct.comp (M.whiskerLeft (whiskerRight f P)) (M.associatorBimod 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 Y Z : CategoryTheory.Mon C} {M N : Bimod X Y} {P Q : Bimod Y Z} (f : M ⟶ N) (g : P ⟶ Q) : CategoryTheory.CategoryStruct.comp (M.whiskerLeft g) (whiskerRight f Q) = CategoryTheory.CategoryStruct.comp (whiskerRight f P) (N.whiskerLeft 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 W X Y Z : CategoryTheory.Mon C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z) : CategoryTheory.CategoryStruct.comp (whiskerRight (M.associatorBimod N P).hom Q) (CategoryTheory.CategoryStruct.comp (M.associatorBimod (N.tensorBimod P) Q).hom (M.whiskerLeft (N.associatorBimod P Q).hom)) = CategoryTheory.CategoryStruct.comp ((M.tensorBimod N).associatorBimod P Q).hom (M.associatorBimod N (P.tensorBimod 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 Y Z : CategoryTheory.Mon C} (M : Bimod X Y) (N : Bimod Y Z) : CategoryTheory.CategoryStruct.comp (M.associatorBimod (regular Y) N).hom (M.whiskerLeft N.leftUnitorBimod.hom) = whiskerRight M.rightUnitorBimod.hom N

@[implicit_reducible]

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 (CategoryTheory.Mon C)

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