IsCoseparating — Mathlib

English

If 𝒢 is separating and α is an equivalence C ≌ D, then the image α.functor.obj '' 𝒢 is separating in D.

Русский

Если 𝒢 разделяющее, и α — эквивалентность, то образ α.functor.obj '' 𝒢 разделяет в D.

LaTeX

$$$IsSeparating(\alpha.functor.obj '' 𝒢)$$$

Lean4

/-- We say that `𝒢` is a coseparating set if the functors `C(-, G)` for `G ∈ 𝒢` are collectively
    faithful, i.e., if `f ≫ h = g ≫ h` for all `h` with codomain in `𝒢` implies `f = g`. -/
def IsCoseparating (𝒢 : Set C) : Prop :=
  ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ G ∈ 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g

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