instIsLeftAdjointForget — Mathlib

English

The forgetful functor forget X has a right adjoint if and only if every binary coproduct X ⊔ Y exists in C.

Русский

Функтор забывания forget X имеет правый сопряжённый тогда и только тогда, когда в C существуют все бинарные coproduct X ⊔ Y.

LaTeX

$$HasRightAdjoint forget_X \Leftrightarrow ∀ Y, ∃ X ⊔ Y$$

Lean4

/-- Note that the binary products assumption is necessary: the existence of a right adjoint to
`Over.forget X` is equivalent to the existence of each binary product `X ⨯ -`. -/
instance : (forget X).IsLeftAdjoint :=
  ⟨_, ⟨forgetAdjStar X⟩⟩

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