English
From a family of solutions (one for each i), there is a canonical solution of the direct-sum relations in the direct sum module ⨁ i M_i, obtained by assembling the per-index solutions via the relevant injections into the direct sum.
Русский
Из семейства решений (по каждому i) существует каноническое решение системы прямой суммы в модуле прямой суммы ⨁ i M_i, получаемое объединением решений по индексам через вложения в прямую сумму.
LaTeX
$$$\\text{directSum}(\\text{solution}) \\in (Relations.directSum(relations)).Solution(\\bigoplus_i M_i)$$$
Lean4
/-- Given `solution : ∀ (i : ι), (relations i).Solution (M i)`, this is the
canonical solution of `Relations.directSum relations` in `⨁ i, M i`. -/
noncomputable def directSum (solution : ∀ (i : ι), (relations i).Solution (M i)) :
(Relations.directSum relations).Solution (⨁ i, M i) :=
directSumEquiv.symm (fun i ↦ (solution i).postcomp (lof A ι M i))
