isLeftAdjoint_comp — Mathlib

English

If F and G are left adjoints, then their composite F ⋙ G is also left adjoint.

Русский

Если F и G — левые adjoint, то их композиция F ⋙ G тоже является левой adjoint.

LaTeX

$$$ (F \circ G).IsLeftAdjoint$$

Lean4

/-- If `F` and `G` are left adjoints then `F ⋙ G` is a left adjoint too. -/
instance isLeftAdjoint_comp {E : Type u₃} [Category.{v₃} E] (F : C ⥤ D) (G : D ⥤ E) [F.IsLeftAdjoint]
    [G.IsLeftAdjoint] : (F ⋙ G).IsLeftAdjoint where
  exists_rightAdjoint := ⟨_, ⟨(Adjunction.ofIsLeftAdjoint F).comp (Adjunction.ofIsLeftAdjoint G)⟩⟩

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