evaluationRightAction

Mathlib.CategoryTheory.Monoidal.Action.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction

Lean4

/-- Functor evaluation gives a right action of `C ⥤ C`.

Note that in the literature, this is defined as a left action, but mathlib's
monoidal structure on `C ⥤ C` is the monoidal opposite of the one usually
considered in the literature. -/
@[simps! actionObj actionHomLeft actionHomRight actionAssocIso actionUnitIso]
scoped instance evaluationRightAction : MonoidalRightAction (C ⥤ C) C :=
  MonoidalRightAction.actionOfMonoidalFunctorToEndofunctor (𝟭 (C ⥤ C))

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru