Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso

{C : Type u_1} →
  {D : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} C} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D} →
        {inst_2 : CategoryTheory.MonoidalCategoryStruct C} →
          [self : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct C D] →
            (d : D) →
              (c c' : C) →
                CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') ≅
                  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj
                    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c) c'

The structural isomorphism d ⊙ᵣ (c ⊗ c') ≅ (d ⊙ᵣ c) ⊙ᵣ c'.

Defined in

Mathlib.CategoryTheory.Monoidal.Action.Basic

Cited by

44 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.MonoidalCategory.MonoidalRightActionStruct