hom_ext — Mathlib

English

Morphisms into a binary product are determined by their two coordinate maps; equality of their compositions with fst and snd implies equality.

Русский

Морфизмы в произведение определяются двумя координатами; равенство композиций с fst и snd дает равенство морфизмов.

LaTeX

$$$$ \forall \{f,g: W \to X \times Y\},\ f \circ \text{prod.fst} = g \circ \text{prod.fst} \land f \circ \text{prod.snd} = g \circ \text{prod.snd} \Rightarrow f=g. $$$$

Lean4

@[ext 1100]
theorem hom_ext {W X Y : C} [HasBinaryProduct X Y] {f g : W ⟶ X ⨯ Y} (h₁ : f ≫ prod.fst = g ≫ prod.fst)
    (h₂ : f ≫ prod.snd = g ≫ prod.snd) : f = g :=
  BinaryFan.IsLimit.hom_ext (limit.isLimit _) h₁ h₂

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