isCoseparator_iff_mono — Mathlib

English

The coseparator property for G is equivalent to the family of monos given by Pi.lift being mono for all A.

Русский

Свойство косепразделителя для G эквивалентно тому, что семейство монофункций Pi.lift является моно-функтором для всех A.

LaTeX

$$$\\mathrm{IsCoseparator}(G) \\iff \\forall A: C,\\; \\mathrm{Mono}(\\Pi\\mathrm{lift}(f: A \\to G \\mapsto f))$$$

Lean4

theorem isCoseparator_iff_mono (G : C) [∀ A : C, HasProduct fun _ : A ⟶ G => G] :
    IsCoseparator G ↔ ∀ A : C, Mono (Pi.lift fun f : A ⟶ G => f) :=
  by
  rw [isCoseparator_def]
  refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
  · simpa using huv =≫ Pi.π _ i
  · haveI := h Y
    refine (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)
    simpa using hh j.as

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