English
In Over X, morphisms into a tensor object are determined by their composites with pullback projections. If two morphisms have equal composites with both fst and snd projections, they are equal.
Русский
В категории Over X морфизмы в тензорный объект определяются по композиторам с проекциями fst и snd; если две стрелки имеют одинаковые композиции с обеими проекциями, они равны.
LaTeX
$$$ \\forall R,S,T \\; (f_1,f_2 : R \\to (S \\otimes T)^{\\text{left}}),\\; f_1 \\circ \\mathrm{fst} = f_2 \\circ \\mathrm{fst} \\land f_1 \\circ \\mathrm{snd} = f_2 \\circ \\mathrm{snd} \\Rightarrow f_1 = f_2 $$$
Lean4
@[ext]
theorem tensorObj_ext {R : C} {S T : Over X} (f₁ f₂ : R ⟶ (S ⊗ T).left)
(e₁ : f₁ ≫ pullback.fst _ _ = f₂ ≫ pullback.fst _ _) (e₂ : f₁ ≫ pullback.snd _ _ = f₂ ≫ pullback.snd _ _) :
f₁ = f₂ :=
pullback.hom_ext e₁ e₂
