eq_of_mono_coequalizer — Mathlib

English

If HasCoequalizer f g and coequalizer.π f g is mono, then f = g.

Русский

Если существуют коэквалайзер f g и проекция коэквалайзера моно, то f = g.

LaTeX

$$$ [HasCoequalizer f g] [Mono (\\mathrm{coequalizer}.\\pi f g)] \\Rightarrow f = g$$$

Lean4

/-- If the coequalizer of two morphisms is a monomorphism, then the two morphisms are equal. -/
theorem eq_of_mono_coequalizer [HasCoequalizer f g] [Mono (coequalizer.π f g)] : f = g :=
  (cancel_mono (coequalizer.π f g)).1 <| coequalizer.condition _ _

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