Mathlib.LinearAlgebra.TensorProduct.Basis

Basis.tensorProduct definition

(b : Basis ι S M) (c : Basis κ R N) : Basis (ι × κ) S (M ⊗[R] N)

Full source

/-- If `b : ι → M` and `c : κ → N` are bases then so is `fun i ↦ b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N`. -/
def Basis.tensorProduct (b : Basis ι S M) (c : Basis κ R N) :
    Basis (ι × κ) S (M ⊗[R] N) :=
  Finsupp.basisSingleOne.map
    ((TensorProduct.AlgebraTensorModule.congr b.repr c.repr).trans <|
        (finsuppTensorFinsupp R S _ _ _ _).trans <|
          Finsupp.lcongr (Equiv.refl _) (TensorProduct.AlgebraTensorModule.rid R S S)).symm

Tensor product of bases

Informal description

Given a basis $b \colon \iota \to M$ for an $S$-module $M$ and a basis $c \colon \kappa \to N$ for an $R$-module $N$, the function $\text{Basis.tensorProduct}$ constructs a basis for the tensor product $M \otimes_R N$ over $S$ indexed by $\iota \times \kappa$. The basis vectors are given by $(i,j) \mapsto b(i) \otimes c(j)$.

Basis.tensorProduct_apply theorem

(b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) : Basis.tensorProduct b c (i, j) = b i ⊗ₜ c j

Full source

@[simp]
theorem Basis.tensorProduct_apply (b : Basis ι S M) (c : Basis κ R N) (i : ι) (j : κ) :
    Basis.tensorProduct b c (i, j) = b i ⊗ₜ c j := by
  simp [Basis.tensorProduct]

Tensor Product Basis Evaluation: $(b \otimes c)(i,j) = b(i) \otimes c(j)$

Informal description

Given a basis $b \colon \iota \to M$ for an $S$-module $M$ and a basis $c \colon \kappa \to N$ for an $R$-module $N$, the tensor product basis $b \otimes c$ evaluated at $(i,j) \in \iota \times \kappa$ equals the tensor product of the basis vectors $b(i) \otimes c(j)$.

Basis.tensorProduct_apply' theorem

(b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) : Basis.tensorProduct b c i = b i.1 ⊗ₜ c i.2

Full source

theorem Basis.tensorProduct_apply' (b : Basis ι S M) (c : Basis κ R N) (i : ι × κ) :
    Basis.tensorProduct b c i = b i.1 ⊗ₜ c i.2 := by
  simp [Basis.tensorProduct]

Tensor Product Basis Evaluation: $(b \otimes c)(i,j) = b(i) \otimes c(j)$

Informal description

Given a basis $b \colon \iota \to M$ for an $S$-module $M$ and a basis $c \colon \kappa \to N$ for an $R$-module $N$, the tensor product basis $b \otimes c$ evaluated at any pair $(i,j) \in \iota \times \kappa$ equals the tensor product of the basis vectors $b(i) \otimes c(j)$.

Basis.tensorProduct_repr_tmul_apply theorem

 (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) :
  (Basis.tensorProduct b c).repr (m ⊗ₜ n) (i, j) = c.repr n j • b.repr m i

Full source

@[simp]
theorem Basis.tensorProduct_repr_tmul_apply (b : Basis ι S M) (c : Basis κ R N) (m : M) (n : N)
    (i : ι) (j : κ) :
    (Basis.tensorProduct b c).repr (m ⊗ₜ n) (i, j) = c.repr n j • b.repr m i := by
  simp [Basis.tensorProduct, mul_comm]

Coefficient Formula for Tensor Product in Basis

Informal description

Let $b \colon \iota \to M$ be a basis for an $S$-module $M$ and $c \colon \kappa \to N$ be a basis for an $R$-module $N$. For any elements $m \in M$ and $n \in N$, and any indices $i \in \iota$ and $j \in \kappa$, the coefficient of the tensor product $m \otimes n$ in the basis $b \otimes c$ at the index $(i,j)$ is given by the product of the coefficient of $n$ in the basis $c$ at $j$ and the coefficient of $m$ in the basis $b$ at $i$. That is, \[ (b \otimes c).\text{repr}(m \otimes n)(i,j) = c.\text{repr}(n)(j) \cdot b.\text{repr}(m)(i). \]

Basis.baseChange definition

(b : Basis ι R M) : Basis ι S (S ⊗[R] M)

Full source

/-- The lift of an `R`-basis of `M` to an `S`-basis of the base change `S ⊗[R] M`. -/
noncomputable
def Basis.baseChange (b : Basis ι R M) : Basis ι S (S ⊗[R] M) :=
  ((Basis.singleton Unit S).tensorProduct b).reindex (Equiv.punitProd ι)

Base change of a basis

Informal description

Given a basis $b \colon \iota \to M$ for an $R$-module $M$, the function $\text{Basis.baseChange}$ constructs a basis for the base change $S \otimes_R M$ over $S$ indexed by $\iota$. The basis vectors are given by $i \mapsto 1 \otimes b(i)$. More precisely, the basis is obtained by first forming the tensor product of the singleton basis of $S$ (indexed by the unit type) with $b$, and then reindexing via the equivalence $\text{PUnit} \times \iota \simeq \iota$.

Basis.baseChange_repr_tmul theorem

(b : Basis ι R M) (x y i) : (b.baseChange S).repr (x ⊗ₜ y) i = b.repr y i • x

Full source

@[simp]
lemma Basis.baseChange_repr_tmul (b : Basis ι R M) (x y i) :
    (b.baseChange S).repr (x ⊗ₜ y) i = b.repr y i • x := by
  simp [Basis.baseChange, Basis.tensorProduct]

Coefficient formula for tensor product in base-changed basis

Informal description

Let $b \colon \iota \to M$ be a basis for an $R$-module $M$, and let $S$ be an $R$-algebra. For any $x \in S$, $y \in M$, and $i \in \iota$, the coefficient of the tensor product $x \otimes y$ in the base-changed basis $b_{\text{baseChange}\,S}$ at index $i$ is given by the scalar multiplication of the coefficient of $y$ in the original basis $b$ at $i$ with $x$. That is, \[ (b_{\text{baseChange}\,S}).\text{repr}(x \otimes y)(i) = b.\text{repr}(y)(i) \cdot x. \]

Basis.baseChange_apply theorem

(b : Basis ι R M) (i) : b.baseChange S i = 1 ⊗ₜ b i

Full source

@[simp]
lemma Basis.baseChange_apply (b : Basis ι R M) (i) :
    b.baseChange S i = 1 ⊗ₜ b i := by
  simp [Basis.baseChange, Basis.tensorProduct]

Base-changed basis vector as tensor product with identity

Informal description

Given a basis $b \colon \iota \to M$ for an $R$-module $M$ and an $R$-algebra $S$, the basis vector at index $i$ in the base-changed basis $b_{\text{baseChange}\,S}$ for $S \otimes_R M$ is equal to $1 \otimes b(i)$, where $1$ is the multiplicative identity in $S$.

TensorProduct.equivFinsuppOfBasisRight definition

: M ⊗[R] N ≃ₗ[R] κ →₀ M

Full source

/--
If `{𝒞ᵢ}` is a basis for the module `N`, then every elements of `x ∈ M ⊗ N` can be uniquely written
as `∑ᵢ mᵢ ⊗ 𝒞ᵢ` for some `mᵢ ∈ M`.
-/
def TensorProduct.equivFinsuppOfBasisRight : M ⊗[R] NM ⊗[R] N ≃ₗ[R] κ →₀ M :=
  LinearEquiv.lTensorLinearEquiv.lTensor M 𝒞.repr ≪≫ₗ TensorProduct.finsuppScalarRight R M κ

Linear equivalence between tensor product and finitely supported functions via a basis

Informal description

Given a basis $\{\mathcal{C}_i\}_{i \in \kappa}$ for the module $N$ over a ring $R$, there is a linear equivalence between the tensor product $M \otimes_R N$ and the space of finitely supported functions from $\kappa$ to $M$. This equivalence maps an element $m \otimes n \in M \otimes_R N$ to the finitely supported function $i \mapsto (\text{coefficient of } \mathcal{C}_i \text{ in } n) \cdot m$.

TensorProduct.equivFinsuppOfBasisRight_apply_tmul theorem

 (m : M) (n : N) : (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) = (𝒞.repr n).mapRange (· • m) (zero_smul _ _)

Full source

@[simp]
lemma TensorProduct.equivFinsuppOfBasisRight_apply_tmul (m : M) (n : N) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) =
    (𝒞.repr n).mapRange (· • m) (zero_smul _ _) := by
  ext; simp [equivFinsuppOfBasisRight]

Image of Tensor Product under Basis-Induced Linear Equivalence

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{C}$ be a basis for $N$ indexed by $\kappa$. For any elements $m \in M$ and $n \in N$, the image of the tensor product $m \otimes n$ under the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisRight}(\mathcal{C})$ is the finitely supported function from $\kappa$ to $M$ given by $i \mapsto (\mathcal{C}.repr(n))(i) \cdot m$, where $\mathcal{C}.repr(n)$ denotes the coordinate representation of $n$ in the basis $\mathcal{C}$.

TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply theorem

(m : M) (n : N) (i : κ) : (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) i = 𝒞.repr n i • m

Full source

lemma TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply
    (m : M) (n : N) (i : κ) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ n) i =
    𝒞.repr n i • m := by
  simp only [equivFinsuppOfBasisRight_apply_tmul, Finsupp.mapRange_apply]

Component Formula for Tensor Product under Basis-Induced Linear Equivalence

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{C}$ be a basis for $N$ indexed by $\kappa$. For any elements $m \in M$ and $n \in N$, and any index $i \in \kappa$, the $i$-th component of the image of the tensor product $m \otimes n$ under the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisRight}(\mathcal{C})$ is given by $(\mathcal{C}.repr(n))(i) \cdot m$, where $\mathcal{C}.repr(n)$ denotes the coordinate representation of $n$ in the basis $\mathcal{C}$.

TensorProduct.equivFinsuppOfBasisRight_symm theorem

 :
  (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.toLinearMap =
    Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i)

Full source

lemma TensorProduct.equivFinsuppOfBasisRight_symm :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.toLinearMap =
    Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i) := by
  ext; simp [equivFinsuppOfBasisRight]

Inverse of Tensor Product-Basis Linear Equivalence as Sum of Tensors

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{C}$ be a basis for $N$ indexed by $\kappa$. The inverse of the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisRight}(\mathcal{C})$ is equal to the linear map obtained by summing over the basis vectors $\mathcal{C}_i$ and applying the flipped tensor product map. Specifically, for any finitely supported function $b : \kappa \to_{\text{f}} M$, we have: $$ \text{TensorProduct.equivFinsuppOfBasisRight}(\mathcal{C})^{-1}(b) = \sum_{i \in \kappa} b(i) \otimes \mathcal{C}_i $$

TensorProduct.equivFinsuppOfBasisRight_symm_apply theorem

(b : κ →₀ M) : (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm b = b.sum fun i m ↦ m ⊗ₜ 𝒞 i

Full source

@[simp]
lemma TensorProduct.equivFinsuppOfBasisRight_symm_apply (b : κ →₀ M) :
    (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm b = b.sum fun i m ↦ m ⊗ₜ 𝒞 i :=
  congr($(TensorProduct.equivFinsuppOfBasisRight_symm 𝒞) b)

Inverse of Tensor Product-Basis Equivalence as Sum of Tensors

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{C} = \{\mathcal{C}_i\}_{i \in \kappa}$ be a basis for $N$. For any finitely supported function $b : \kappa \to_{\text{f}} M$, the inverse of the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisRight}(\mathcal{C})$ maps $b$ to the sum $\sum_{i \in \kappa} b(i) \otimes \mathcal{C}_i$ in $M \otimes_R N$.

TensorProduct.sum_tmul_basis_right_injective theorem

: Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i))

Full source

lemma TensorProduct.sum_tmul_basis_right_injective :
    Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N).flip (𝒞 i)) :=
  have := Classical.decEq κ
  (equivFinsuppOfBasisRight_symm (M := M) 𝒞).symm ▸
    (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.injective

Injectivity of Tensor Summation with Basis Elements

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\{\mathcal{C}_i\}_{i \in \kappa}$ be a basis for $N$. The linear map $$\sum_{i \in \kappa} (m \otimes \mathcal{C}_i) \mapsto \sum_{i \in \kappa} m \otimes \mathcal{C}_i$$ is injective. In other words, if $\sum_{i \in \kappa} m_i \otimes \mathcal{C}_i = 0$ in $M \otimes_R N$, then $m_i = 0$ for all $i \in \kappa$.

TensorProduct.sum_tmul_basis_right_eq_zero theorem

(b : κ →₀ M) (h : (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = 0) : b = 0

Full source

lemma TensorProduct.sum_tmul_basis_right_eq_zero
    (b : κ →₀ M) (h : (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = 0) : b = 0 :=
  have := Classical.decEq κ
  (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.injective (a₂ := 0) <| by simpa

Vanishing of Tensor Sum Implies Vanishing of Coefficients (Right Basis)

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\{\mathcal{C}_i\}_{i \in \kappa}$ be a basis for $N$. For any finitely supported function $b : \kappa \to_{\text{f}} M$, if the sum $\sum_{i \in \kappa} b(i) \otimes \mathcal{C}_i$ equals zero in the tensor product $M \otimes_R N$, then $b$ must be the zero function.

TensorProduct.equivFinsuppOfBasisLeft definition

: M ⊗[R] N ≃ₗ[R] ι →₀ N

Full source

/--
If `{ℬᵢ}` is a basis for the module `M`, then every elements of `x ∈ M ⊗ N` can be uniquely written
as `∑ᵢ ℬᵢ ⊗ nᵢ` for some `nᵢ ∈ N`.
-/
def TensorProduct.equivFinsuppOfBasisLeft : M ⊗[R] NM ⊗[R] N ≃ₗ[R] ι →₀ N :=
  TensorProduct.commTensorProduct.comm R M N ≪≫ₗ TensorProduct.equivFinsuppOfBasisRight ℬ

Linear equivalence between tensor product and finitely supported functions via a left basis

Informal description

Given a basis $\{\mathcal{B}_i\}_{i \in \iota}$ for the module $M$ over a ring $R$, there is a linear equivalence between the tensor product $M \otimes_R N$ and the space of finitely supported functions from $\iota$ to $N$. This equivalence maps an element $m \otimes n \in M \otimes_R N$ to the finitely supported function $i \mapsto (\text{coefficient of } \mathcal{B}_i \text{ in } m) \cdot n$.

TensorProduct.equivFinsuppOfBasisLeft_apply_tmul theorem

 (m : M) (n : N) : (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) = (ℬ.repr m).mapRange (· • n) (zero_smul _ _)

Full source

@[simp]
lemma TensorProduct.equivFinsuppOfBasisLeft_apply_tmul (m : M) (n : N) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) =
    (ℬ.repr m).mapRange (· • n) (zero_smul _ _) := by
  ext; simp [equivFinsuppOfBasisLeft]

Image of Tensor Product under Basis-Induced Linear Equivalence (Left Basis)

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{B}$ be a basis for $M$ indexed by $\iota$. For any elements $m \in M$ and $n \in N$, the image of the tensor product $m \otimes n$ under the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisLeft}(\mathcal{B})$ is the finitely supported function from $\iota$ to $N$ given by $i \mapsto (\mathcal{B}.repr(m))(i) \cdot n$, where $\mathcal{B}.repr(m)$ denotes the coordinate representation of $m$ in the basis $\mathcal{B}$.

TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply theorem

(m : M) (n : N) (i : ι) : (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) i = ℬ.repr m i • n

Full source

lemma TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply
    (m : M) (n : N) (i : ι) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ n) i =
    ℬ.repr m i • n := by
  simp only [equivFinsuppOfBasisLeft_apply_tmul, Finsupp.mapRange_apply]

Component Formula for Tensor Product under Basis-Induced Linear Equivalence (Left Basis)

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{B}$ be a basis for $M$ indexed by $\iota$. For any elements $m \in M$, $n \in N$, and any index $i \in \iota$, the $i$-th component of the image of $m \otimes n$ under the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisLeft}(\mathcal{B})$ is equal to the scalar multiple $(\mathcal{B}.repr(m))(i) \cdot n$, where $\mathcal{B}.repr(m)$ denotes the coordinate representation of $m$ in the basis $\mathcal{B}$.

TensorProduct.equivFinsuppOfBasisLeft_symm theorem

 : (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.toLinearMap = Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N) (ℬ i)

Full source

lemma TensorProduct.equivFinsuppOfBasisLeft_symm :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.toLinearMap =
    Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N) (ℬ i) := by
  ext; simp [equivFinsuppOfBasisLeft]

Inverse of Tensor Product-Basis Equivalence as Sum of Tensors (Left Basis)

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{B} = \{\mathcal{B}_i\}_{i \in \iota}$ be a basis for $M$. The inverse of the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisLeft}(\mathcal{B})$ is given by the linear map that sends a finitely supported function $f : \iota \to_{\text{f}} N$ to the sum $\sum_{i \in \iota} \mathcal{B}_i \otimes f(i)$ in $M \otimes_R N$.

TensorProduct.equivFinsuppOfBasisLeft_symm_apply theorem

(b : ι →₀ N) : (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm b = b.sum fun i n ↦ ℬ i ⊗ₜ n

Full source

@[simp]
lemma TensorProduct.equivFinsuppOfBasisLeft_symm_apply (b : ι →₀ N) :
    (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm b = b.sum fun i n ↦ ℬ i ⊗ₜ n :=
  congr($(TensorProduct.equivFinsuppOfBasisLeft_symm ℬ) b)

Inverse of Tensor Product-Basis Equivalence Applied to Finitely Supported Function (Left Basis)

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{B} = \{\mathcal{B}_i\}_{i \in \iota}$ be a basis for $M$. For any finitely supported function $b : \iota \to_{\text{f}} N$, the inverse of the linear equivalence $\text{TensorProduct.equivFinsuppOfBasisLeft}(\mathcal{B})$ maps $b$ to the sum $\sum_{i \in \iota} \mathcal{B}_i \otimes b(i)$ in $M \otimes_R N$.

TensorProduct.sum_tmul_basis_left_injective theorem

: Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N) (ℬ i))

Full source

lemma TensorProduct.sum_tmul_basis_left_injective :
    Function.Injective (Finsupp.lsum R fun i ↦ (TensorProduct.mk R M N) (ℬ i)) :=
  have := Classical.decEq ι
  (equivFinsuppOfBasisLeft_symm (N := N) ℬ).symm ▸
    (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.injective

Injectivity of Tensor Summation via Basis Vectors

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{B} = \{\mathcal{B}_i\}_{i \in \iota}$ be a basis for $M$. The linear map that sends a finitely supported function $f : \iota \to_{\text{f}} N$ to the sum $\sum_{i \in \iota} \mathcal{B}_i \otimes f(i)$ in $M \otimes_R N$ is injective.

TensorProduct.sum_tmul_basis_left_eq_zero theorem

(b : ι →₀ N) (h : (b.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = 0) : b = 0

Full source

lemma TensorProduct.sum_tmul_basis_left_eq_zero
    (b : ι →₀ N) (h : (b.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = 0) : b = 0 :=
  have := Classical.decEq ι
  (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.injective (a₂ := 0) <| by simpa

Vanishing Tensor Sum Implies Zero Coefficients for Basis Expansion

Informal description

Let $M$ and $N$ be modules over a ring $R$, and let $\mathcal{B} = \{\mathcal{B}_i\}_{i \in \iota}$ be a basis for $M$. For any finitely supported function $b : \iota \to_{\text{f}} N$, if the sum $\sum_{i \in \iota} \mathcal{B}_i \otimes b(i) = 0$ in $M \otimes_R N$, then $b$ must be the zero function.

Module.Free.tensor instance

: Module.Free S (M ⊗[R] N)

Full source

instance Module.Free.tensor : Module.Free S (M ⊗[R] N) :=
  let ⟨bM⟩ := exists_basis (R := S) (M := M)
  let ⟨bN⟩ := exists_basis (R := R) (M := N)
  of_basis (bM.2.tensorProduct bN.2)

Tensor Product of Free Modules is Free

Informal description

Given a free module $M$ over a semiring $S$ and a free module $N$ over a semiring $R$, the tensor product $M \otimes_R N$ is a free module over $S$.