isIso_of_epi_of_nonzero — Mathlib

English

A nonzero epimorphism from a simple X is an isomorphism.

Русский

Ненулевой эпиморфизм из простого X является изоморфизмом.

LaTeX

$$$ \forall X Y, [Simple X], {f: X \to Y} [Epi f] (w: f \neq 0) \Rightarrow IsIso f. $$$

Lean4

/-- A nonzero epimorphism from a simple object is an isomorphism. -/
theorem isIso_of_epi_of_nonzero {X Y : C} [Simple X] {f : X ⟶ Y} [Epi f] (w : f ≠ 0) : IsIso f :=
  -- `f ≠ 0` means that `kernel.ι f` is not an iso, and hence zero, and hence `f` is a mono.

  haveI : Mono f := Preadditive.mono_of_kernel_zero (mono_to_simple_zero_of_not_iso (kernel_not_iso_of_nonzero w))
  isIso_of_mono_of_epi f

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