Documentation

Mathlib.CategoryTheory.Functor.ReflectsIso

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.

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

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

    @[deprecated CategoryTheory.Functor.ReflectsIsomorphisms]

    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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {A : C} {B : C} (f : A B) (F : CategoryTheory.Functor C D) [CategoryTheory.IsIso (F.map f)] [F.ReflectsIsomorphisms] :

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

      @[instance 100]
      Equations
      • =
      instance CategoryTheory.reflectsIsomorphisms_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsIsomorphisms] [G.ReflectsIsomorphisms] :
      (F.comp G).ReflectsIsomorphisms
      Equations
      • =
      @[instance 100]
      Equations
      • =
      theorem CategoryTheory.Functor.balanced_of_preserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [F.PreservesEpimorphisms] [F.PreservesMonomorphisms] [CategoryTheory.Balanced D] :