coequalizer_ext — Mathlib

English

If s is a colimit cofork, any two arrows k,l: s.pt → W with Cofork.π s ≫ k = Cofork.π s ≫ l are equal.

Русский

Если s — коколимитный кофорк, стрелки k,l: s.pt → W равны при условии Cofork.π s ≫ k = Cofork.π s ≫ l.

LaTeX

$$hs.hom_ext (Cofork.coequalizer_ext _ h)$$

Lean4

/-- To check whether two maps are coequalized by both maps of a cofork, it suffices to check it for
the second map -/
theorem coequalizer_ext (s : Cofork f g) {W : C} {k l : s.pt ⟶ W} (h : Cofork.π s ≫ k = Cofork.π s ≫ l) :
    ∀ j : WalkingParallelPair, s.ι.app j ≫ k = s.ι.app j ≫ l
  | zero => by simp only [s.app_zero_eq_comp_π_left, Category.assoc, h]
  | one => h

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