Documentation

Mathlib.Algebra.Module.Presentation.Tensor

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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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)
    source
    @[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₂)
    source
    @[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)
    source
    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₂.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[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₂
      source
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        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
        source
        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₂.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[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)
          source
          @[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)
          source
          @[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₂
          source
          @[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₂)