hom_ext — Mathlib

English

Two maps out of the wide equalizer are equal if they agree after composing with the universal projection π f.

Русский

Две стрелки из широкого коэквалайзера равны, если согласны после составления с универсальной проекцией π f.

LaTeX

$$$\forall k,l : \mathrm{wideEqualizer} f \to W,\ (\mathrm{wideEqualizer.}\\pi f) \circ k = (\mathrm{wideEqualizer.}\\pi f) \circ l \Rightarrow k = l$$$

Lean4

/-- Two maps from a wide coequalizer are equal if they are equal when composed with the wide
    coequalizer map -/
@[ext]
theorem hom_ext [Nonempty J] {W : C} {k l : wideCoequalizer f ⟶ W}
    (h : wideCoequalizer.π f ≫ k = wideCoequalizer.π f ≫ l) : k = l :=
  Cotrident.IsColimit.hom_ext (colimit.isColimit _) h

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