isLeftAdjoint_post

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.isLeftAdjoint_post

English

If F is left adjoint, then (Under.isLeftAdjoint_post) gives (Under.post F) is left adjoint.

Русский

Если F левый суффиксный, то Under.post F является левым сопряженным.

LaTeX

$$Under.post F isLeftAdjoint$$

Lean4

instance isLeftAdjoint_post [F.IsLeftAdjoint] : (post (X := X) F).IsLeftAdjoint :=
  let ⟨G, ⟨a⟩⟩ := ‹F.IsLeftAdjoint›;
  ⟨_, ⟨postAdjunctionLeft a⟩⟩

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

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

Разделы

Аффилиация

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