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_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
(F : Functor C D)
:
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.
For any
f, ifF.map fis an iso, then so wasf.
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]
:
IsIso f
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_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)
[F.ReflectsIsomorphisms]
:
theorem
CategoryTheory.Functor.FullyFaithful.reflectsIsomorphisms
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
{F : Functor C D}
(hF : F.FullyFaithful)
:
@[instance 100]
instance
CategoryTheory.reflectsIsomorphisms_of_full_and_faithful
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
(F : Functor C D)
[F.Full]
[F.Faithful]
:
instance
CategoryTheory.reflectsIsomorphisms_comp
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
{E : Type u_3}
[Category.{u_6, u_3} E]
(F : Functor C D)
(G : Functor D E)
[F.ReflectsIsomorphisms]
[G.ReflectsIsomorphisms]
:
(F.comp G).ReflectsIsomorphisms
theorem
CategoryTheory.reflectsIsomorphisms_of_comp
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
{E : Type u_3}
[Category.{u_6, u_3} E]
(F : Functor C D)
(G : Functor D E)
[(F.comp G).ReflectsIsomorphisms]
:
instance
CategoryTheory.instReflectsIsomorphismsFunctorObjWhiskeringRight
{C : Type u_1}
[Category.{u_6, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
{E : Type u_3}
[Category.{u_5, u_3} E]
(F : Functor D E)
[F.ReflectsIsomorphisms]
:
((Functor.whiskeringRight C D E).obj F).ReflectsIsomorphisms