English
The linear sum lsum expresses a linear equivalence between families of linear maps and linear maps out of the product.
Русский
Линейная сумма lsum задаёт линейное эквивалентное отображение между семействами линейных отображений и линейными отображениями из произведения.
LaTeX
$$$\\text{lsum}: ((i\\in \\iota)\\ φ_i \\to_ℓ[R] M) \\simeq ((i\\in \\iota) φ_i) \\to_ℓ[R] M.$$$
Lean4
/-- The linear equivalence between linear functions on a finite product of modules and
families of functions on these modules. See note [bundled maps over different rings]. -/
@[simps symm_apply]
def lsum (S) [AddCommMonoid M] [Module R M] [Fintype ι] [Semiring S] [Module S M] [SMulCommClass R S M] :
((i : ι) → φ i →ₗ[R] M) ≃ₗ[S] ((i : ι) → φ i) →ₗ[R] M
where
toFun f := ∑ i : ι, (f i).comp (proj i)
invFun f i := f.comp (single R φ i)
map_add' f g := by simp only [Pi.add_apply, add_comp, Finset.sum_add_distrib]
map_smul' c f := by simp only [Pi.smul_apply, smul_comp, Finset.smul_sum, RingHom.id_apply]
left_inv
f := by
ext i x
simp [apply_single]
right_inv
f := by
ext x
suffices f (∑ j, Pi.single j (x j)) = f x by simpa [apply_single]
rw [Finset.univ_sum_single]
