CategoryTheory.isIso_of_reflects_iso

theorem CategoryTheory.isIso_of_reflects_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {A B : C} (f : A ⟶ B) (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.IsIso (F.map f)] [inst_3 : F.ReflectsIsomorphisms], CategoryTheory.IsIso f

This theorem states that if a functor `F` reflects isomorphisms and `F.map f` is an isomorphism, then `f` is also an isomorphism. In the context of category theory, this theorem is saying that if we have two categories `C` and `D`, objects `A` and `B` in `C`, and a morphism `f` from `A` to `B`, if the image of `f` under the functor `F` is an isomorphism and `F` has the property that it reflects isomorphisms, then `f` must also be an isomorphism. The property of a functor reflecting isomorphisms means that whenever the functor sends a morphism to an isomorphism, the original morphism was also an isomorphism.

More concisely: If a functor reflecting isomorphisms maps an isomorphism to an isomorphism, then the original morphism is an isomorphism.