isLeftAdjoint_of_isEquivalence — Mathlib

English

If F is an equivalence of categories, then F is a left adjoint.

Русский

Если F — эквивалентность категорий, тогда F является левой адъюнктной.

LaTeX

$$$F \\text{ is an equivalence} \\Rightarrow F \\text{ is a left adjoint}$$$

Lean4

/-- If `F` is an equivalence, it's a left adjoint. -/
instance (priority := 10) isLeftAdjoint_of_isEquivalence {F : C ⥤ D} [F.IsEquivalence] : IsLeftAdjoint F :=
  F.asEquivalence.isLeftAdjoint_functor

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