English
From presentations pres1 of M1 and pres2 of M2 one obtains a presentation for M1 ⊗A M2; the generators are those coming from the tensor of their generators and the relations come from combining the two presentations.
Русский
Из презентаций pres1 M1 и pres2 M2 строится презентация M1 ⊗A M2; порождающие соответствуют тензору их порождающих, а отношения получаются из объединения двух презентаций.
LaTeX
$$$$ \\text{Pres}_1 \\otimes \\text{Pres}_2 \\;\\text{presents } M_1 \\otimes_A M_2. $$$$
Lean4
/-- The presentation of the `A`-module `M₁ ⊗[A] M₂` that is deduced from
a presentation of `M₁` and a presentation of `M₂`. -/
@[simps!]
noncomputable def tensor : Presentation A (M₁ ⊗[A] M₂)
where
G := _
R := _
relation := _
toSolution := pres₁.toSolution.tensor pres₂.toSolution
toIsPresentation := pres₁.toIsPresentation.tensor pres₂.toIsPresentation
