isRightAdjoint_comp — Mathlib

English

If F and G are right adjoint functors, then their composition F ∘ G is also a right adjoint.

Русский

Если F и G являются правыми сопряжёнными функторами, то их композиция F ∘ G также является правым сопряжённым.

LaTeX

$$$\exists L,\ L \dashv (F \circ G)$$$

Lean4

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

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