English
Let F: C → D be a functor with ReflectsFiniteEffectiveEpiFamilies. For a finite index α and X : α → C, π : α → X a ⟶ B, if the family (F.obj (X a)) with maps (F.map (π a)) is an effective epi family, then X and π form an effective epi family.
Русский
Пусть F: C → D — функтор, удовлетворяющий ReflectsFiniteEffectiveEpiFamilies. Для конечного множества индексов α и X : α → C, π : α → X a ⟶ B, если семейство (F.obj (X a)) с отображениями (F.map (π a)) является эффективной epi-семейственностью, то X и π образуют эффективную epi-семейство.
LaTeX
$$$\\forall {C} [\\mathbf{Category} C] {D} [\\mathbf{Category} D] (F : C \\to D) [ReflectsFiniteEffectiveEpiFamilies F] {\\alpha : Type} [Finite \\alpha] {B : C} (X : α \\to C) (\\pi : (a : α) \\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 finite_effectiveEpiFamily_of_map (F : C ⥤ D) [ReflectsFiniteEffectiveEpiFamilies F] {α : Type} [Finite α]
{B : C} (X : α → C) (π : (a : α) → (X a ⟶ B)) (h : EffectiveEpiFamily (fun a ↦ F.obj (X a)) (fun a ↦ F.map (π a))) :
EffectiveEpiFamily X π :=
ReflectsFiniteEffectiveEpiFamilies.reflects X π h
