Balanced categories and functors reflecting isomorphisms #
If a category is C, and a functor out of C reflects epimorphisms and monomorphsims,
then the functor reflects isomorphisms.
Furthermore, categories that admits a functor that ReflectsIsomorphisms, PreservesEpimorphisms
and PreservesMonomorphisms are balanced.
@[instance 100]
instance
CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
[Balanced C]
(F : Functor C D)
[F.ReflectsMonomorphisms]
[F.ReflectsEpimorphisms]
:
theorem
CategoryTheory.Functor.balanced_of_preserves
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.ReflectsIsomorphisms]
[F.PreservesEpimorphisms]
[F.PreservesMonomorphisms]
[Balanced D]
:
Balanced C