Documentation

Mathlib.CategoryTheory.Monoidal.Bimod

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

theorem id_tensor_π_preserves_coequalizer_inv_colimMap_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X Y) (g : X Y) (f' : X' Y') (g' : X' Y') (p : CategoryTheory.MonoidalCategory.tensorObj Z X X') (q : CategoryTheory.MonoidalCategory.tensorObj Z Y Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Z) g) q = CategoryTheory.CategoryStruct.comp p g') (h : Y' Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) :
theorem π_tensor_id_preserves_coequalizer_inv_colimMap_desc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (f : X Y) (g : X Y) (f' : X' Y') (g' : X' Y') (p : CategoryTheory.MonoidalCategory.tensorObj X Z X') (q : CategoryTheory.MonoidalCategory.tensorObj Y Z Y') (wf : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Z)) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g (CategoryTheory.CategoryStruct.id Z)) q = CategoryTheory.CategoryStruct.comp p g') (h : Y' Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h) :
structure Bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (A : Mon_ C) (B : Mon_ C) :
Type (max u₁ v₁)

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

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

    The identity morphism on a bimodule object.

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

      Composition of bimodule object morphisms.

      Instances For
        theorem Bimod.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} (f : M N) (g : M N) (h : f.hom = g.hom) :
        f = g
        @[simp]
        theorem Bimod.comp_hom' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} {M : Bimod A B} {N : Bimod A B} {K : Bimod A B} (f : M N) (g : N K) :

        Construct an isomorphism of bimodules by giving an isomorphism between the underlying objects and checking compatibility with left and right actions only in the forward direction.

        Instances For

          A monoid object as a bimodule over itself.

          Instances For

            The forgetful functor from bimodule objects to the ambient category.

            Instances For

              The underlying object of the tensor product of two bimodules.

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

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

                Instances For

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

                  Instances For

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

                    Instances For

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

                      Instances For