isIso_of_mono_of_epi — Mathlib

English

In a Balanced category, an arrow f is an isomorphism if and only if it is both monic and epic.

Русский

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

LaTeX

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

Lean4

theorem isIso_of_mono_of_epi [Balanced C] {X Y : C} (f : X ⟶ Y) [Mono f] [Epi f] : IsIso f :=
  Balanced.isIso_of_mono_of_epi _

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