English
For a family of arrows X → B indexed by α with π(a): X(a) ⟶ B, the presieve of arrows is effectively epimorphic iff the family X → B is an EffectiveEpiFamily.
Русский
Для семейства стрел X(a) → B индекса α предсеве по стрелам является эффективной эпиморфией тогда и только тогда, когда семействo стрел X(a) → B является EffectiveEpiFamily.
LaTeX
$$$$ (\mathrm{Presieve.ofArrows}\ X π).\mathrm{EffectiveEpimorphic} \iff \mathrm{EffectiveEpiFamily}\ X π $$$$
Lean4
theorem effectiveEpimorphic_family {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) :
(Presieve.ofArrows X π).EffectiveEpimorphic ↔ EffectiveEpiFamily X π :=
by
constructor
· intro (h : Nonempty _)
rw [Sieve.generateFamily_eq] at h
constructor
apply Nonempty.map (effectiveEpiFamilyStructOfIsColimit _ _) h
· rintro ⟨h⟩
change Nonempty _
rw [Sieve.generateFamily_eq]
apply Nonempty.map (isColimitOfEffectiveEpiFamilyStruct _ _) h
