English
The tensor product of two presented modules can be presented; i.e., the tensor product of two presentations yields a presentation core for the tensor product module.
Русский
Тензорное произведение двух представленных модулей можно представить; то есть тензорное произведение двух презентаций образует презентацию модуля-tensor.
LaTeX
$$$$ \\text{If } (M_1, \\mathcal{R}_1) \\text{ and } (M_2, \\mathcal{R}_2) \\text{ are presentations, then } M_1 \\otimes_A M_2 \\text{ has a presentation given by } \\mathcal{R}_1 \\otimes \\mathcal{R}_2. $$$$
Lean4
/-- The tensor product of two modules admits a presentation by generators and relations. -/
noncomputable def isPresentationCoreTensor : Solution.IsPresentationCore.{w} (solution₁.tensor solution₂)
where
desc
s :=
uncurry _ _ _ _
(h₁.desc
{ var := fun g₁ ↦
h₂.desc
{ var := fun g₂ ↦ s.var ⟨g₁, g₂⟩
linearCombination_var_relation := fun r₂ ↦
by
erw [← Finsupp.linearCombination_embDomain A (Function.Embedding.sectR g₁ relations₂.G)]
exact s.linearCombination_var_relation (.inr ⟨g₁, r₂⟩) }
linearCombination_var_relation := fun r₁ ↦
h₂.postcomp_injective
(by
ext g₂
dsimp
erw [Finsupp.apply_linearCombination A (LinearMap.applyₗ (solution₂.var g₂))]
have := s.linearCombination_var_relation (.inl ⟨r₁, g₂⟩)
erw [Finsupp.linearCombination_embDomain] at this
convert this
ext g₁
simp) })
postcomp_desc _ := by aesop
postcomp_injective
h :=
curry_injective
(h₁.postcomp_injective
(by
ext g₁ : 2
refine h₂.postcomp_injective ?_
ext g₂
exact congr_var h ⟨g₁, g₂⟩))
