English
An extensionality principle for the three-fold tensor object: if two morphisms agree after composing with all iota projections ιTensorObj3, then they are equal.
Русский
Принцип экстенсивности для тройного тензорного объекта: если две морфизмы совпадают после композиции с всеми проекциями iotaTensorObj3, то они равны.
LaTeX
$$$\text{If } f,g: ιTensorObj_3 X_1 X_2 X_3 j \to A \text{ satisfy } \forall i_1,i_2,i_3, hi, ιTensorObj_3 X_1 X_2 X_3 i_1 i_2 i_3 j hi ≫ f = ιTensorObj_3 X_1 X_2 X_3 i_1 i_2 i_3 j hi ≫ g, \text{ then } f=g.$$$
Lean4
@[reassoc (attr := simp)]
theorem ιTensorObj₃'_tensorHom (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j) :
ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ tensorHom (tensorHom f₁ f₂) f₃ j =
((f₁ i₁ ⊗ₘ f₂ i₂) ⊗ₘ f₃ i₃) ≫ ιTensorObj₃' Y₁ Y₂ Y₃ i₁ i₂ i₃ j h :=
by
rw [ιTensorObj₃'_eq _ _ _ i₁ i₂ i₃ j h _ rfl, ιTensorObj₃'_eq _ _ _ i₁ i₂ i₃ j h _ rfl, assoc, ι_tensorHom, ←
tensorHom_id, ← tensorHom_id, MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, ι_tensorHom,
MonoidalCategory.tensorHom_comp_tensorHom_assoc, comp_id]
