Presentation of the tensor product of two modules

Given presentations of two A-modules M₁ and M₂, we obtain a presentation of M₁ ⊗[A] M₂.

noncomputable def Module.Relations.tensor {A : Type u} [CommRing A] (relations₁ : Relations A) (relations₂ : Relations A) : Relations A

The tensor product of systems of linear equations.

@[simp]

theorem Module.Relations.tensor_R {A : Type u} [CommRing A] (relations₁ : Relations A) (relations₂ : Relations A) : (relations₁.tensor relations₂).R = (relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R)

@[simp]

theorem Module.Relations.tensor_G {A : Type u} [CommRing A] (relations₁ : Relations A) (relations₂ : Relations A) : (relations₁.tensor relations₂).G = (relations₁.G × relations₂.G)

@[simp]

theorem Module.Relations.tensor_relation {A : Type u} [CommRing A] (relations₁ : Relations A) (relations₂ : Relations A) (x✝ : relations₁.R × relations₂.G ⊕ relations₁.G × relations₂.R) : (relations₁.tensor relations₂).relation x✝ = match x✝ with | Sum.inl (r₁, g₂) => Finsupp.embDomain (Function.Embedding.sectL relations₁.G g₂) (relations₁.relation r₁) | Sum.inr (g₁, r₂) => Finsupp.embDomain (Function.Embedding.sectR g₁ relations₂.G) (relations₂.relation r₂)

noncomputable def Module.Relations.Solution.tensor {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Relations A} {relations₂ : Relations A} (solution₁ : relations₁.Solution M₁) (solution₂ : relations₂.Solution M₂) : (relations₁.tensor relations₂).Solution (TensorProduct A M₁ M₂)

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₂.

@[simp]

theorem Module.Relations.Solution.tensor_var {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Relations A} {relations₂ : Relations A} (solution₁ : relations₁.Solution M₁) (solution₂ : relations₂.Solution M₂) (x✝ : (relations₁.tensor relations₂).G) : (solution₁.tensor solution₂).var x✝ = match x✝ with | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂

noncomputable def Module.Relations.Solution.isPresentationCoreTensor {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Relations A} {relations₂ : Relations A} {solution₁ : relations₁.Solution M₁} {solution₂ : relations₂.Solution M₂} (h₁ : solution₁.IsPresentation) (h₂ : solution₂.IsPresentation) : (solution₁.tensor solution₂).IsPresentationCore

The tensor product of two modules admits a presentation by generators and relations.

theorem Module.Relations.Solution.IsPresentation.tensor {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] {relations₁ : Relations A} {relations₂ : Relations A} {solution₁ : relations₁.Solution M₁} {solution₂ : relations₂.Solution M₂} (h₁ : solution₁.IsPresentation) (h₂ : solution₂.IsPresentation) : (solution₁.tensor solution₂).IsPresentation

noncomputable def Module.Presentation.tensor {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Presentation A M₁) (pres₂ : Presentation A M₂) : Presentation A (TensorProduct A M₁ M₂)

The presentation of the A-module M₁ ⊗[A] M₂ that is deduced from a presentation of M₁ and a presentation of M₂.

@[simp]

theorem Module.Presentation.tensor_relation {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Presentation A M₁) (pres₂ : Presentation A M₂) (x✝ : pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R) : (pres₁.tensor pres₂).relation x✝ = match x✝ with | Sum.inl (r₁, g₂) => Finsupp.embDomain (Function.Embedding.sectL pres₁.G g₂) (pres₁.relation r₁) | Sum.inr (g₁, r₂) => Finsupp.embDomain (Function.Embedding.sectR g₁ pres₂.G) (pres₂.relation r₂)

@[simp]

theorem Module.Presentation.tensor_var {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Presentation A M₁) (pres₂ : Presentation A M₂) (x✝ : (pres₁.tensor pres₂.toRelations).G) : (pres₁.tensor pres₂).var x✝ = match x✝ with | (g₁, g₂) => pres₁.var g₁ ⊗ₜ[A] pres₂.var g₂

@[simp]

theorem Module.Presentation.tensor_R {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Presentation A M₁) (pres₂ : Presentation A M₂) : (pres₁.tensor pres₂).R = (pres₁.R × pres₂.G ⊕ pres₁.G × pres₂.R)

@[simp]

theorem Module.Presentation.tensor_G {A : Type u} [CommRing A] {M₁ : Type v₁} {M₂ : Type v₂} [AddCommGroup M₁] [AddCommGroup M₂] [Module A M₁] [Module A M₂] (pres₁ : Presentation A M₁) (pres₂ : Presentation A M₂) : (pres₁.tensor pres₂).G = (pres₁.G × pres₂.G)