π_of_eq — Mathlib

English

If f = g, the coequalizer projection π f g is an isomorphism.

Русский

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

LaTeX

$$$ \\text{If } f = g: \\; \\mathrm{IsIso}(\\mathrm{coequalizer}.\\pi f g)$$$

Lean4

/-- The coequalizer of `(f, g)`, where `f = g`, is an isomorphism. -/
theorem π_of_eq [HasCoequalizer f g] (h : f = g) : IsIso (coequalizer.π f g) :=
  isIso_colimit_cocone_parallelPair_of_eq h <| colimit.isColimit _

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