mono_iff_forall_injective — Mathlib

English

Let f: X → Y. Then f is mono iff for every object Z, the map g: Z → X, defined by g ↦ g ∘ f, is injective.

Русский

Пусть f: X → Y. Тогда f мономорфизм тогда и только тогда, когда для каждого объекта Z отображение g: Z → X, задаваемое g ↦ g ∘ f, инъективно.

LaTeX

$$$$\\mathrm{Mono}(f) \\iff \\forall Z, \\operatorname{Injective}(\\lambda g: Z\\to X, g\\circ f).$$$$

Lean4

/-- `f : X ⟶ Y` is a monomorphism iff for all `Z`, composition of morphisms `Z ⟶ X` with `f`
is injective. -/
theorem mono_iff_forall_injective {X Y : C} (f : X ⟶ Y) : Mono f ↔ ∀ Z, (fun g : Z ⟶ X ↦ g ≫ f).Injective :=
  ⟨fun _ _ _ _ hg ↦ (cancel_mono f).1 hg, fun h ↦ ⟨fun _ _ hg ↦ h _ hg⟩⟩

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