isSeparating_iff — Mathlib

English

In a preadditive category, a family 𝒢 is separating iff for every morphism f, if h ∘ f = 0 for all h from all objects in 𝒢, then f = 0.

Русский

В предадитивной категории семейство 𝒢 разделяющее тогда и только тогда, когда для каждого морфизма f, если h ∘ f = 0 для всех факторов h из объектов 𝒢, то f = 0.

LaTeX

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

Lean4

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

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