isRightAdjoint_post — Mathlib

English

If D has pushouts and G is right adjoint, then (Under.post G) is right adjoint.

Русский

Если у D есть pushouts и G — правый сопряжённый, то (Under.post G) является правым сопряжённым.

LaTeX

$$Under.isRightAdjoint_post$$

Lean4

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

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