curriedActionMop

Mathlib.CategoryTheory.Monoidal.Action.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop

Lean4

/-- A variant of
`CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction`
that takes value in the monoidal opposite of `D ⥤ D`. -/
@[simps! obj_unmop_obj obj_unmop_map]
def curriedActionMop : C ⥤ (D ⥤ D)ᴹᵒᵖ :=
  (curriedAction C D) ⋙
    mopFunctor
      _
        -- This simp lemma is necessary because the simps projection generated for
        -- unmop of a morphism is actually its underlying unmop field, rather than
        -- the application of `Quiver.Hom.unmop`.

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

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

Разделы

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

Аффилиация

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