hom_ext — Mathlib

English

Two morphisms out of a pushout are equal if their compositions with both pushout injections are equal.

Русский

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

LaTeX

$$$\forall k,l:\; \mathrm{pushout}\ f\ g \to W,\; k\circ \mathrm{inl} = l\circ \mathrm{inl}\;\land\; k\circ \mathrm{inr} = l\circ \mathrm{inr} \Rightarrow k=l$$$

Lean4

/-- Two morphisms into a pullback are equal if their compositions with the pullback morphisms are
equal -/
@[ext 1100]
theorem hom_ext {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] {W : C} {k l : W ⟶ pullback f g}
    (h₀ : k ≫ pullback.fst f g = l ≫ pullback.fst f g) (h₁ : k ≫ pullback.snd f g = l ≫ pullback.snd f g) : k = l :=
  limit.hom_ext <| PullbackCone.equalizer_ext _ h₀ h₁

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