English
Morphisms out of a tensor object are determined by their precomposition with the left and right injections; equality after those precompositions implies equality of the morphisms.
Русский
Гомоморфизмы из тензорного объекта задаются через предварительное композиционирование с левым и правым включениями; равенство после таких предварительных композиции означает равенство гомоморфизмов.
LaTeX
$$$\\forall x,y,z,\\ f,g:\\,x\\otimes y\\to z,\\ h_1:\\,inl\\_\\_\\to f = inl\\_\\_\\to g,\\ h_2:\\,inr\\_\\_\\to f = inr\\_\\_\\to g\\;\\Rightarrow\\; f=g.$$$
Lean4
/-- We can characterize morphisms out of a tensor product via their precomposition with `inl` and
`inr`. -/
@[ext]
theorem tensorObj_hom_ext {x y z : AugmentedSimplexCategory} (f g : x ⊗ y ⟶ z) (h₁ : inl _ _ ≫ f = inl _ _ ≫ g)
(h₂ : inr _ _ ≫ f = inr _ _ ≫ g) : f = g :=
match x, y, z, f, g with
| .of x, .of y, .of z, f, g => by
change (tensorObjOf x y) ⟶ z at f g
change inl' _ _ ≫ f = inl' _ _ ≫ g at h₁
change inr' _ _ ≫ f = inr' _ _ ≫ g at h₂
ext i
let j : Fin ((x.len + 1) + (y.len + 1)) := i.cast (Nat.succ_add x.len (y.len + 1)).symm
have : i = j.cast (Nat.succ_add x.len (y.len + 1)) := rfl
rw [this]
cases j using Fin.addCases (m := x.len + 1) (n := y.len + 1) with
| left j =>
rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₁
simpa [← inl'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₁ j
| right j =>
rw [SimplexCategory.Hom.ext_iff, OrderHom.ext_iff] at h₂
simpa [← inr'_eval, ConcreteCategory.hom, Fin.ext_iff] using congrFun h₂ j
| .of x, .star, .of z, f, g =>
by
simp only [inl, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self, whiskerLeft_id_star] at h₁
simpa [Category.id_comp f, Category.id_comp g] using h₁
| .star, .of y, .of z, f, g =>
by
simp only [inr, Category.assoc, Iso.cancel_iso_inv_left, Limits.IsInitial.to_self, id_star_whiskerRight] at h₂
simpa [Category.id_comp f, Category.id_comp g] using h₂
| .star, .star, .of z, f, g => rfl
| .star, .star, .star, f, g => rfl
