English
Let F: C → D be a functor with ReflectsEffectiveEpiFamilies. For any α, B in C and objects X: α → C with maps π(a): X(a) → B, if the family (F.obj (X a)) with maps (F.map (π a)) is an effective epi family, then the original X and π form an effective epi family.
Русский
Пусть F: C → D — функтор, удовлетворяющий ReflectsEffectiveEpiFamilies. Для любой пары α, B в C и семейства объектов X: α → C с переходными отображениями π(a): X(a) → B, если семейство (F.obj (X a)) с переходами (F.map (π a)) является эффективной семейной эпиморфизмов, то исходная пара X, π образуют эффективную epi-семейство.
LaTeX
$$$\\forall {C} [\\mathbf{Category} C] {D} [\\mathbf{Category} D] (F : C \\to D) [ReflectsEffectiveEpiFamilies F] {\\alpha : Type} {B : C} (X : \\alpha \\to C) (\\pi : (a : \\alpha) \\to (X a \\to B)) (h : \\operatorname{EffectiveEpiFamily}( (\\lambda a. F.obj (X a)) ) ( (\\lambda a. F.map (\\pi a)) )) , \\operatorname{EffectiveEpiFamily} X \\pi$$
Lean4
theorem effectiveEpiFamily_of_map (F : C ⥤ D) [ReflectsEffectiveEpiFamilies.{u} F] {α : Type u} {B : C} (X : α → C)
(π : (a : α) → (X a ⟶ B)) (h : EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a ↦ F.map (π a))) :
EffectiveEpiFamily X π :=
ReflectsEffectiveEpiFamilies.reflects X π h
