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

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

• @CategoryTheory.ReflectsIsomorphisms = @CategoryTheory.Functor.ReflectsIsomorphisms

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)] [CategoryTheory.Functor.ReflectsIsomorphisms F] : CategoryTheory.IsIso f

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

instance CategoryTheory.reflectsIsomorphisms_of_full_and_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.Full F] [CategoryTheory.Functor.Faithful F] : CategoryTheory.Functor.ReflectsIsomorphisms F

Equations

• ⋯ = ⋯

instance CategoryTheory.reflectsIsomorphisms_of_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) [CategoryTheory.Functor.ReflectsIsomorphisms F] [CategoryTheory.Functor.ReflectsIsomorphisms G] : CategoryTheory.Functor.ReflectsIsomorphisms (CategoryTheory.Functor.comp F G)

Equations

• ⋯ = ⋯

instance CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Balanced C] (F : CategoryTheory.Functor C D) [CategoryTheory.Functor.ReflectsMonomorphisms F] [CategoryTheory.Functor.ReflectsEpimorphisms F] : CategoryTheory.Functor.ReflectsIsomorphisms F

Equations

• ⋯ = ⋯