instIsRightAdjointForget — Mathlib

English

The forgetful functor forget X has a right adjoint (via costarAdjForget X).

Русский

Забывающий функтор forget X имеет правый сопряжённый.

LaTeX

$$Under.forget X IsRightAdjoint$$

Lean4

/-- Note that the binary coproducts assumption is necessary: the existence of a left adjoint to
`Under.forget X` is equivalent to the existence of each binary coproduct `X ⨿ -`. -/
instance : (forget X).IsRightAdjoint :=
  ⟨_, ⟨costarAdjForget X⟩⟩

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