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.whiskerLeft Z f) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft 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.whiskerRight f Z) q = CategoryTheory.CategoryStruct.comp p f') (wg : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight g 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_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 : M.Hom N}, x = y x.hom = y.hom
    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 : M.Hom N}, x.hom = y.homx = y
    structure Bimod.Hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {A : Mon_ C} {B : Mon_ C} (M : Bimod A B) (N : Bimod A B) :
    Type v₁

    A morphism of bimodule objects.

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

      The identity morphism on a bimodule object.

      Equations
      Instances For
        Equations
        • M.homInhabited = { default := M.id' }
        @[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 : M.Hom N) (g : N.Hom 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 : M.Hom N) (g : N.Hom O) :
        M.Hom O

        Composition of bimodule object morphisms.

        Equations
        Instances For
          theorem Bimod.hom_ext_iff {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} :
          f = g f.hom = g.hom
          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) :
          @[simp]
          theorem Bimod.isoOfIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Mon_ C} {Y : Mon_ C} {P : Bimod X Y} {Q : Bimod X Y} (f : P.X Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X.X f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f.hom Y.X) Q.actRight) :
          (Bimod.isoOfIso f f_left_act_hom f_right_act_hom).inv.hom = f.inv
          @[simp]
          theorem Bimod.isoOfIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {X : Mon_ C} {Y : Mon_ C} {P : Bimod X Y} {Q : Bimod X Y} (f : P.X Q.X) (f_left_act_hom : CategoryTheory.CategoryStruct.comp P.actLeft f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X.X f.hom) Q.actLeft) (f_right_act_hom : CategoryTheory.CategoryStruct.comp P.actRight f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f.hom Y.X) Q.actRight) :
          (Bimod.isoOfIso f f_left_act_hom f_right_act_hom).hom.hom = f.hom

          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
          • One or more equations did not get rendered due to their size.
          Instances For

            A monoid object as a bimodule over itself.

            Equations
            • Bimod.regular A = { X := A.X, actLeft := A.mul, one_actLeft := , left_assoc := , actRight := A.mul, actRight_one := , right_assoc := , middle_assoc := }
            Instances For

              The forgetful functor from bimodule objects to the ambient category.

              Equations
              • Bimod.forget A = { obj := fun (A_1 : Bimod A B) => A_1.X, map := fun {X Y : Bimod A B} (f : X Y) => f.hom, map_id := , map_comp := }
              Instances For

                The underlying object of the tensor product of two bimodules.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  Left action for the tensor product of two bimodules.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Right action for the tensor product of two bimodules.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      Tensor product of two bimodule objects as a bimodule object.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        Left whiskering for morphisms of bimodule objects.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Right whiskering for morphisms of bimodule objects.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

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

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

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

                              Equations
                              Instances For

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    Instances For

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

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

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

                                        Equations
                                        Instances For

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

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            The associator as a bimodule isomorphism.

                                            Equations
                                            Instances For
                                              theorem Bimod.pentagon_bimod {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasCoequalizers C] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorLeft X)] [(X : C) → CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (CategoryTheory.MonoidalCategory.tensorRight X)] {V : Mon_ C} {W : Mon_ C} {X : Mon_ C} {Y : Mon_ C} {Z : Mon_ C} (M : Bimod V W) (N : Bimod W X) (P : Bimod X Y) (Q : Bimod Y Z) :
                                              CategoryTheory.CategoryStruct.comp (Bimod.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

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

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For