mono_of_cancel_zero — Mathlib

English

If for all Z and g: Z → X, g ∘ f = 0 implies g = 0, then f is mono.

Русский

Если для всех Z и g: Z ⟶ X выполняется g ∘ f = 0 ⇒ g = 0, то f является моно.

LaTeX

$$$\forall Z,g: Z\to X, g \circ f = 0 \Rightarrow g = 0 \; \Rightarrow \; Mono f$$$

Lean4

/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `f` is a monomorphism. -/
theorem mono_of_cancel_zero {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X) (_ : g ≫ f = 0), g = 0) : Mono f :=
  mono_of_zero_kernel f 0 <| zeroKernelOfCancelZero f hf

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