Structures · Category theory

CategoryTheory.MonoidalCategory.MonoidalLeftAction

A MonoidalLeftAction C D is the data of: - For every object c : C and d : D, an object c ⊙ₗ d of D. - For every morphism f : (c : C) ⟶ c' and every d : D, a morphism f ⊵ₗ d : c ⊙ₗ d ⟶ c' ⊙ₗ d. - For every morphism f : (d : D) ⟶ d' and every c : C, a morphism c ⊴ₗ f : c ⊙ₗ d ⟶ c ⊙ₗ d'. - For every pair of morphisms f : (c : C) ⟶ c' and f : (d : D) ⟶ d', a morphism f ⊙ₗ f' : c ⊙ₗ d ⟶ c' ⊙ₗ d'. - A structure isomorphism αₗ c c' d : c ⊗ c' ⊙ₗ d ≅ c ⊙ₗ c' ⊙ₗ d. - A structure isomorphism λₗ d : (𝟙_ C) ⊙ₗ d ≅ d. Furthermore, we require identities that turn - ⊙ₗ - into a bifunctor, ensure naturality of αₗ and λₗ, and ensure compatibilities with the associator and unitor isomorphisms in C.

Defined in

Mathlib.CategoryTheory.Monoidal.Action.Basic

Shape

2 explicit arguments · adds actionHom_def, actionHomRight_id, id_actionHomLeft, actionHom_comp, actionAssocIso_hom_naturality, actionUnitIso_hom_naturality, whiskerLeft_actionHomLeft, whiskerRight_actionHomLeft, associator_actionHom, leftUnitor_actionHom, rightUnitor_actionHom