English
There is a natural equivalence between the data of a solution of the direct-sum relations in N and the family of solutions of each relation i in N. In other words, giving a solution to the direct-sum system is the same as giving, for every index i, a solution to the i-th relation in N.
Русский
Существует естественное эквивалентное соответствие между данными решения системы прямой суммы отношений в N и семейством решений для каждой i‑й отношения в N. Другими словами, задание решения системы прямой суммы эквивалентно выбору для каждого индекса i решения соответствующего отношения в N.
LaTeX
$$$\\ (Relations.directSum(relations)).Solution\\,N\\; \\cong\\; \\forall i, (relations\\,i).Solution\\,N\\,$$$
Lean4
/-- Given an `A`-module `N` and a family `relations : ι → Relations A`,
the data of a solution of `Relations.directSum relations` in `N`
is equivalent to the data of a family of solutions of `relations i` in `N`
for all `i`. -/
@[simps]
noncomputable def directSumEquiv : (Relations.directSum relations).Solution N ≃ ∀ i, (relations i).Solution N
where
toFun s
i :=
{ var := fun g ↦ s.var ⟨i, g⟩
linearCombination_var_relation := fun r ↦
by
rw [← s.linearCombination_var_relation ⟨i, r⟩]
symm
apply Finsupp.linearCombination_embDomain }
invFun
t :=
{ var := fun ⟨i, g⟩ ↦ (t i).var g
linearCombination_var_relation := fun ⟨i, r⟩ ↦
by
rw [← (t i).linearCombination_var_relation r]
apply Finsupp.linearCombination_embDomain }
