English
Under HasProduct, IsCoseparating 𝒢 is equivalent to the property that Pi.lift of Σ.snd is mono for every A.
Русский
При наличии произведений IsCoseparating 𝒢 эквивалентно тому, что Pi.lift(Σ.snd) является моно для каждого A.
LaTeX
$$$IsCoseparating(\mathcal{G}) \iff \forall A:\,C, Mono(Pi.lift(Σ.snd))$$$
Lean4
theorem isCoseparating_iff_mono (𝒢 : Set C) [∀ A : C, HasProduct fun f : Σ G : 𝒢, A ⟶ (G : C) => (f.1 : C)] :
IsCoseparating 𝒢 ↔ ∀ A : C, Mono (Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C))) :=
by
refine ⟨fun h A => ⟨fun u v huv => h _ _ fun G hG f => ?_⟩, fun h X Y f g hh => ?_⟩
· simpa using huv =≫ Pi.π (fun f : Σ G : 𝒢, A ⟶ (G : C) => (f.1 : C)) ⟨⟨G, hG⟩, f⟩
· haveI := h Y
refine (cancel_mono (Pi.lift (@Sigma.snd 𝒢 fun G => Y ⟶ (G : C)))).1 (limit.hom_ext fun j => ?_)
simpa using hh j.as.1.1 j.as.1.2 j.as.2
