hom_ext — Mathlib

English

A pair of arrows out of a pushout are equal whenever their compositions with the two pushout injections are equal.

Русский

Пусть два отображения из пуш-аута равны, если их композиции с двумя инъекциями пушаута равны друг другу.

LaTeX

$$$\forall k,l:\; \mathrm{inl}\ f g ≫ k = \mathrm{inl}\ f g ≫ l \Rightarrow \mathrm{inr}\ f g ≫ k = \mathrm{inr}\ f g ≫ l \Rightarrow k=l$$$

Lean4

/-- Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are
equal -/
@[ext 1100]
theorem hom_ext {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} [HasPushout f g] {W : C} {k l : pushout f g ⟶ W}
    (h₀ : pushout.inl _ _ ≫ k = pushout.inl _ _ ≫ l) (h₁ : pushout.inr _ _ ≫ k = pushout.inr _ _ ≫ l) : k = l :=
  colimit.hom_ext <| PushoutCocone.coequalizer_ext _ h₀ h₁

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