instIsLeftAdjointModuleCatMulOppositeEndTensorObj

Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsGrothendieckAbelian.instIsLeftAdjointModuleCatMulOppositeEndTensorObj

English

There is a compatibility between LLP and RLP for monomorphisms in the abelian context with separator G.

Русский

Существует совместимость между LLP и RLP для мономорфизмов в абелевой обстановке с разделяющим G.

LaTeX

$$$(llp) = (rlp)$ on Monomorphisms$$

Lean4

instance {G : C} : (tensorObj G).IsLeftAdjoint :=
  (tensorObjPreadditiveCoyonedaObjAdjunction G).isLeftAdjoint

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

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

Разделы

Аффилиация

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