English
Given solutions in M1 and M2 to their respective systems of linear equations, one obtains a natural solution to the tensor product system in M1 ⊗A M2 by taking the tensor product of the individual solutions: var⟨g1,g2⟩ = var1(g1) ⊗ var2(g2), and this construction respects the linear-combination relations.
Русский
Даны решения в M1 и M2 их соответствующих систем линейных уравнений; тогда естественным образом получается решение для системы тензорного произведения в M1 ⊗A M2: var⟨g1,g2⟩ = var1(g1) ⊗ var2(g2), и эта конструкция сохраняет линейные соотношения.
LaTeX
$$$$ \\text{If } s_1 \\text{ is a solution for } \\mathcal{R}_1 \\text{ on } M_1 \\text{ and } s_2 \\text{ is a solution for } \\mathcal{R}_2 \\text{ on } M_2, \\\\ \n \\text{then } s: (\\mathcal{R}_1 \\otimes \\mathcal{R}_2).\\mathrm{Solution}(M_1 \\otimes_A M_2) \\\\ \n \\text{is given by } s(\\langle g_1,g_2\\rangle) = s_1(g_1) \\otimes s_2(g_2). $$$$
Lean4
/-- Given solutions in `M₁` and `M₂` to systems of linear equations, this is the obvious
solution to the tensor product of these systems in `M₁ ⊗[A] M₂`. -/
@[simps]
noncomputable def tensor : (relations₁.tensor relations₂).Solution (M₁ ⊗[A] M₂)
where
var := fun ⟨g₁, g₂⟩ => solution₁.var g₁ ⊗ₜ solution₂.var g₂
linearCombination_var_relation := by
rintro (⟨r₁, g₂⟩ | ⟨g₁, r₂⟩)
· dsimp
rw [Finsupp.linearCombination_embDomain]
exact
(solution₁.postcomp
(curry (TensorProduct.comm A M₂ M₁).toLinearMap (solution₂.var g₂))).linearCombination_var_relation
r₁
· dsimp
rw [Finsupp.linearCombination_embDomain]
exact (solution₂.postcomp (curry .id (solution₁.var g₁))).linearCombination_var_relation r₂
