isIso_of_epi_of_isSplitMono — Mathlib

English

Let f: X → Y be a morphism in a category which is both a split mono and epi. Then f is an isomorphism; equivalently there exists a morphism g: Y → X with f ∘ g = id_Y and g ∘ f = id_X.

Русский

Пусть f: X → Y — морфизм в категории, который является разложимым моно и эпиморфизмом. Тогда f является изоморфизмом; то есть существует g: Y → X such that f ∘ g = id_Y и g ∘ f = id_X.

LaTeX

$$$\exists g: Y \to X\;\big(\;f \circ g = \mathrm{id}_Y \land g \circ f = \mathrm{id}_X\;\) .$$$

Lean4

/-- A split mono which is epi is an iso. -/
theorem isIso_of_epi_of_isSplitMono {X Y : C} (f : X ⟶ Y) [IsSplitMono f] [Epi f] : IsIso f :=
  ⟨⟨retraction f, ⟨by simp, by simp [← cancel_epi f]⟩⟩⟩

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