# 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 ReflectsIsomorphisms F.

Any fully faithful functor reflects isomorphisms.

class CategoryTheory.Functor.ReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] (F : ) :

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.

• reflects : ∀ {A B : C} (f : A B) [inst : CategoryTheory.IsIso (F.map f)],

For any f, if F.map f is an iso, then so was f

Instances
theorem CategoryTheory.Functor.ReflectsIsomorphisms.reflects {C : Type u₁} [] {D : Type u₂} [] (F : ) [self : F.ReflectsIsomorphisms] {A : C} {B : C} (f : A B) [CategoryTheory.IsIso (F.map f)] :

For any f, if F.map f is an iso, then so was f

@[deprecated CategoryTheory.Functor.ReflectsIsomorphisms]
def CategoryTheory.ReflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] (F : ) :

Alias of CategoryTheory.Functor.ReflectsIsomorphisms.

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.

Equations
Instances For
theorem CategoryTheory.isIso_of_reflects_iso {C : Type u₁} [] {D : Type u₂} [] {A : C} {B : C} (f : A B) (F : ) [CategoryTheory.IsIso (F.map f)] [F.ReflectsIsomorphisms] :

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

theorem CategoryTheory.isIso_iff_of_reflects_iso {C : Type u₁} [] {D : Type u₂} [] {A : C} {B : C} (f : A B) (F : ) [F.ReflectsIsomorphisms] :
theorem CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms {C : Type u₁} [] {D : Type u₂} [] {F : } (hF : F.FullyFaithful) :
F.ReflectsIsomorphisms
@[instance 100]
instance CategoryTheory.reflectsIsomorphisms_of_full_and_faithful {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.Full] [F.Faithful] :
F.ReflectsIsomorphisms
Equations
• =
instance CategoryTheory.reflectsIsomorphisms_comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) [F.ReflectsIsomorphisms] [G.ReflectsIsomorphisms] :
(F.comp G).ReflectsIsomorphisms
Equations
• =
theorem CategoryTheory.reflectsIsomorphisms_of_comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) [(F.comp G).ReflectsIsomorphisms] :
F.ReflectsIsomorphisms
@[instance 100]
instance CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.ReflectsMonomorphisms] [F.ReflectsEpimorphisms] :
F.ReflectsIsomorphisms
Equations
• =
instance CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) [F.ReflectsIsomorphisms] :
(().obj F).ReflectsIsomorphisms
Equations
• =
theorem CategoryTheory.Functor.balanced_of_preserves {C : Type u₁} [] {D : Type u₂} [] (F : ) [F.ReflectsIsomorphisms] [F.PreservesEpimorphisms] [F.PreservesMonomorphisms] :