The category of bimodule objects over a pair of monoid objects. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
id_tensor_π_preserves_coequalizer_inv_desc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
{W X Y Z : C}
(f g : X ⟶ Y)
(h : Z ⊗ Y ⟶ W)
(wh : (𝟙 Z ⊗ f) ≫ h = (𝟙 Z ⊗ g) ≫ h) :
theorem
id_tensor_π_preserves_coequalizer_inv_colim_map_desc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
{X Y Z X' Y' Z' : C}
(f g : X ⟶ Y)
(f' g' : X' ⟶ Y')
(p : Z ⊗ X ⟶ X')
(q : Z ⊗ Y ⟶ Y')
(wf : (𝟙 Z ⊗ f) ≫ q = p ≫ f')
(wg : (𝟙 Z ⊗ g) ≫ q = p ≫ g')
(h : Y' ⟶ Z')
(wh : f' ≫ h = g' ≫ h) :
(𝟙 Z ⊗ category_theory.limits.coequalizer.π f g) ≫ (category_theory.limits.preserves_coequalizer.iso (category_theory.monoidal_category.tensor_left Z) f g).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (𝟙 Z ⊗ f) (𝟙 Z ⊗ g) f' g' p q wf wg) ≫ category_theory.limits.coequalizer.desc h wh = q ≫ h
theorem
π_tensor_id_preserves_coequalizer_inv_desc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{W X Y Z : C}
(f g : X ⟶ Y)
(h : Y ⊗ Z ⟶ W)
(wh : (f ⊗ 𝟙 Z) ≫ h = (g ⊗ 𝟙 Z) ≫ h) :
theorem
π_tensor_id_preserves_coequalizer_inv_colim_map_desc
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z X' Y' Z' : C}
(f g : X ⟶ Y)
(f' g' : X' ⟶ Y')
(p : X ⊗ Z ⟶ X')
(q : Y ⊗ Z ⟶ Y')
(wf : (f ⊗ 𝟙 Z) ≫ q = p ≫ f')
(wg : (g ⊗ 𝟙 Z) ≫ q = p ≫ g')
(h : Y' ⟶ Z')
(wh : f' ≫ h = g' ≫ h) :
(category_theory.limits.coequalizer.π f g ⊗ 𝟙 Z) ≫ (category_theory.limits.preserves_coequalizer.iso (category_theory.monoidal_category.tensor_right Z) f g).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (f ⊗ 𝟙 Z) (g ⊗ 𝟙 Z) f' g' p q wf wg) ≫ category_theory.limits.coequalizer.desc h wh = q ≫ h
structure
Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A B : Mon_ C) :
Type (max u₁ v₁)
- X : C
- act_left : A.X ⊗ self.X ⟶ self.X
- one_act_left' : (A.one ⊗ 𝟙 self.X) ≫ self.act_left = (λ_ self.X).hom . "obviously"
- left_assoc' : (A.mul ⊗ 𝟙 self.X) ≫ self.act_left = (α_ A.X A.X self.X).hom ≫ (𝟙 A.X ⊗ self.act_left) ≫ self.act_left . "obviously"
- act_right : self.X ⊗ B.X ⟶ self.X
- act_right_one' : (𝟙 self.X ⊗ B.one) ≫ self.act_right = (ρ_ self.X).hom . "obviously"
- right_assoc' : (𝟙 self.X ⊗ B.mul) ≫ self.act_right = (α_ self.X B.X B.X).inv ≫ (self.act_right ⊗ 𝟙 B.X) ≫ self.act_right . "obviously"
- middle_assoc' : (self.act_left ⊗ 𝟙 B.X) ≫ self.act_right = (α_ A.X self.X B.X).hom ≫ (𝟙 A.X ⊗ self.act_right) ≫ self.act_left . "obviously"
A bimodule object for a pair of monoid objects, all internal to some monoidal category.
Instances for Bimod
- Bimod.has_sizeof_inst
- Bimod.category_theory.category
- Bimod.inhabited
@[simp]
@[simp]
@[simp]
theorem
Bimod.hom.ext_iff
{C : Type u₁}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.monoidal_category C}
{A B : Mon_ C}
{M N : Bimod A B}
(x y : M.hom N) :
@[ext]
structure
Bimod.hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(M N : Bimod A B) :
Type v₁
- hom : M.X ⟶ N.X
- left_act_hom' : M.act_left ≫ self.hom = (𝟙 A.X ⊗ self.hom) ≫ N.act_left . "obviously"
- right_act_hom' : M.act_right ≫ self.hom = (self.hom ⊗ 𝟙 B.X) ≫ N.act_right . "obviously"
A morphism of bimodule objects.
Instances for Bimod.hom
- Bimod.hom.has_sizeof_inst
- Bimod.hom_inhabited
theorem
Bimod.hom.ext
{C : Type u₁}
{_inst_1 : category_theory.category C}
{_inst_2 : category_theory.monoidal_category C}
{A B : Mon_ C}
{M N : Bimod A B}
(x y : M.hom N)
(h : x.hom = y.hom) :
x = y
def
Bimod.id'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(M : Bimod A B) :
M.hom M
The identity morphism on a bimodule object.
Equations
- M.id' = {hom := 𝟙 M.X, left_act_hom' := _, right_act_hom' := _}
@[simp]
theorem
Bimod.id'_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(M : Bimod A B) :
@[protected, instance]
def
Bimod.hom_inhabited
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(M : Bimod A B) :
Equations
- M.hom_inhabited = {default := M.id'}
@[simp]
theorem
Bimod.comp_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
{M N O : Bimod A B}
(f : M.hom N)
(g : N.hom O) :
def
Bimod.comp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
{M N O : Bimod A B}
(f : M.hom N)
(g : N.hom O) :
M.hom O
Composition of bimodule object morphisms.
Equations
- Bimod.comp f g = {hom := f.hom ≫ g.hom, left_act_hom' := _, right_act_hom' := _}
@[protected, instance]
def
Bimod.category_theory.category
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C} :
@[simp]
theorem
Bimod.id_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
(M : Bimod A B) :
@[simp]
theorem
Bimod.comp_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : Mon_ C}
{M N K : Bimod A B}
(f : M ⟶ N)
(g : N ⟶ K) :
def
Bimod.iso_of_iso
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : Mon_ C}
{P Q : Bimod X Y}
(f : P.X ≅ Q.X)
(f_left_act_hom : P.act_left ≫ f.hom = (𝟙 X.X ⊗ f.hom) ≫ Q.act_left)
(f_right_act_hom : P.act_right ≫ f.hom = (f.hom ⊗ 𝟙 Y.X) ≫ Q.act_right) :
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.
Equations
- Bimod.iso_of_iso f f_left_act_hom f_right_act_hom = {hom := {hom := f.hom, left_act_hom' := f_left_act_hom, right_act_hom' := f_right_act_hom}, inv := {hom := f.inv, left_act_hom' := _, right_act_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
Bimod.iso_of_iso_inv_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : Mon_ C}
{P Q : Bimod X Y}
(f : P.X ≅ Q.X)
(f_left_act_hom : P.act_left ≫ f.hom = (𝟙 X.X ⊗ f.hom) ≫ Q.act_left)
(f_right_act_hom : P.act_right ≫ f.hom = (f.hom ⊗ 𝟙 Y.X) ≫ Q.act_right) :
(Bimod.iso_of_iso f f_left_act_hom f_right_act_hom).inv.hom = f.inv
@[simp]
theorem
Bimod.iso_of_iso_hom_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : Mon_ C}
{P Q : Bimod X Y}
(f : P.X ≅ Q.X)
(f_left_act_hom : P.act_left ≫ f.hom = (𝟙 X.X ⊗ f.hom) ≫ Q.act_left)
(f_right_act_hom : P.act_right ≫ f.hom = (f.hom ⊗ 𝟙 Y.X) ≫ Q.act_right) :
(Bimod.iso_of_iso f f_left_act_hom f_right_act_hom).hom.hom = f.hom
@[simp]
theorem
Bimod.regular_X
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
(Bimod.regular A).X = A.X
def
Bimod.regular
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
Bimod A A
A monoid object as a bimodule over itself.
Equations
- Bimod.regular A = {X := A.X, act_left := A.mul, one_act_left' := _, left_assoc' := _, act_right := A.mul, act_right_one' := _, right_assoc' := _, middle_assoc' := _}
@[simp]
theorem
Bimod.regular_act_right
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
(Bimod.regular A).act_right = A.mul
@[simp]
theorem
Bimod.regular_act_left
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
(Bimod.regular A).act_left = A.mul
@[protected, instance]
def
Bimod.inhabited
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C) :
Equations
- Bimod.inhabited A = {default := Bimod.regular A}
def
Bimod.forget
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : Mon_ C)
{B : Mon_ C} :
The forgetful functor from bimodule objects to the ambient category.
noncomputable
def
Bimod.tensor_Bimod.X
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S 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.tensor_Bimod.act_left
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)] :
R.X ⊗ Bimod.tensor_Bimod.X P Q ⟶ Bimod.tensor_Bimod.X P Q
Left action for the tensor product of two bimodules.
Equations
- Bimod.tensor_Bimod.act_left P Q = (category_theory.limits.preserves_coequalizer.iso (category_theory.monoidal_category.tensor_left R.X) (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom ((category_theory.monoidal_category.tensor_left R.X).map (P.act_right ⊗ 𝟙 Q.X)) ((category_theory.monoidal_category.tensor_left R.X).map ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))) (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left)) ((𝟙 R.X ⊗ (α_ P.X S.X Q.X).hom) ≫ (α_ R.X P.X (S.X ⊗ Q.X)).inv ≫ (P.act_left ⊗ 𝟙 S.X ⊗ 𝟙 Q.X) ≫ (α_ P.X S.X Q.X).inv) ((α_ R.X P.X Q.X).inv ≫ (P.act_left ⊗ 𝟙 Q.X)) _ _)
theorem
Bimod.tensor_Bimod.id_tensor_π_act_left
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)] :
(𝟙 R.X ⊗ category_theory.limits.coequalizer.π (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))) ≫ Bimod.tensor_Bimod.act_left P Q = (α_ R.X P.X Q.X).inv ≫ (P.act_left ⊗ 𝟙 Q.X) ≫ category_theory.limits.coequalizer.π (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))
theorem
Bimod.tensor_Bimod.one_act_left'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)] :
(R.one ⊗ 𝟙 (Bimod.tensor_Bimod.X P Q)) ≫ Bimod.tensor_Bimod.act_left P Q = (λ_ (Bimod.tensor_Bimod.X P Q)).hom
theorem
Bimod.tensor_Bimod.left_assoc'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)] :
(R.mul ⊗ 𝟙 (Bimod.tensor_Bimod.X P Q)) ≫ Bimod.tensor_Bimod.act_left P Q = (α_ R.X R.X (Bimod.tensor_Bimod.X P Q)).hom ≫ (𝟙 R.X ⊗ Bimod.tensor_Bimod.act_left P Q) ≫ Bimod.tensor_Bimod.act_left P Q
noncomputable
def
Bimod.tensor_Bimod.act_right
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
Bimod.tensor_Bimod.X P Q ⊗ T.X ⟶ Bimod.tensor_Bimod.X P Q
Right action for the tensor product of two bimodules.
Equations
- Bimod.tensor_Bimod.act_right P Q = (category_theory.limits.preserves_coequalizer.iso (category_theory.monoidal_category.tensor_right T.X) (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))).inv ≫ category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom ((category_theory.monoidal_category.tensor_right T.X).map (P.act_right ⊗ 𝟙 Q.X)) ((category_theory.monoidal_category.tensor_right T.X).map ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))) (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left)) ((α_ (P.X ⊗ S.X) Q.X T.X).hom ≫ (α_ P.X S.X (Q.X ⊗ T.X)).hom ≫ (𝟙 P.X ⊗ 𝟙 S.X ⊗ Q.act_right) ≫ (α_ P.X S.X Q.X).inv) ((α_ P.X Q.X T.X).hom ≫ (𝟙 P.X ⊗ Q.act_right)) _ _)
theorem
Bimod.tensor_Bimod.π_tensor_id_act_right
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
(category_theory.limits.coequalizer.π (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left)) ⊗ 𝟙 T.X) ≫ Bimod.tensor_Bimod.act_right P Q = (α_ P.X Q.X T.X).hom ≫ (𝟙 P.X ⊗ Q.act_right) ≫ category_theory.limits.coequalizer.π (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))
theorem
Bimod.tensor_Bimod.act_right_one'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
(𝟙 (Bimod.tensor_Bimod.X P Q) ⊗ T.one) ≫ Bimod.tensor_Bimod.act_right P Q = (ρ_ (Bimod.tensor_Bimod.X P Q)).hom
theorem
Bimod.tensor_Bimod.right_assoc'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
(𝟙 (Bimod.tensor_Bimod.X P Q) ⊗ T.mul) ≫ Bimod.tensor_Bimod.act_right P Q = (α_ (Bimod.tensor_Bimod.X P Q) T.X T.X).inv ≫ (Bimod.tensor_Bimod.act_right P Q ⊗ 𝟙 T.X) ≫ Bimod.tensor_Bimod.act_right P Q
theorem
Bimod.tensor_Bimod.middle_assoc'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S T : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
(Bimod.tensor_Bimod.act_left P Q ⊗ 𝟙 T.X) ≫ Bimod.tensor_Bimod.act_right P Q = (α_ R.X (Bimod.tensor_Bimod.X P Q) T.X).hom ≫ (𝟙 R.X ⊗ Bimod.tensor_Bimod.act_right P Q) ≫ Bimod.tensor_Bimod.act_left P Q
noncomputable
def
Bimod.tensor_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
(M : Bimod X Y)
(N : Bimod Y Z) :
Bimod X Z
Tensor product of two bimodule objects as a bimodule object.
Equations
- M.tensor_Bimod N = {X := Bimod.tensor_Bimod.X M N, act_left := Bimod.tensor_Bimod.act_left M N (λ (X : C), _inst_4 X), one_act_left' := _, left_assoc' := _, act_right := Bimod.tensor_Bimod.act_right M N (λ (X : C), _inst_5 X), act_right_one' := _, right_assoc' := _, middle_assoc' := _}
@[simp]
theorem
Bimod.tensor_Bimod_act_right
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
(M : Bimod X Y)
(N : Bimod Y Z) :
(M.tensor_Bimod N).act_right = Bimod.tensor_Bimod.act_right M N
@[simp]
theorem
Bimod.tensor_Bimod_X
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
(M : Bimod X Y)
(N : Bimod Y Z) :
(M.tensor_Bimod N).X = Bimod.tensor_Bimod.X M N
@[simp]
theorem
Bimod.tensor_Bimod_act_left
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
(M : Bimod X Y)
(N : Bimod Y Z) :
(M.tensor_Bimod N).act_left = Bimod.tensor_Bimod.act_left M N
noncomputable
def
Bimod.tensor_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
{M₁ M₂ : Bimod X Y}
{N₁ N₂ : Bimod Y Z}
(f : M₁ ⟶ M₂)
(g : N₁ ⟶ N₂) :
M₁.tensor_Bimod N₁ ⟶ M₂.tensor_Bimod N₂
Tensor product of two morphisms of bimodule objects.
Equations
- Bimod.tensor_hom f g = {hom := category_theory.limits.colim_map (category_theory.limits.parallel_pair_hom (M₁.act_right ⊗ 𝟙 N₁.X) ((α_ M₁.X Y.X N₁.X).hom ≫ (𝟙 M₁.X ⊗ N₁.act_left)) (M₂.act_right ⊗ 𝟙 N₂.X) ((α_ M₂.X Y.X N₂.X).hom ≫ (𝟙 M₂.X ⊗ N₂.act_left)) ((f.hom ⊗ 𝟙 Y.X) ⊗ g.hom) (f.hom ⊗ g.hom) _ _), left_act_hom' := _, right_act_hom' := _}
@[simp]
theorem
Bimod.tensor_hom_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
{M₁ M₂ : Bimod X Y}
{N₁ N₂ : Bimod Y Z}
(f : M₁ ⟶ M₂)
(g : N₁ ⟶ N₂) :
theorem
Bimod.tensor_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
{M : Bimod X Y}
{N : Bimod Y Z} :
Bimod.tensor_hom (𝟙 M) (𝟙 N) = 𝟙 (M.tensor_Bimod N)
theorem
Bimod.tensor_comp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
{M₁ M₂ M₃ : Bimod X Y}
{N₁ N₂ N₃ : Bimod Y Z}
(f₁ : M₁ ⟶ M₂)
(f₂ : M₂ ⟶ M₃)
(g₁ : N₁ ⟶ N₂)
(g₂ : N₂ ⟶ N₃) :
Bimod.tensor_hom (f₁ ≫ f₂) (g₁ ≫ g₂) = Bimod.tensor_hom f₁ g₁ ≫ Bimod.tensor_hom f₂ g₂
noncomputable
def
Bimod.associator_Bimod.hom_aux
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
(P.tensor_Bimod Q).X ⊗ L.X ⟶ (P.tensor_Bimod (Q.tensor_Bimod L)).X
An auxiliary morphism for the definition of the underlying morphism of the forward component of the associator isomorphism.
Equations
- Bimod.associator_Bimod.hom_aux P Q L = (category_theory.limits.preserves_coequalizer.iso (category_theory.monoidal_category.tensor_right L.X) (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left))).inv ≫ category_theory.limits.coequalizer.desc ((α_ P.X Q.X L.X).hom ≫ (𝟙 P.X ⊗ category_theory.limits.coequalizer.π (Q.act_right ⊗ 𝟙 L.X) ((α_ Q.X T.X L.X).hom ≫ (𝟙 Q.X ⊗ L.act_left))) ≫ category_theory.limits.coequalizer.π (P.act_right ⊗ 𝟙 (Q.tensor_Bimod L).X) ((α_ P.X S.X (Q.tensor_Bimod L).X).hom ≫ (𝟙 P.X ⊗ (Q.tensor_Bimod L).act_left))) _
noncomputable
def
Bimod.associator_Bimod.hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
((P.tensor_Bimod Q).tensor_Bimod L).X ⟶ (P.tensor_Bimod (Q.tensor_Bimod L)).X
The underlying morphism of the forward component of the associator isomorphism.
Equations
theorem
Bimod.associator_Bimod.hom_left_act_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
((P.tensor_Bimod Q).tensor_Bimod L).act_left ≫ Bimod.associator_Bimod.hom P Q L = (𝟙 R.X ⊗ Bimod.associator_Bimod.hom P Q L) ≫ (P.tensor_Bimod (Q.tensor_Bimod L)).act_left
theorem
Bimod.associator_Bimod.hom_right_act_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
((P.tensor_Bimod Q).tensor_Bimod L).act_right ≫ Bimod.associator_Bimod.hom P Q L = (Bimod.associator_Bimod.hom P Q L ⊗ 𝟙 U.X) ≫ (P.tensor_Bimod (Q.tensor_Bimod L)).act_right
noncomputable
def
Bimod.associator_Bimod.inv_aux
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
P.X ⊗ (Q.tensor_Bimod L).X ⟶ ((P.tensor_Bimod Q).tensor_Bimod L).X
An auxiliary morphism for the definition of the underlying morphism of the inverse component of the associator isomorphism.
Equations
- Bimod.associator_Bimod.inv_aux P Q L = (category_theory.limits.preserves_coequalizer.iso (category_theory.monoidal_category.tensor_left P.X) (Q.act_right ⊗ 𝟙 L.X) ((α_ Q.X T.X L.X).hom ≫ (𝟙 Q.X ⊗ L.act_left))).inv ≫ category_theory.limits.coequalizer.desc ((α_ P.X Q.X L.X).inv ≫ (category_theory.limits.coequalizer.π (P.act_right ⊗ 𝟙 Q.X) ((α_ P.X S.X Q.X).hom ≫ (𝟙 P.X ⊗ Q.act_left)) ⊗ 𝟙 L.X) ≫ category_theory.limits.coequalizer.π ((P.tensor_Bimod Q).act_right ⊗ 𝟙 L.X) ((α_ (P.tensor_Bimod Q).X T.X L.X).hom ≫ (𝟙 (P.tensor_Bimod Q).X ⊗ L.act_left))) _
noncomputable
def
Bimod.associator_Bimod.inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
(P.tensor_Bimod (Q.tensor_Bimod L)).X ⟶ ((P.tensor_Bimod Q).tensor_Bimod L).X
The underlying morphism of the inverse component of the associator isomorphism.
Equations
theorem
Bimod.associator_Bimod.hom_inv_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
Bimod.associator_Bimod.hom P Q L ≫ Bimod.associator_Bimod.inv P Q L = 𝟙 ((P.tensor_Bimod Q).tensor_Bimod L).X
theorem
Bimod.associator_Bimod.inv_hom_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{R S T U : Mon_ C}
(P : Bimod R S)
(Q : Bimod S T)
(L : Bimod T U) :
Bimod.associator_Bimod.inv P Q L ≫ Bimod.associator_Bimod.hom P Q L = 𝟙 (P.tensor_Bimod (Q.tensor_Bimod L)).X
noncomputable
def
Bimod.left_unitor_Bimod.hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
Bimod.tensor_Bimod.X (Bimod.regular R) P ⟶ P.X
The underlying morphism of the forward component of the left unitor isomorphism.
Equations
noncomputable
def
Bimod.left_unitor_Bimod.inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
P.X ⟶ Bimod.tensor_Bimod.X (Bimod.regular R) P
The underlying morphism of the inverse component of the left unitor isomorphism.
theorem
Bimod.left_unitor_Bimod.hom_inv_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
theorem
Bimod.left_unitor_Bimod.inv_hom_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
theorem
Bimod.left_unitor_Bimod.hom_left_act_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
((Bimod.regular R).tensor_Bimod P).act_left ≫ Bimod.left_unitor_Bimod.hom P = (𝟙 R.X ⊗ Bimod.left_unitor_Bimod.hom P) ≫ P.act_left
theorem
Bimod.left_unitor_Bimod.hom_right_act_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
((Bimod.regular R).tensor_Bimod P).act_right ≫ Bimod.left_unitor_Bimod.hom P = (Bimod.left_unitor_Bimod.hom P ⊗ 𝟙 S.X) ≫ P.act_right
noncomputable
def
Bimod.right_unitor_Bimod.hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
Bimod.tensor_Bimod.X P (Bimod.regular S) ⟶ P.X
The underlying morphism of the forward component of the right unitor isomorphism.
noncomputable
def
Bimod.right_unitor_Bimod.inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
P.X ⟶ Bimod.tensor_Bimod.X P (Bimod.regular S)
The underlying morphism of the inverse component of the right unitor isomorphism.
theorem
Bimod.right_unitor_Bimod.hom_inv_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
theorem
Bimod.right_unitor_Bimod.inv_hom_id
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S) :
theorem
Bimod.right_unitor_Bimod.hom_left_act_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
(P.tensor_Bimod (Bimod.regular S)).act_left ≫ Bimod.right_unitor_Bimod.hom P = (𝟙 R.X ⊗ Bimod.right_unitor_Bimod.hom P) ≫ P.act_left
theorem
Bimod.right_unitor_Bimod.hom_right_act_hom'
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
{R S : Mon_ C}
(P : Bimod R S)
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
(P.tensor_Bimod (Bimod.regular S)).act_right ≫ Bimod.right_unitor_Bimod.hom P = (Bimod.right_unitor_Bimod.hom P ⊗ 𝟙 S.X) ≫ P.act_right
noncomputable
def
Bimod.associator_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{W X Y Z : Mon_ C}
(L : Bimod W X)
(M : Bimod X Y)
(N : Bimod Y Z) :
(L.tensor_Bimod M).tensor_Bimod N ≅ L.tensor_Bimod (M.tensor_Bimod N)
The associator as a bimodule isomorphism.
Equations
- L.associator_Bimod M N = Bimod.iso_of_iso {hom := Bimod.associator_Bimod.hom L M N, inv := Bimod.associator_Bimod.inv L M N, hom_inv_id' := _, inv_hom_id' := _} _ _
noncomputable
def
Bimod.left_unitor_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y : Mon_ C}
(M : Bimod X Y) :
(Bimod.regular X).tensor_Bimod M ≅ M
The left unitor as a bimodule isomorphism.
Equations
- M.left_unitor_Bimod = Bimod.iso_of_iso {hom := Bimod.left_unitor_Bimod.hom M, inv := Bimod.left_unitor_Bimod.inv M, hom_inv_id' := _, inv_hom_id' := _} _ _
noncomputable
def
Bimod.right_unitor_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y : Mon_ C}
(M : Bimod X Y) :
M.tensor_Bimod (Bimod.regular Y) ≅ M
The right unitor as a bimodule isomorphism.
Equations
- M.right_unitor_Bimod = Bimod.iso_of_iso {hom := Bimod.right_unitor_Bimod.hom M, inv := Bimod.right_unitor_Bimod.inv M, hom_inv_id' := _, inv_hom_id' := _} _ _
theorem
Bimod.whisker_left_comp_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
(M : Bimod X Y)
{N P Q : Bimod Y Z}
(f : N ⟶ P)
(g : P ⟶ Q) :
Bimod.tensor_hom (𝟙 M) (f ≫ g) = Bimod.tensor_hom (𝟙 M) f ≫ Bimod.tensor_hom (𝟙 M) g
theorem
Bimod.id_whisker_left_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y : Mon_ C}
{M N : Bimod X Y}
(f : M ⟶ N) :
Bimod.tensor_hom (𝟙 (Bimod.regular X)) f = M.left_unitor_Bimod.hom ≫ f ≫ N.left_unitor_Bimod.inv
theorem
Bimod.comp_whisker_left_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{W X Y Z : Mon_ C}
(M : Bimod W X)
(N : Bimod X Y)
{P P' : Bimod Y Z}
(f : P ⟶ P') :
Bimod.tensor_hom (𝟙 (M.tensor_Bimod N)) f = (M.associator_Bimod N P).hom ≫ Bimod.tensor_hom (𝟙 M) (Bimod.tensor_hom (𝟙 N) f) ≫ (M.associator_Bimod N P').inv
theorem
Bimod.comp_whisker_right_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
{M N P : Bimod X Y}
(f : M ⟶ N)
(g : N ⟶ P)
(Q : Bimod Y Z) :
Bimod.tensor_hom (f ≫ g) (𝟙 Q) = Bimod.tensor_hom f (𝟙 Q) ≫ Bimod.tensor_hom g (𝟙 Q)
theorem
Bimod.whisker_right_id_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y : Mon_ C}
{M N : Bimod X Y}
(f : M ⟶ N) :
Bimod.tensor_hom f (𝟙 (Bimod.regular Y)) = M.right_unitor_Bimod.hom ≫ f ≫ N.right_unitor_Bimod.inv
theorem
Bimod.whisker_right_comp_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{W X Y Z : Mon_ C}
{M M' : Bimod W X}
(f : M ⟶ M')
(N : Bimod X Y)
(P : Bimod Y Z) :
Bimod.tensor_hom f (𝟙 (N.tensor_Bimod P)) = (M.associator_Bimod N P).inv ≫ Bimod.tensor_hom (Bimod.tensor_hom f (𝟙 N)) (𝟙 P) ≫ (M'.associator_Bimod N P).hom
theorem
Bimod.whisker_assoc_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{W X Y Z : Mon_ C}
(M : Bimod W X)
{N N' : Bimod X Y}
(f : N ⟶ N')
(P : Bimod Y Z) :
Bimod.tensor_hom (Bimod.tensor_hom (𝟙 M) f) (𝟙 P) = (M.associator_Bimod N P).hom ≫ Bimod.tensor_hom (𝟙 M) (Bimod.tensor_hom f (𝟙 P)) ≫ (M.associator_Bimod N' P).inv
theorem
Bimod.whisker_exchange_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
{M N : Bimod X Y}
{P Q : Bimod Y Z}
(f : M ⟶ N)
(g : P ⟶ Q) :
Bimod.tensor_hom (𝟙 M) g ≫ Bimod.tensor_hom f (𝟙 Q) = Bimod.tensor_hom f (𝟙 P) ≫ Bimod.tensor_hom (𝟙 N) g
theorem
Bimod.pentagon_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{V W X Y Z : Mon_ C}
(M : Bimod V W)
(N : Bimod W X)
(P : Bimod X Y)
(Q : Bimod Y Z) :
Bimod.tensor_hom (M.associator_Bimod N P).hom (𝟙 Q) ≫ (M.associator_Bimod (N.tensor_Bimod P) Q).hom ≫ Bimod.tensor_hom (𝟙 M) (N.associator_Bimod P Q).hom = ((M.tensor_Bimod N).associator_Bimod P Q).hom ≫ (M.associator_Bimod N (P.tensor_Bimod Q)).hom
theorem
Bimod.triangle_Bimod
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)]
{X Y Z : Mon_ C}
(M : Bimod X Y)
(N : Bimod Y Z) :
(M.associator_Bimod (Bimod.regular Y) N).hom ≫ Bimod.tensor_hom (𝟙 M) N.left_unitor_Bimod.hom = Bimod.tensor_hom M.right_unitor_Bimod.hom (𝟙 N)
noncomputable
def
Bimod.Mon_bicategory
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.limits.has_coequalizers C]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_left X)]
[Π (X : C), category_theory.limits.preserves_colimits_of_size (category_theory.monoidal_category.tensor_right X)] :
The bicategory of algebras (monoids) and bimodules, all internal to some monoidal category.
Equations
- Bimod.Mon_bicategory = {to_category_struct := {to_quiver := {hom := λ (X Y : Mon_ C), Bimod X Y}, id := λ (X : Mon_ C), Bimod.regular X, comp := λ (_x _x_1 _x_2 : Mon_ C) (M : _x ⟶ _x_1) (N : _x_1 ⟶ _x_2), Bimod.tensor_Bimod M N}, hom_category := λ (_x _x_1 : Mon_ C), Bimod.category_theory.category, whisker_left := λ (_x _x_1 _x_2 : Mon_ C) (L : _x ⟶ _x_1) (_x_3 _x_4 : _x_1 ⟶ _x_2) (f : _x_3 ⟶ _x_4), Bimod.tensor_hom (𝟙 L) f, whisker_right := λ (_x _x_1 _x_2 : Mon_ C) (_x_3 _x_4 : _x ⟶ _x_1) (f : _x_3 ⟶ _x_4) (N : _x_1 ⟶ _x_2), Bimod.tensor_hom f (𝟙 N), associator := λ (_x _x_1 _x_2 _x_3 : Mon_ C) (L : _x ⟶ _x_1) (M : _x_1 ⟶ _x_2) (N : _x_2 ⟶ _x_3), Bimod.associator_Bimod L M N, left_unitor := λ (_x _x_1 : Mon_ C) (M : _x ⟶ _x_1), Bimod.left_unitor_Bimod M, right_unitor := λ (_x _x_1 : Mon_ C) (M : _x ⟶ _x_1), Bimod.right_unitor_Bimod M, whisker_left_id' := _, whisker_left_comp' := _, id_whisker_left' := _, comp_whisker_left' := _, id_whisker_right' := _, comp_whisker_right' := _, whisker_right_id' := _, whisker_right_comp' := _, whisker_assoc' := _, whisker_exchange' := _, pentagon' := _, triangle' := _}