hom_ext — Mathlib

English

Two arrows into an equalizer are equal if they agree after composing with the equalizer map: if k,l: W ⟶ equalizer f g and k ≫ equalizer.ι f g = l ≫ equalizer.ι f g, then k = l.

Русский

Две стрелки в равножку равны, если они совпадают после композиции с равножкой: если k,l: W ⟶ equalizer f g и k ≫ equalizer.ι f g = l ≫ equalizer.ι f g, то k = l.

LaTeX

$$$\forall W\,k,l:\, W \to \mathrm{equalizer}(f,g),\ k \circ \mathrm{equalizer.}\iota f g = l \circ \mathrm{equalizer.}\iota f g \Rightarrow k = l$$$

Lean4

/-- Two maps into an equalizer are equal if they are equal when composed with the equalizer map. -/
@[ext]
theorem hom_ext {W : C} {k l : W ⟶ equalizer f g} (h : k ≫ equalizer.ι f g = l ≫ equalizer.ι f g) : k = l :=
  Fork.IsLimit.hom_ext (limit.isLimit _) h

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