English
If C is a balanced category and F : C ⥤ D reflects monomorphisms and epimorphisms, then F reflects isomorphisms.
Русский
Если C — балансированная категория, а F : C ⥤ D отражает моноиморфизмы и эпиморфизмы, то F отражает изоморфизмы.
LaTeX
$$$\\text{Balanced}(C) \\,\\wedge\\, F\\text{ reflects mono and epi} \\implies F\\text{ reflects isomorphisms}.$$$
Lean4
instance (priority := 100) reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms [Balanced C]
(F : C ⥤ D) [ReflectsMonomorphisms F] [ReflectsEpimorphisms F] : F.ReflectsIsomorphisms where
reflects f
hf := by
haveI : Epi f := epi_of_epi_map F inferInstance
haveI : Mono f := mono_of_mono_map F inferInstance
exact isIso_of_mono_of_epi f
