English
If F is an equivalence of categories, then F reflects effective epi families; consequently it reflects effective epis.
Русский
Если F — эквивалентность категорий, то F отражает эффективные семейства эпиморфизмов; следовательно, F отражает эффективные эпиморфизмы.
LaTeX
$$$\\forall {C} [\\mathbf{Category} C] {D} [\\mathbf{Category} D] (F : \\mathbf{Functor} C D) [IsEquivalence F] , \\operatorname{ReflectsEffectiveEpiFamilies} F$$
Lean4
instance (F : C ⥤ D) [ReflectsEffectiveEpiFamilies.{0} F] : ReflectsFiniteEffectiveEpiFamilies F where
reflects _ _
h := by
have := F.effectiveEpiFamily_of_map _ _ h
infer_instance
