isIso_limit_cocone_parallelPair_of_epi

English

If a coequalizer projection c.π is mono, then it is an isomorphism: a mono coequalizer map is invertible.

Русский

Если проекция коэквалайзера c.π моно, то она является изоморфизмом: моно-коэквалайзеровская стрелка обратима.

LaTeX

$$$ \\text{If } [Mono\\, c.\\pi] \\Rightarrow \\mathrm{IsIso}(c.\\pi)$$$

Lean4

/-- A coequalizer that is a monomorphism is an isomorphism. -/
theorem isIso_limit_cocone_parallelPair_of_epi {c : Cofork f g} (h : IsColimit c) [Mono c.π] : IsIso c.π :=
  isIso_colimit_cocone_parallelPair_of_eq ((cancel_mono _).1 (Cofork.condition c)) h

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