English
For graded objects X1,X2,Y1,Y2 with tensor products, and morphisms f : X1 → X2 and g : Y1 → Y2, the canonical map ιTensorObj intertwines with tensoring: composing ιTensorObj with tensorHom f g equals composing the tensor of components with ιTensorObj on the target side.
Русский
Для градуированных объектов X1,X2,Y1,Y2 с тензорными произведениями и морфизмами f : X1 → X2, g : Y1 → Y2 каноническое отображение ιTensorObj коммуникативно взаимодействует с тензоризацией: композиция ιTensorObj с tensorHom f g равна композиции tensorHom по компонентам с ιTensorObj на целевом объекте.
LaTeX
$$$\iotaTensorObj X_1 Y_1 i_1 i_2 i_{12} h \circ \tensorHom f g i_{12} = (f i_1 \otimes_\m g i_2) \circ \iotaTensorObj X_2 Y_2 i_1 i_2 i_{12} h.$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_tensorHom {X₁ X₂ Y₁ Y₂ : GradedObject I C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) [HasTensor X₁ Y₁] [HasTensor X₂ Y₂]
(i₁ i₂ i₁₂ : I) (h : i₁ + i₂ = i₁₂) :
ιTensorObj X₁ Y₁ i₁ i₂ i₁₂ h ≫ tensorHom f g i₁₂ = (f i₁ ⊗ₘ g i₂) ≫ ιTensorObj X₂ Y₂ i₁ i₂ i₁₂ h :=
by
rw [tensorHom_def, assoc]
apply ι_mapBifunctorMapMap
