Structures · Category theory

CategoryTheory.MonoidalCategory.MonoidalRightAction

A MonoidalRightAction 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, actionHomRight_whiskerRight, whiskerRight_actionHomLeft, actionHom_associator, actionHom_leftUnitor, actionHom_rightUnitor