English
On a pure tensor DirectSumLeft acts by sending DirectSum.lof i x ⊗ y to DirectSum.lof i (x ⊗ y).
Русский
На чистом тензоре DirectSumLeft действует так, что DirectSum.lof i x ⊗ y отображается в DirectSum.lof i (x ⊗ y).
LaTeX
$$$$ \\mathrm{TensorProduct.directSumLeft}\\, R\\, M_1\\, M_2'\\ (\\mathrm{DirectSum.lof}\\ R\\ ι_1\\ M_1\\ i\\ x \\otimes_R y) = \\mathrm{DirectSum.lof}\\ R\\ ι_1\\ (fun i \\mapsto M_1 i)\\ i\\ (x \\otimes_R y). $$$$
Lean4
/-- Tensor products distribute over a direct sum on the left . -/
def directSumLeft : (⨁ i₁, M₁ i₁) ⊗[R] M₂' ≃ₗ[R] ⨁ i, M₁ i ⊗[R] M₂' :=
LinearEquiv.ofLinear
(lift <| DirectSum.toModule R _ _ fun _ => (mk R _ _).compr₂ <| DirectSum.lof R ι₁ (fun i => M₁ i ⊗[R] M₂') _)
(DirectSum.toModule R _ _ fun _ => rTensor _ (DirectSum.lof R ι₁ _ _))
(DirectSum.linearMap_ext R fun i =>
TensorProduct.ext <|
LinearMap.ext₂ fun m₁ m₂ =>
by
dsimp only [comp_apply, compr₂_apply, id_apply, mk_apply]
simp_rw [DirectSum.toModule_lof, rTensor_tmul, lift.tmul, DirectSum.toModule_lof, compr₂_apply, mk_apply])
(TensorProduct.ext <|
DirectSum.linearMap_ext R fun i =>
LinearMap.ext₂ fun m₁ m₂ =>
by
dsimp only [comp_apply, compr₂_apply, id_apply, mk_apply]
simp_rw [lift.tmul, DirectSum.toModule_lof, compr₂_apply, mk_apply, DirectSum.toModule_lof, rTensor_tmul])
