English
For a family f: β → C, IsCoseparator of the Pi-object ∏ᶜ f is equivalent to IsCoseparating of the range of f.
Русский
Для семейства f: β → C, косепараторность Pi-объекта ∏ᶜ f эквивалентна косепараторности диапазона f.
LaTeX
$$$\\mathrm{IsCoseparator}(\\prod^\\!\\!_i f_i) \\iff \\mathrm{IsCoseparating}(\\mathrm{range}(f))$$$
Lean4
theorem isCoseparator_pi {β : Type w} (f : β → C) [HasProduct f] :
IsCoseparator (∏ᶜ f) ↔ IsCoseparating (Set.range f) :=
by
refine ⟨fun h X Y u v huv => ?_, fun h => (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => ?_⟩
· refine h.def _ _ fun g => limit.hom_ext fun b => ?_
simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _)
· obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b
