isIso_iff_mono_and_epi — Mathlib

English

In a Balanced category, an arrow f is an isomorphism if and only if it is mono and epi; this equivalence characterizes isomorphisms.

Русский

В сбалансированной категории стрелка f является изоморфизмом тогда и только тогда, когда она моно и эпиморфна; это эквивалентность характеризует изоморфизмы.

LaTeX

$$$$ \text{IsIso}(f) \iff (\text{Mono}(f) \wedge \text{Epi}(f)). $$$$

Lean4

theorem isIso_iff_mono_and_epi [Balanced C] {X Y : C} (f : X ⟶ Y) : IsIso f ↔ Mono f ∧ Epi f :=
  ⟨fun _ => ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ => isIso_of_mono_of_epi _⟩

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