English
Let t be a PullbackCone for f: X → Z and g: Y → Z, and let k, l: W → t.pt be two arrows such that k ≫ fst t = l ≫ fst t and k ≫ snd t = l ≫ snd t. Then for every j in WalkingCospan, k ≫ t.π.app j = l ≫ t.π.app j.
Русский
Пусть t — пуллбэк-конус к f: X → Z и g: Y → Z. Пусть k, l: W → t.pt таковы, что k ∘ fst t = l ∘ fst t и k ∘ snd t = l ∘ snd t. Тогда для каждого j из WalkingCospan имеет k ∘ t.π.app j = l ∘ t.π.app j.
LaTeX
$$$k \\circ t.fst = l \\circ t.fst \quad\\text{и}\\quad k \\circ t.snd = l \\circ t.snd \\Rightarrow \\forall j:\\text{WalkingCospan},\\; k \\circ t.\\pi.app j = l \\circ t.\\pi.app j$$$
Lean4
/-- To check whether two morphisms are equalized by the maps of a pullback cone, it suffices to
check it for `fst t` and `snd t` -/
theorem equalizer_ext (t : PullbackCone f g) {W : C} {k l : W ⟶ t.pt} (h₀ : k ≫ fst t = l ≫ fst t)
(h₁ : k ≫ snd t = l ≫ snd t) : ∀ j : WalkingCospan, k ≫ t.π.app j = l ≫ t.π.app j
| some WalkingPair.left => h₀
| some WalkingPair.right => h₁
| none => by rw [← t.w inl, reassoc_of% h₀]
