hom_ext — Mathlib

English

Let t be a PullbackCone for f: X → Z and g: Y → Z, and ht an IsLimit t. Then for any W and arrows k, l: W → t.pt, if k ≫ fst t = l ≫ fst t and k ≫ snd t = l ≫ snd t, then k = l.

Русский

Пусть t — пуллбэк-конус к f: X → Z и g: Y → Z, и ht — IsLimit(t). Тогда для любых W и стрел k, l: W ⟶ t.pt, если k; fst t = l; fst t и k; snd t = l; snd t, то k = l.

LaTeX

$$$k = l$ при $k \\circ t.fst = l \\circ t.fst$ и $k \\circ t.snd = l \\circ t.snd$$$

Lean4

theorem hom_ext {t : PullbackCone f g} (ht : IsLimit t) {W : C} {k l : W ⟶ t.pt} (h₀ : k ≫ fst t = l ≫ fst t)
    (h₁ : k ≫ snd t = l ≫ snd t) : k = l :=
  ht.hom_ext <| equalizer_ext _ h₀ h₁

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