epi_of_isColimit_cofork — Mathlib

English

The coequalizer map from a colimit cocone is an epimorphism: c.π is epi for any colimit cocone c.

Русский

Коэквалайзерная стрелка в любом колимитном коконе является эпиморфизмом: c.π — эпиморфизм.

LaTeX

$$$ \\mathrm{Epi}(c.\\pi)$$$

Lean4

/-- The coequalizer morphism in any colimit cocone is an epimorphism. -/
theorem epi_of_isColimit_cofork {c : Cofork f g} (i : IsColimit c) : Epi c.π :=
  { left_cancellation := fun _ _ w => Cofork.IsColimit.hom_ext i w }

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