Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight

{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.MonoidalLeftActionStruct C D] →
            (c : C) →
              {d d' : D} →
                (d ⟶ d') →
                  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d ⟶
                    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d')

The action of an object c : C on a map f : d ⟶ d' in D. If we are to consider the action as a functor Α : C ⥤ D ⥤ D, this is (Α.obj c).map f. This is denoted c ⊴ₗ f.

Defined in

Mathlib.CategoryTheory.Monoidal.Action.Basic

Cited by

83 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct