Documentation

Mathlib.CategoryTheory.Functor.ReflectsIso.Basic

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.

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) [IsIso (F.map f)] : IsIso f

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

Instances
    theorem CategoryTheory.isIso_of_reflects_iso {C : Type u_1} [Category.{u_4, u_1} C] {D : Type u_2} [Category.{u_5, u_2} D] {A B : C} (f : A B) (F : Functor C D) [IsIso (F.map f)] [F.ReflectsIsomorphisms] :

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