tensor_ext — Mathlib

English

If f and g are morphisms X ⟶ Y ⊗ Z and their compositions with the canonical projections fst and snd agree, then f = g.

Русский

Если два морфизма X ⟶ Y ⊗ Z согласованы по проекциям fst и snd, то они равны.

LaTeX

$$$f \circ \mathrm{prod}.\mathrm{fst} = g \circ \mathrm{prod}.\mathrm{fst} \land f \circ \mathrm{prod}.\mathrm{snd} = g \circ \mathrm{prod}.\mathrm{snd} \Rightarrow f = g$$$

Lean4

@[ext]
theorem tensor_ext {X Y Z : C} (f g : X ⟶ Y ⊗ Z) (w₁ : f ≫ prod.fst = g ≫ prod.fst) (w₂ : f ≫ prod.snd = g ≫ prod.snd) :
    f = g :=
  Limits.prod.hom_ext w₁ w₂

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