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.

source
class CategoryTheory.Functor.ReflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor 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.

  • 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
    source
    @[deprecated CategoryTheory.Functor.ReflectsIsomorphisms (since := "2024-04-06")]
    def CategoryTheory.ReflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :
    Prop

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

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

      source
      theorem CategoryTheory.isIso_iff_of_reflects_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {A B : C} (f : A ⟶ B) (F : Functor C D) [F.ReflectsIsomorphisms] :
      IsIso (F.map f) ↔ IsIso f
      source
      theorem CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) :
      F.ReflectsIsomorphisms
      source
      @[instance 100]
      instance CategoryTheory.reflectsIsomorphisms_of_full_and_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] :
      F.ReflectsIsomorphisms
      source
      instance CategoryTheory.reflectsIsomorphisms_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.ReflectsIsomorphisms] [G.ReflectsIsomorphisms] :
      (F.comp G).ReflectsIsomorphisms
      source
      theorem CategoryTheory.reflectsIsomorphisms_of_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [(F.comp G).ReflectsIsomorphisms] :
      F.ReflectsIsomorphisms
      source
      @[instance 100]
      instance CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] [Balanced C] (F : Functor C D) [F.ReflectsMonomorphisms] [F.ReflectsEpimorphisms] :
      F.ReflectsIsomorphisms
      source
      instance CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor D E) [F.ReflectsIsomorphisms] :
      ((whiskeringRight C D E).obj F).ReflectsIsomorphisms
      source
      theorem CategoryTheory.Functor.balanced_of_preserves {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.ReflectsIsomorphisms] [F.PreservesEpimorphisms] [F.PreservesMonomorphisms] [Balanced D] :
      Balanced C