isIso_of_mono_of_isSplitEpi — Mathlib

English

A morphism that is both split mono and epi is an isomorphism.

Русский

Моризм, который одновременно является разложимым моно и эпиморфизмом, является изоморфизмом.

LaTeX

$$$ \\text{IsIso}(f) \\quad\\text{if } f \\text{ isSplitMono and epi}$$$

Lean4

/-- A split epi which is mono is an iso. -/
theorem isIso_of_mono_of_isSplitEpi {X Y : C} (f : X ⟶ Y) [Mono f] [IsSplitEpi f] : IsIso f :=
  ⟨⟨section_ f, ⟨by simp [← cancel_mono f], by simp⟩⟩⟩

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