isCoseparating_iff — Mathlib

English

In a preadditive setting, 𝒢 is coseparating iff for every f: X→Y, h from Y→G with G∈𝒢, f≫h=0 implies f=0.

Русский

В предадитивной среде 𝒢 косепараторное тогда и только тогда, когда для каждого f: X→Y, если f затем идёт в G через любой h: Y→G с G∈𝒢, и f≫h=0, то f=0.

LaTeX

$$$\mathrm{IsCoseparating}(\mathcal{G}) \iff \forall X,Y\; \forall f: X\to Y,\; (\forall G\in\mathcal{G},\; \forall h: Y\to G,\; f\circ h = 0) \Rightarrow f = 0$$$

Lean4

theorem isCoseparating_iff (𝒢 : Set C) :
    IsCoseparating 𝒢 ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0 :=
  ⟨fun h𝒢 X Y f hf => h𝒢 _ _ (by simpa only [Limits.zero_comp] using hf), fun h𝒢 X Y f g hfg =>
    sub_eq_zero.1 <| h𝒢 _ (by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg)⟩

Похожие утверждения