coequalizer_ext — Mathlib

English

Let t be a PushoutCocone f g with ht a IsColimit. If two arrows k,l: t.pt ⟶ W agree after composing with inl t and inr t respectively, then k = l.

Русский

Пусть t — PushoutCocone f g, ht — IsColimit. Если два стрелы k,l: t.pt ⟶ W совпадают после композиции с inl t и inr t соответственно, то они равны.

LaTeX

$$k = l$$

Lean4

/-- To check whether a morphism is coequalized by the maps of a pushout cocone, it suffices to check
  it for `inl t` and `inr t` -/
theorem coequalizer_ext (t : PushoutCocone f g) {W : C} {k l : t.pt ⟶ W} (h₀ : inl t ≫ k = inl t ≫ l)
    (h₁ : inr t ≫ k = inr t ≫ l) : ∀ j : WalkingSpan, t.ι.app j ≫ k = t.ι.app j ≫ l
  | some WalkingPair.left => h₀
  | some WalkingPair.right => h₁
  | none => by rw [← t.w fst, Category.assoc, Category.assoc, h₀]

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