isRightAdjointOfStructuredArrowInitials

English

If every structured-arrow category on G has an initial object, G is a right adjoint.

Русский

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

LaTeX

$$If ∀ A HasInitial (StructuredArrow A G), then G is a right adjoint.$$

Lean4

/-- If each structured arrow category on `G` has an initial object, `G` is a right adjoint. -/
theorem isRightAdjointOfStructuredArrowInitials : G.IsRightAdjoint where
  exists_leftAdjoint := ⟨_, ⟨adjunctionOfStructuredArrowInitials G⟩⟩

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