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