English
If F: C ⥤ D is an equivalence and G : D ⥤ C with η: Id_C ≅ F ⋙ G and ε: G ⋙ F ≅ Id_D, then F is an equivalence.
Русский
Пусть F: C ⥤ D является эквивалентностью, а G: D ⥤ C оснащён естественными изоморфиями η: Id_C ≅ F ⋙ G и ε: G ⋙ F ≅ Id_D. Тогда F — эквивалентность.
LaTeX
$$$(\eta : \mathrm{Id}_C \cong F \circ G) \; (ε : G \circ F \cong \mathrm{Id}_D) \Rightarrow \operatorname{IsEquivalence} F.$$$
Lean4
/-- To see that a functor is an equivalence, it suffices to provide an inverse functor `G` such that
`F ⋙ G` and `G ⋙ F` are naturally isomorphic to identity functors. -/
protected theorem mk' {F : C ⥤ D} (G : D ⥤ C) (η : 𝟭 C ≅ F ⋙ G) (ε : G ⋙ F ≅ 𝟭 D) : IsEquivalence F :=
inferInstanceAs (IsEquivalence (Equivalence.mk F G η ε).functor)
