isIso_of_mono_of_strongEpi — Mathlib

English

If f is mono and strong epi, then f is an isomorphism.

Русский

Если стрелка моно и сильная эпиморфизм, то она является изоморфизмом.

LaTeX

$$$\\forall f:\\, P \\to Q,\\ [\\mathrm{Mono}(f)]\\land [\\mathrm{StrongEpi}(f)]\\Rightarrow \\mathrm{IsIso}(f).$$$

Lean4

/-- A strong epimorphism that is a monomorphism is an isomorphism. -/
theorem isIso_of_mono_of_strongEpi (f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f :=
  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by simp⟩⟩

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