English
Tensor products distribute over a product on the right: there exists a canonical linear equivalence M1 ⊗_R (M2 × M3) ≃ (M1 ⊗_R M2) × (M1 ⊗_R M3) over an appropriate base through an algebra S.
Русский
Тензорные произведения распространяются на правую долю над произведением: существует каноническое линейное эквивалентство M1 ⊗_R (M2 × M3) ≃ (M1 ⊗_R M2) × (M1 ⊗_R M3).
LaTeX
$$$M_1 \\otimes_R (M_2 \\times M_3) \\cong_S (M_1 \\otimes_R M_2) \\times (M_1 \\otimes_R M_3)$$$
Lean4
/-- Tensor products distribute over a product on the right. -/
def prodRight : M₁ ⊗[R] (M₂ × M₃) ≃ₗ[S] (M₁ ⊗[R] M₂) × (M₁ ⊗[R] M₃) :=
LinearEquiv.ofLinear
(TensorProduct.AlgebraTensorModule.lift <|
LinearMap.prodMapLinear R M₂ M₃ (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₃) S ∘ₗ
LinearMap.prod (AlgebraTensorModule.mk R S M₁ M₂) (AlgebraTensorModule.mk R S M₁ M₃))
(LinearMap.coprod (AlgebraTensorModule.lTensor _ _ <| LinearMap.inl _ _ _)
(AlgebraTensorModule.lTensor _ _ <| LinearMap.inr _ _ _))
(by ext <;> simp) (by ext <;> simp)
