# mathlibdocumentation

category_theory.reflects_isomorphisms

# Functors which reflect isomorphisms #

A functor F reflects isomorphisms if whenever F.map f is an isomorphism, f was too.

It is formalized as a Prop valued typeclass reflects_isomorphisms F.

Any fully faithful functor reflects isomorphisms.

@[class]
structure category_theory.reflects_isomorphisms {C : Type u₁} {D : Type u₂} (F : C D) :
Prop

Define what it means for a functor F : C ⥤ D to reflect isomorphisms: for any morphism f : A ⟶ B, if F.map f is an isomorphism then f is as well. Note that we do not assume or require that F is faithful.

Instances
theorem category_theory.is_iso_of_reflects_iso {C : Type u₁} {D : Type u₂} {A B : C} (f : A B) (F : C D) [category_theory.is_iso (F.map f)]  :

If F reflects isos and F.map f is an iso, then f is an iso.

@[instance]
def category_theory.of_full_and_faithful {C : Type u₁} {D : Type u₂} (F : C D)  :