isLeftAdjoint_of_costructuredArrowTerminals

English

If each costructured-arrow category on G has a terminal object, G is a left adjoint.

Русский

Если в каждой CostructuredArrow G A есть терминальный объект, G является левой адъюнктной.

LaTeX

$$$\\forall A, HasTerminal(CostructuredArrow G A) \\Rightarrow G \\text{ is left adjoint}$$$

Lean4

/-- If each costructured arrow category on `G` has a terminal object, `G` is a left adjoint. -/
theorem isLeftAdjoint_of_costructuredArrowTerminals : G.IsLeftAdjoint where
  exists_rightAdjoint := ⟨rightAdjointOfCostructuredArrowTerminals G, ⟨Adjunction.adjunctionOfEquivRight _ _⟩⟩

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