English
Let X1, Y1, Z1, X2, Y2, Z2 be R-modules and f1: X1 → Y1, f2: X2 → Y2, g1: Y1 → Z1, g2: Y2 → Z2. Then the tensor product of morphisms is compatible with composition, i.e. (f1 ⊗ f2) ≫ (g1 ⊗ g2) = (f1 ≫ g1) ⊗ (f2 ≫ g2).
Русский
Пусть X1, Y1, Z1, X2, Y2, Z2 — модули над кольцом R; f1: X1 → Y1, f2: X2 → Y2, g1: Y1 → Z1, g2: Y2 → Z2. Тогда тензорное произведение отображений удовлетворяет композиционной совместимости: (f1 ⊗ f2) ≫ (g1 ⊗ g2) = (f1 ≫ g1) ⊗ (f2 ≫ g2).
LaTeX
$$$ (f_1 \\otimes f_2) \\; \\gg\\; (g_1 \\otimes g_2) = (f_1 \\gg g_1) \\otimes (f_2 \\gg g_2) $$$
Lean4
theorem tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁)
(g₂ : Y₂ ⟶ Z₂) : tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ = tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) :=
by
ext : 1
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): even with high priority `ext` fails to find this.
apply TensorProduct.ext
rfl
