isRightAdjoint_post — Mathlib

English

For any functor G: D ⥤ T with a right adjoint structure, (Over.post G) is a right adjoint.

Русский

Для любого функторa G: D ⥤ T с правым сопряженным, Over.post G — правый сопряженный.

LaTeX

$$$\\forall G\\, [G.\\mathbf{IsRightAdjoint}]\\; \\operatorname{IsRightAdjoint}(\\mathrm{Over.post}\\ G)$$$

Lean4

instance isRightAdjoint_post {Y : D} {G : D ⥤ T} [G.IsRightAdjoint] : (post (X := Y) G).IsRightAdjoint :=
  let ⟨F, ⟨a⟩⟩ := ‹G.IsRightAdjoint›;
  ⟨_, ⟨postAdjunctionRight a⟩⟩

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