isRightAdjoint_iff_hasInitial_structuredArrow

English

A functor G is a right adjoint iff every StructuredArrow A G has an initial object.

Русский

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

LaTeX

$$G.IsRightAdjoint ⇔ ∀ A, HasInitial (StructuredArrow A G)$$

Lean4

theorem isRightAdjoint_iff_hasInitial_structuredArrow {G : D ⥤ C} :
    G.IsRightAdjoint ↔ ∀ A, HasInitial (StructuredArrow A G) :=
  ⟨fun _ A => (mkInitialOfLeftAdjoint _ (Adjunction.ofIsRightAdjoint G) A).hasInitial, fun _ =>
    isRightAdjointOfStructuredArrowInitials _⟩

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