epi_of_cancel_zero — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem epi_of_cancel_zero {P Q : C} (f : P ⟶ Q) (h : ∀ {R : C} (g : Q ⟶ R), f ≫ g = 0 → g = 0) : Epi f :=
  ⟨fun {Z} g g' hg => sub_eq_zero.1 <| h _ <| (map_sub (leftComp Z f) g g').trans <| sub_eq_zero.2 hg⟩

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