Action functors of a monoidal left action

For a left action of a monoidal category C on a category D, this file records how the action functors actionLeft D c : D ⥤ D compose and invert.

• actionLeftTensorIso identifies the action functor of c ⊗ c' with the composite actionLeft D c' ⋙ actionLeft D c, with components the associator αₗ c c'. In particular a left action of a monoid M (that is, of Discrete M) satisfies T (h * g) ≅ T g ⋙ T h.
• actionLeftEquivOfIso shows that the action functor of an object with a tensor inverse is an equivalence; actionLeftEquivalence specializes this to Discrete G for a group G, where the inverse of the action functor of g is the action functor of g⁻¹.
• actionHomLeft_eq_eqToHom: when C is discrete, the action of a morphism of C is an eqToHom.

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftTensorIso {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (D : Type u_2) [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (c c' : C) : actionLeft D (tensorObj c c') ≅ (actionLeft D c').comp (actionLeft D c)

The action functor of a tensor product is the composite of the action functors, in the order c ⊗ c' ↦ actionLeft D c' ⋙ actionLeft D c; its components are αₗ c c' d.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftTensorIso_hom_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (D : Type u_2) [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (c c' : C) (d : D) : (actionLeftTensorIso D c c').hom.app d = (actionAssocIso c c' d).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftTensorIso_inv_app {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (D : Type u_2) [Category.{v_2, u_2} D] [MonoidalLeftAction C D] (c c' : C) (d : D) : (actionLeftTensorIso D c c').inv.app d = (actionAssocIso c c' d).inv

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftEquivOfIso {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (D : Type u_2) [Category.{v_2, u_2} D] [MonoidalLeftAction C D] {c c' : C} (e : tensorObj c' c ≅ tensorUnit C) (e' : tensorObj c c' ≅ tensorUnit C) : D ≌ D

If c' ⊗ c ≅ 𝟙_ C and c ⊗ c' ≅ 𝟙_ C, then the action functor of c is an equivalence whose inverse is the action functor of c'.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftEquivOfIso_functor {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (D : Type u_2) [Category.{v_2, u_2} D] [MonoidalLeftAction C D] {c c' : C} (e : tensorObj c' c ≅ tensorUnit C) (e' : tensorObj c c' ≅ tensorUnit C) : (actionLeftEquivOfIso D e e').functor = actionLeft D c

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftEquivOfIso_inverse {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (D : Type u_2) [Category.{v_2, u_2} D] [MonoidalLeftAction C D] {c c' : C} (e : tensorObj c' c ≅ tensorUnit C) (e' : tensorObj c c' ≅ tensorUnit C) : (actionLeftEquivOfIso D e e').inverse = actionLeft D c'

def CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftEquivalence (D : Type u_2) [Category.{v_2, u_2} D] {G : Type u_3} [Group G] [MonoidalLeftAction (Discrete G) D] (g : G) : D ≌ D

For a left action of a group G, the action functor of g is an equivalence whose inverse is the action functor of g⁻¹.

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftEquivalence_functor (D : Type u_2) [Category.{v_2, u_2} D] {G : Type u_3} [Group G] [MonoidalLeftAction (Discrete G) D] (g : G) : (actionLeftEquivalence D g).functor = actionLeft D { as := g }

@[simp]

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionLeftEquivalence_inverse (D : Type u_2) [Category.{v_2, u_2} D] {G : Type u_3} [Group G] [MonoidalLeftAction (Discrete G) D] (g : G) : (actionLeftEquivalence D g).inverse = actionLeft D { as := g⁻¹ }

theorem CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomLeft_eq_eqToHom {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] {D : Type u_2} [Category.{v_2, u_2} D] [MonoidalLeftAction C D] [IsDiscrete C] {c c' : C} (f : c ⟶ c') (d : D) : actionHomLeft f d = eqToHom ⋯

When the acting monoidal category is discrete, the action of a morphism on an object is an eqToHom.