equalizer_ext — Mathlib

English

If s is a limit fork, any two arrows k,l: W → s.pt with k ≫ Fork.ι s = l ≫ Fork.ι s are equal.

Русский

Если s — предельный форк, то любые стрелки k,l: W → s.pt с k ≫ Fork.ι s = l ≫ Fork.ι s равны.

LaTeX

$$hs.hom_ext (Fork.equalizer_ext _ h)$$

Lean4

/-- To check whether two maps are equalized by both maps of a fork, it suffices to check it for the
first map -/
theorem equalizer_ext (s : Fork f g) {W : C} {k l : W ⟶ s.pt} (h : k ≫ s.ι = l ≫ s.ι) :
    ∀ j : WalkingParallelPair, k ≫ s.π.app j = l ≫ s.π.app j
  | zero => h
  | one => by
    have : k ≫ ι s ≫ f = l ≫ ι s ≫ f := by simp only [← Category.assoc]; exact congrArg (· ≫ f) h
    rw [s.app_one_eq_ι_comp_left, this]

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