English
The action of tensorHom on triple-graded objects respects the primed iota construction: composing ιTensorObj3' with tensorHom (f1,f2) and f3 is the same as tensorHom of f1,f2,f3 composed with ιTensorObj3'.
Русский
Действие tensorHom на тройно градуированных объектах сохраняет конструкцию ιTensorObj3′: композиция с tensorHom (f1,f2) и f3 равна композиции tensorHom(f1,f2,f3) с ιTensorObj3′.
LaTeX
$$$\iotaTensorObj_3' X_1 X_2 X_3 i_1 i_2 i_3 j h ≫ tensorHom (tensorHom f_1 f_2) f_3 j = ((f_1 i_1 ⊗_m f_2 i_2) ⊗_m f_3 i_3) ≫ \iotaTensorObj_3' Y_1 Y_2 Y_3 i_1 i_2 i_3 j h.$$$
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 f₁ (tensorHom 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, ←
id_tensorHom, ← id_tensorHom, MonoidalCategory.tensorHom_comp_tensorHom_assoc, ι_tensorHom,
MonoidalCategory.tensorHom_comp_tensorHom_assoc, id_comp, comp_id]
