English
Define a canonical coproduct map: from the coproduct space to N by summing the images of each component after applying f_i to x_i, intertwined with mapRange.
Русский
Определяем каноническое отображение копродукта: сумма образов каждого компонента после применения f_i к x_i через mapRange.
LaTeX
$$$\\mathrm{coprodMap}\\; f := (\\mathrm{DFinsupp.lsum}\\; \\mathbb{N} \\; (\\lambda i, \\mathrm{id}) ) \\circ_\\ell \\mathrm{DFinsupp.mapRange.linearMap}\\; f$$$
Lean4
/-- Given a family of linear maps `f i : M i →ₗ[R] N`, we can form a linear map
`(Π₀ i, M i) →ₗ[R] N` which sends `x : Π₀ i, M i` to the sum over `i` of `f i` applied to `x i`.
This is the map coming from the universal property of `Π₀ i, M i` as the coproduct of the `M i`.
See also `LinearMap.coprod` for the binary product version. -/
def coprodMap (f : ∀ i : ι, M i →ₗ[R] N) : (Π₀ i, M i) →ₗ[R] N :=
(DFinsupp.lsum ℕ fun _ : ι => LinearMap.id) ∘ₗ DFinsupp.mapRange.linearMap f
