mono_iff_cancel_zero — Mathlib

English

A morphism f is mono iff for every P and g: P → Q, g ≫ f = 0 implies g = 0.

Русский

Морфизм f моно тогда и только тогда, когда для любого P и любого g: P → Q верно, что g ≫ f = 0 приводит к g = 0.

LaTeX

$$$\operatorname{Mono}(f) \iff \forall P\,\forall g: P \to Q,\; g \circ f = 0 \Rightarrow g = 0$$$

Lean4

theorem mono_iff_cancel_zero {Q R : C} (f : Q ⟶ R) : Mono f ↔ ∀ (P : C) (g : P ⟶ Q), g ≫ f = 0 → g = 0 :=
  ⟨fun _ _ _ => zero_of_comp_mono _, mono_of_cancel_zero f⟩

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