balanced_of_strongMonoCategory — Mathlib

English

If the category is a StrongMonoCategory, then it is Balanced; i.e., mono plus epi implies isomorphism.

Русский

Если категория является StrongMonoCategory, то она Balanced; то есть моно и эпиморфизм вместе приводят к изоморфизму.

LaTeX

$$$\\forall f:\\, X \\to Y,\\ (\\mathrm{Mono}(f) \\land \\mathrm{Epi}(f)) \\Rightarrow \\mathrm{IsIso}(f).$$$

Lean4

instance (priority := 100) balanced_of_strongMonoCategory [StrongMonoCategory C] : Balanced C where
  isIso_of_mono_of_epi _ _ _ := isIso_of_epi_of_strongMono _

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