isIso_of_mono_of_nonzero — Mathlib

English

A mono f: X ⟶ Y with Y simple and f ≠ 0 is an isomorphism.

Русский

Моно-отрез f: X → Y в категории с нулевыми морфизмами и простым Y обязательно является изоморфизмом, если f не ноль.

LaTeX

$$$ \forall X Y, [Simple\ Y], (f: X \to Y), [Mono f], (f \neq 0) \Rightarrow IsIso f. $$$

Lean4

/-- A nonzero monomorphism to a simple object is an isomorphism. -/
theorem isIso_of_mono_of_nonzero {X Y : C} [Simple Y] {f : X ⟶ Y} [Mono f] (w : f ≠ 0) : IsIso f :=
  (Simple.mono_isIso_iff_nonzero f).mpr w

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