isLeftAdjoint_iff_hasTerminal_costructuredArrow

English

A functor F is a left adjoint iff for all A, CostructuredArrow F A has a terminal object.

Русский

Функтор F — левая адъюнктность тогда и только тогда, когда для каждого A категория CostructuredArrow F A имеет терминальный объект.

LaTeX

$$F.IsLeftAdjoint ⇔ ∀ A, HasTerminal (CostructuredArrow F A)$$

Lean4

theorem isLeftAdjoint_iff_hasTerminal_costructuredArrow {F : C ⥤ D} :
    F.IsLeftAdjoint ↔ ∀ A, HasTerminal (CostructuredArrow F A) :=
  ⟨fun _ A => (mkTerminalOfRightAdjoint _ (Adjunction.ofIsLeftAdjoint F) A).hasTerminal, fun _ =>
    isLeftAdjoint_of_costructuredArrowTerminals _⟩

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