Theorems · Definition · category theory

Bimod.isoOfIso

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

Defined in

Mathlib.CategoryTheory.Monoidal.Bimod

Cited by

9 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategory