epi_of_zero_cancel — Mathlib

English

If f is right-cancellable by zero: for all Z and g: Y → Z, f ∘ g = 0 implies g = 0, then f is epi.

Русский

Если для любого Z и g: Y→Z выполняется f∘g = 0 ⇒ g = 0, то f — эпиморфизм.

LaTeX

$$$\forall Z,g: Y\to Z,\; f\circ g=0 \Rightarrow g=0 \Rightarrow Epi f$$$

Lean4

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

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