The monoidal category of bimodules over a monoid object #
Let R be a monoid object in a monoidal category C with coequalizers, such that tensoring on
either side preserves (universe-0 small) colimits. Mathlib's bicategory Bimod.monBicategory
of monoids and bimodules makes the category Bimod R R of endomorphisms of R a monoidal
category, under the tensor product of bimodules Bimod.tensorBimod. This file records that
instance and describes its structure maps on representatives in the tensor products of the
underlying objects.
Main definitions #
Bimod.monoidalCategory: the monoidal category ofR-R-bimodules under the tensor product of bimodules.
Main statements #
Bimod.π_whiskerLeft_hom,Bimod.π_whiskerRight_hom,Bimod.π_associator_hom_hom,Bimod.π_leftUnitor_hom_homandBimod.π_rightUnitor_hom_hom: the monoidal structure on representatives.Bimod.tensorBimod_actRight_eq: in a braided category, the tensor product of bimodules whose right actions are their left actions moved through the braiding again has this property.
@[instance_reducible]
noncomputable instance
Bimod.monoidalCategory
{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 : CategoryTheory.Mon C)
:
Bimodules over a monoid object R form a monoidal category under the tensor product of
bimodules, with unit the regular bimodule: the category of endomorphisms of R in Mathlib's
bicategory Bimod.monBicategory.
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)]
{R : CategoryTheory.Mon C}
(P : Bimod R R)
{Q Q' : Bimod R R}
(g : Q ⟶ Q')
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X g.hom)
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q'.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q'.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q'.actLeft)))
Whiskering on the left acts on representatives in P.X ⊗ Q.X by whiskering on the left.
theorem
Bimod.π_whiskerLeft_hom_assoc
{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 : CategoryTheory.Mon C}
(P : Bimod R R)
{Q Q' : Bimod R R}
(g : Q ⟶ Q')
{Z : C}
(h : (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q').X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X g.hom)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q'.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q'.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q'.actLeft)))
h)
Whiskering on the left acts on representatives in P.X ⊗ Q.X by whiskering on the left.
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)]
{R : CategoryTheory.Mon C}
{P P' : Bimod R R}
(f : P ⟶ P')
(Q : Bimod R R)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
(CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Q.X)
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P'.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P'.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P'.X Q.actLeft)))
Whiskering on the right acts on representatives in P.X ⊗ Q.X by whiskering on the right.
theorem
Bimod.π_whiskerRight_hom_assoc
{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 : CategoryTheory.Mon C}
{P P' : Bimod R R}
(f : P ⟶ P')
(Q : Bimod R R)
{Z : C}
(h : (CategoryTheory.MonoidalCategoryStruct.tensorObj P' Q).X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom Q.X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P'.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P'.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P'.X Q.actLeft)))
h)
Whiskering on the right acts on representatives in P.X ⊗ Q.X by whiskering on the right.
theorem
Bimod.π_associator_hom_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 : CategoryTheory.Mon C}
(P Q L : Bimod R R)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
L.X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.MonoidalCategoryStruct.tensorObj P Q).actRight L.X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q).X R.X
L.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q).X
L.actLeft)))
(CategoryTheory.MonoidalCategoryStruct.associator P Q L).hom.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X Q.X L.X).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight Q.actRight L.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Q.X R.X L.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q.X L.actLeft))))
(CategoryTheory.Limits.coequalizer.π
(CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight
(CategoryTheory.MonoidalCategoryStruct.tensorObj Q L).X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator P.X R.X
(CategoryTheory.MonoidalCategoryStruct.tensorObj Q L).X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X
(CategoryTheory.MonoidalCategoryStruct.tensorObj Q L).actLeft))))
The associator of bimodules on representatives in P.X ⊗ Q.X ⊗ L.X is the associator of the
underlying objects.
theorem
Bimod.π_associator_hom_hom_assoc
{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 : CategoryTheory.Mon C}
(P Q L : Bimod R R)
{Z : C}
(h : (CategoryTheory.MonoidalCategoryStruct.tensorObj P (CategoryTheory.MonoidalCategoryStruct.tensorObj Q L)).X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight Q.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X Q.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X Q.actLeft)))
L.X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π
(CategoryTheory.MonoidalCategoryStruct.whiskerRight
(CategoryTheory.MonoidalCategoryStruct.tensorObj P Q).actRight L.X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q).X R.X
L.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj P Q).X
L.actLeft)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P Q L).hom.hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X Q.X L.X).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight Q.actRight L.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Q.X R.X L.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q.X L.actLeft))))
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π
(CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight
(CategoryTheory.MonoidalCategoryStruct.tensorObj Q L).X)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategoryStruct.associator P.X R.X
(CategoryTheory.MonoidalCategoryStruct.tensorObj Q L).X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X
(CategoryTheory.MonoidalCategoryStruct.tensorObj Q L).actLeft)))
h))
The associator of bimodules on representatives in P.X ⊗ Q.X ⊗ L.X is the associator of the
underlying objects.
theorem
Bimod.π_leftUnitor_hom_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 : CategoryTheory.Mon C}
(P : Bimod R R)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight (regular R).actRight P.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (regular R).X R.X P.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (regular R).X P.actLeft)))
(CategoryTheory.MonoidalCategoryStruct.leftUnitor P).hom.hom = P.actLeft
The left unitor of bimodules is induced by the left action.
theorem
Bimod.π_leftUnitor_hom_hom_assoc
{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 : CategoryTheory.Mon C}
(P : Bimod R R)
{Z : C}
(h : P.X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight (regular R).actRight P.X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (regular R).X R.X P.X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft (regular R).X P.actLeft)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor P).hom.hom h) = CategoryTheory.CategoryStruct.comp P.actLeft h
The left unitor of bimodules is induced by the left action.
theorem
Bimod.π_rightUnitor_hom_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 : CategoryTheory.Mon C}
(P : Bimod R R)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight (regular R).X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X (regular R).X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (regular R).actLeft)))
(CategoryTheory.MonoidalCategoryStruct.rightUnitor P).hom.hom = P.actRight
The right unitor of bimodules is induced by the right action.
theorem
Bimod.π_rightUnitor_hom_hom_assoc
{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 : CategoryTheory.Mon C}
(P : Bimod R R)
{Z : C}
(h : P.X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.coequalizer.π (CategoryTheory.MonoidalCategoryStruct.whiskerRight P.actRight (regular R).X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator P.X R.X (regular R).X).hom
(CategoryTheory.MonoidalCategoryStruct.whiskerLeft P.X (regular R).actLeft)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor P).hom.hom h) = CategoryTheory.CategoryStruct.comp P.actRight h
The right unitor of bimodules is induced by the right action.
theorem
Bimod.tensorBimod_actRight_eq
{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 : CategoryTheory.Mon C}
[CategoryTheory.BraidedCategory C]
(P Q : Bimod R R)
(hP : P.actRight = CategoryTheory.CategoryStruct.comp (β_ R.X P.X).inv P.actLeft)
(hQ : Q.actRight = CategoryTheory.CategoryStruct.comp (β_ R.X Q.X).inv Q.actLeft)
:
(P.tensorBimod Q).actRight = CategoryTheory.CategoryStruct.comp (β_ R.X (P.tensorBimod Q).X).inv (P.tensorBimod Q).actLeft
If the right actions of two R-R-bimodules are their left actions precomposed with the
inverse braiding, then so is the right action of their tensor product.