hom_ext — Mathlib

English

Dually, morphisms out of a binary coproduct are determined by their two coordinate maps; equality of compositions with inl and inr implies equality.

Русский

Дуально: морфизмы из двоечного копроизведения определяются двумя координатами; равенство композиция с inl и inr дает равенство морфизмов.

LaTeX

$$$$ \forall \{f,g: X \uplus Y \to W\},\ coprod.inl \circ f = coprod.inl \circ g \land coprod.inr \circ f = coprod.inr \circ g \Rightarrow f=g. $$$$

Lean4

@[ext 1100]
theorem hom_ext {W X Y : C} [HasBinaryCoproduct X Y] {f g : X ⨿ Y ⟶ W} (h₁ : coprod.inl ≫ f = coprod.inl ≫ g)
    (h₂ : coprod.inr ≫ f = coprod.inr ≫ g) : f = g :=
  BinaryCofan.IsColimit.hom_ext (colimit.isColimit _) h₁ h₂

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