English
If G is a separator, then for every A, the projection from the Sigma object to A is an epimorphism; equivalently, the Sigma-desc map is epi for all A.
Русский
Если G является разделителем, то для каждого объекта A проекция из coproduct (Sigma) на A является эпиморфизм; эквивалентно тому, что Sigma-desc-морфизм является эпиморфом для всех A.
LaTeX
$$$\\mathrm{IsSeparator}(G) \\iff \\forall A: C,\\; \\mathrm{Epi}(\\Sigma.\\mathrm{desc}(f))$$$
Lean4
theorem isSeparator_iff_epi (G : C) [∀ A : C, HasCoproduct fun _ : G ⟶ A => G] :
IsSeparator G ↔ ∀ A : C, Epi (Sigma.desc fun f : G ⟶ A => f) :=
by
rw [isSeparator_def]
refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
· simpa using Sigma.ι _ i ≫= huv
· haveI := h X
refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)
simpa using hh j.as
