English
Let A be a commutative ring and (relations1, G1) and (relations2, G2) be systems of linear equations over A with generators G1, G2 and relations R1, R2. The tensor product of these systems has generators G1 × G2 and relations given by the two families: (R1 × G2) and (G1 × R2), embedded into the combined relation set by the natural left and right embedding maps.
Русский
Пусть A — коммутативное кольцо и даны две системы линейных уравнений с порождающими G1, G2 и отношениями R1, R2. Их тензорная композиция имеет порождающие G1 × G2 и отношения из двух семейств: (R1 × G2) и (G1 × R2), встроенные посредством естественных отображений вложения.
LaTeX
$$$$ \\mathcal{R}_{\\otimes} = (\\mathcal{R}_1 \\times \\mathcal{G}_2) \\;\\cup\\; (\\mathcal{G}_1 \\times \\mathcal{R}_2), \\quad \\text{with relations on } (g_1,g_2) \\mapsto \\text{emb}_L(\\cdot)(\\mathcal{r}_1) \\text{ or } \\text{emb}_R(\\cdot)(\\mathcal{r}_2). $$$$
Lean4
/-- The tensor product of systems of linear equations. -/
@[simps]
noncomputable def tensor : Relations A where
G := relations₁.G × relations₂.G
R := Sum (relations₁.R × relations₂.G) (relations₁.G × relations₂.R)
relation
| .inl ⟨r₁, g₂⟩ => Finsupp.embDomain (Function.Embedding.sectL relations₁.G g₂) (relations₁.relation r₁)
| .inr ⟨g₁, r₂⟩ => Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)
