isLeftAdjoint_post — Mathlib

English

If F is a left adjoint, then the Over-post construction (post X F) is left adjoint.

Русский

Если F — левый сопряжённый, то конструкция Over.post X F также левый сопряжённый.

LaTeX

$$(post F).IsLeftAdjoint$$

Lean4

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

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