of_isLeftAdjoint

Mathlib.CategoryTheory.Functor.Flat

URI: https://scilib.ai/kg/mathlib#CategoryTheory.RepresentablyCoflat.of_isLeftAdjoint

← MathLib Explorer

English

If F is a right adjoint, then RepresentablyFlat F.

Русский

Если F является правым сопряжением, то F представимо плоский.

LaTeX

$$$$ \\mathrm{RepresentablyFlat}(F). $$$$

Lean4

instance of_isLeftAdjoint [F.IsLeftAdjoint] : RepresentablyCoflat F where
  filtered _ := IsFiltered.of_isTerminal _ (mkTerminalOfRightAdjoint _ (.ofIsLeftAdjoint F) _)

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

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

Разделы

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

Аффилиация

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