instMonoidalClosed

Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

URI: https://scilib.ai/kg/mathlib#ModuleCat.instMonoidalClosed

Lean4

instance : MonoidalClosed (ModuleCat.{u} R) where
  closed
    M :=
    { rightAdj := (linearCoyoneda R (ModuleCat.{u} R)).obj (op M)
      adj :=
        Adjunction.mkOfHomEquiv
          { homEquiv := fun N P => monoidalClosedHomEquiv M N P
            homEquiv_naturality_left_symm := by
              intros
              ext : 1
              apply TensorProduct.ext'
              intro m n
              rfl } }

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

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

Разделы

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

Аффилиация

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