hom_ext — Mathlib

English

If two arrows into the multiequalizer agree after composing with all π I b, then they are equal.

Русский

Если два отображения в multiequalizer дают одинаковые композиции с каждым π I b, то они равны.

LaTeX

$$$\forall i,j:\, (\text{multiequalizer } I \to W),\ (\forall b,\; (\text{Multiequalizer.π } I b) \circ i = (\text{Multiequalizer.π } I b) \circ j) \Rightarrow i=j$$$

Lean4

@[ext]
theorem hom_ext {W : C} (i j : multicoequalizer I ⟶ W)
    (h : ∀ b, Multicoequalizer.π I b ≫ i = Multicoequalizer.π I b ≫ j) : i = j :=
  colimit.hom_ext
    (by
      rintro (a | b)
      · simp_rw [← colimit.w I.multispan (WalkingMultispan.Hom.fst a), Category.assoc, h]
      · apply h)

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