isRightAdjoint_of_isEquivalence — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `F` is an equivalence, it's a right adjoint. -/
instance (priority := 10) isRightAdjoint_of_isEquivalence {F : C ⥤ D} [F.IsEquivalence] : IsRightAdjoint F :=
  F.asEquivalence.isRightAdjoint_functor

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