isIso_colimit_cocone_parallelPair_of_eq

English

If f = g, then the coequalizer projection π f g is an isomorphism (hence the coequalizer is essentially Y).

Русский

Если f = g, то проекция коэквалайзера π f g является изоморфизмом (коэквалайзер эквивалентен Y).

LaTeX

$$$ f = g \\Rightarrow \\mathrm{IsIso}(\\mathrm{coequalizer}.\\pi f g)$$$

Lean4

/-- Every coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem isIso_colimit_cocone_parallelPair_of_eq (h₀ : f = g) {c : Cofork f g} (h : IsColimit c) : IsIso c.π :=
  Iso.isIso_hom <| IsColimit.coconePointUniqueUpToIso (isColimitIdCofork h₀) h

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