English
If a single component f b is a separator, then the coproduct ∐ f is a separator.
Русский
Если компонент f b является разделителем, то их coproduct ∐ f является разделителем.
LaTeX
$$$\\mathrm{IsSeparator}(f b) \\Rightarrow \\mathrm{IsSeparator}(\\bigsqcup_{i} f(i))$$$
Lean4
theorem isSeparator_coprod (G H : C) [HasBinaryCoproduct G H] : IsSeparator (G ⨿ H) ↔ IsSeparating ({ G, H } : Set C) :=
by
refine ⟨fun h X Y u v huv => ?_, fun h => (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩
· refine h.def _ _ fun g => coprod.hom_ext ?_ ?_
· simpa using huv G (by simp) (coprod.inl ≫ g)
· simpa using huv H (by simp) (coprod.inr ≫ g)
· simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
rcases hZ with (rfl | rfl)
· simpa using coprod.inl ≫= huv (coprod.desc g 0)
· simpa using coprod.inr ≫= huv (coprod.desc 0 g)
