English
Let DecidableEq α, Module R S, Module S M, and an IsScalarTower R S M. For w: α' → S, the linear combination over α × α' with weights w i.2 mapped to vectors v i.1 equals a composition of maps starting from the S-linear combination on v, restricting scalars to R, and applying mapRange to the linear combination of w, through the finsuppProdLEquiv R.
Русский
Пусть DecidableEq α, модули R и S, и т. д. Тогда линейная комбинация по парному индексу α × α' с весами w выражает собой композицию отображений: линейная комбинация над S для v, ограничение скалярами до R, применение линейного отображения от mapRange к линейной комбинации w через (finsuppProdLEquiv R).toLinearMap.
LaTeX
$$$\\operatorname{linearCombination}_R\\bigl(\\lambda i:(\\alpha \\times \\alpha') \\mapsto w(i).2 \\cdot v(i).1\\bigr) = (\\operatorname{restrictScalars}_R^S (\\operatorname{linearCombination}_S v)) \\circ\\!\n (\\operatorname{mapRange.linearMap}(\\operatorname{linearCombination}_R w)) \\circ (\\!(\\operatorname{finsuppProdLEquiv}_R).toLinearMap)$$$
Lean4
theorem linearCombination_smul [DecidableEq α] [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :
linearCombination R (fun i : α × α' ↦ w i.2 • v i.1) =
(linearCombination S v).restrictScalars R ∘ₗ
mapRange.linearMap (linearCombination R w) ∘ₗ (finsuppProdLEquiv R).toLinearMap :=
by ext; simp
