Mathlib.LinearAlgebra.DirectSum.Finsupp

TensorProduct.finsuppLeft definition

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

Full source

/-- The tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N` -/
noncomputable def finsuppLeft :
    (ι →₀ M) ⊗[R] N(ι →₀ M) ⊗[R] N ≃ₗ[R] ι →₀ M ⊗[R] N :=
  congrcongr (finsuppLEquivDirectSum R M ι) (.refl R N) ≪≫ₗ
    directSumLeft R (fun _ ↦ M) Ncongr (finsuppLEquivDirectSum R M ι) (.refl R N) ≪≫ₗ
    directSumLeft R (fun _ ↦ M) N ≪≫ₗ (finsuppLEquivDirectSum R _ ι).symm

Linear equivalence between tensor product of finitely supported functions and finitely supported tensor products

Informal description

The tensor product of the space of finitely supported functions $\iota \to M$ with an $R$-module $N$ is linearly equivalent to the space of finitely supported functions $\iota \to (M \otimes_R N)$. More precisely, there exists a linear equivalence between $(\iota \to_{\text{f}} M) \otimes_R N$ and $\iota \to_{\text{f}} (M \otimes_R N)$, where $\to_{\text{f}}$ denotes finitely supported functions.

TensorProduct.finsuppLeft_apply_tmul theorem

(p : ι →₀ M) (n : N) : finsuppLeft R M N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)

Full source

lemma finsuppLeft_apply_tmul (p : ι →₀ M) (n : N) :
    finsuppLeft R M N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
  induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [add_tmul, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppLeft]

Image of Tensor Product under Linear Equivalence $\text{finsuppLeft}$ as Sum of Single-Element Functions

Informal description

For any finitely supported function $p \colon \iota \to M$ and any element $n \in N$, the image of the tensor product $p \otimes_R n$ under the linear equivalence $\text{finsuppLeft}$ is equal to the sum over $\iota$ of the single-element finitely supported functions $\text{single}(i, m \otimes_R n)$, where $m = p(i)$. That is, \[ \text{finsuppLeft}(p \otimes_R n) = \sum_{i \in \iota} \text{single}(i, p(i) \otimes_R n). \]

TensorProduct.finsuppLeft_apply_tmul_apply theorem

(p : ι →₀ M) (n : N) (i : ι) : finsuppLeft R M N ι (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n

Full source

@[simp]
lemma finsuppLeft_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) :
    finsuppLeft R M N ι (p ⊗ₜ[R] n) i = p i ⊗ₜ[R] n := by
  rw [finsuppLeft_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Evaluation of Tensor-Finsupp Equivalence at Index $i$: $\text{finsuppLeft}(p \otimes n)(i) = p(i) \otimes n$

Informal description

For any finitely supported function $p \colon \iota \to M$, any element $n \in N$, and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppLeft}_{R,M,N,\iota}$ at the tensor product $p \otimes_R n$ and index $i$ is equal to the tensor product $p(i) \otimes_R n$. That is, \[ \text{finsuppLeft}_{R,M,N,\iota}(p \otimes_R n)(i) = p(i) \otimes_R n. \]

TensorProduct.finsuppLeft_apply theorem

(t : (ι →₀ M) ⊗[R] N) (i : ι) : finsuppLeft R M N ι t i = rTensor N (Finsupp.lapply i) t

Full source

theorem finsuppLeft_apply (t : (ι →₀ M) ⊗[R] N) (i : ι) :
    finsuppLeft R M N ι t i = rTensor N (Finsupp.lapply i) t := by
  induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
  | add x y hx hy => simp [map_add, hx, hy]

Evaluation of Tensor-Finsupp Equivalence via Right Tensor Map: $\text{finsuppLeft}(t)(i) = \text{rTensor}_N(\text{lapply}_i)(t)$

Informal description

For any element $t$ in the tensor product $(\iota \to_{\text{f}} M) \otimes_R N$ and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppLeft}_{R,M,N,\iota}(t)$ at $i$ is equal to the right tensor product map $\text{rTensor}_N$ applied to the left application map $\text{lapply}_i$ evaluated at $t$. That is, \[ \text{finsuppLeft}_{R,M,N,\iota}(t)(i) = \text{rTensor}_N(\text{lapply}_i)(t). \]

TensorProduct.finsuppLeft_symm_apply_single theorem

 (i : ι) (m : M) (n : N) : (finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i m ⊗ₜ[R] n

Full source

@[simp]
lemma finsuppLeft_symm_apply_single (i : ι) (m : M) (n : N) :
    (finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
      Finsupp.singleFinsupp.single i m ⊗ₜ[R] n := by
  simp [finsuppLeft, Finsupp.lsum]

Inverse of Tensor-Finsupp Equivalence on Single Elements

Informal description

For any index $i \in \iota$, elements $m \in M$ and $n \in N$, the inverse of the linear equivalence $\text{finsuppLeft}_{R,M,N,\iota}$ maps the finitely supported function $\text{single}_i(m \otimes_R n)$ to the tensor product $\text{single}_i m \otimes_R n$ in $(\iota \to_{\text{f}} M) \otimes_R N$.

TensorProduct.finsuppRight definition

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

Full source

/-- The tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N` -/
noncomputable def finsuppRight :
    M ⊗[R] (ι →₀ N)M ⊗[R] (ι →₀ N) ≃ₗ[R] ι →₀ M ⊗[R] N :=
  congrcongr (.refl R M) (finsuppLEquivDirectSum R N ι) ≪≫ₗ
    directSumRight R M (fun _ : ι ↦ N)congr (.refl R M) (finsuppLEquivDirectSum R N ι) ≪≫ₗ
    directSumRight R M (fun _ : ι ↦ N) ≪≫ₗ (finsuppLEquivDirectSum R _ ι).symm

Linear equivalence between tensor product with finitely supported functions and finitely supported tensor products

Informal description

The tensor product $M \otimes_R (\iota \to_{\text{f}} N)$ of an $R$-module $M$ with the space of finitely supported functions $\iota \to_{\text{f}} N$ is linearly equivalent to the space of finitely supported functions $\iota \to_{\text{f}} (M \otimes_R N)$. Here $\iota \to_{\text{f}} N$ denotes functions from $\iota$ to $N$ with finite support.

TensorProduct.finsuppRight_apply_tmul theorem

(m : M) (p : ι →₀ N) : finsuppRight R M N ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n)

Full source

lemma finsuppRight_apply_tmul (m : M) (p : ι →₀ N) :
    finsuppRight R M N ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (m ⊗ₜ[R] n) := by
  induction p using Finsupp.induction_linear with
  | zero => simp
  | add f g hf hg => simp [tmul_add, map_add, hf, hg, Finsupp.sum_add_index]
  | single => simp [finsuppRight]

Image of Tensor Product under Linear Equivalence $\text{finsuppRight}_{R,M,N,\iota}$ as Finite Sum of Single-Element Functions

Informal description

For any element $m$ in an $R$-module $M$ and any finitely supported function $p \colon \iota \to_{\text{f}} N$, the image of the tensor product $m \otimes p$ under the linear equivalence $\text{finsuppRight}_{R,M,N,\iota}$ is equal to the finite sum \[ \sum_{i \in \iota} \text{single}(i, m \otimes p(i)), \] where $\text{single}(i, m \otimes p(i))$ denotes the finitely supported function that is $m \otimes p(i)$ at $i$ and zero elsewhere.

TensorProduct.finsuppRight_apply_tmul_apply theorem

(m : M) (p : ι →₀ N) (i : ι) : finsuppRight R M N ι (m ⊗ₜ[R] p) i = m ⊗ₜ[R] p i

Full source

@[simp]
lemma finsuppRight_apply_tmul_apply (m : M) (p : ι →₀ N) (i : ι) :
    finsuppRight R M N ι (m ⊗ₜ[R] p) i = m ⊗ₜ[R] p i := by
  rw [finsuppRight_apply_tmul, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Evaluation of Tensor-Finsupp Equivalence: $\text{finsuppRight}(m \otimes p)(i) = m \otimes p(i)$

Informal description

For any element $m$ in an $R$-module $M$, any finitely supported function $p \colon \iota \to_{\text{f}} N$, and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppRight}_{R,M,N,\iota}$ at the tensor product $m \otimes p$ and index $i$ is equal to the tensor product $m \otimes p(i)$. That is, \[ \text{finsuppRight}_{R,M,N,\iota}(m \otimes p)(i) = m \otimes p(i). \]

TensorProduct.finsuppRight_apply theorem

(t : M ⊗[R] (ι →₀ N)) (i : ι) : finsuppRight R M N ι t i = lTensor M (Finsupp.lapply i) t

Full source

theorem finsuppRight_apply (t : M ⊗[R] (ι →₀ N)) (i : ι) :
    finsuppRight R M N ι t i = lTensor M (Finsupp.lapply i) t := by
  induction t with
  | zero => simp
  | tmul m f => simp [finsuppRight_apply_tmul_apply]
  | add x y hx hy => simp [map_add, hx, hy]

Evaluation of Tensor-Finsupp Equivalence via Left Tensor Action

Informal description

For any element $t$ in the tensor product $M \otimes_R (\iota \to_{\text{f}} N)$ and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppRight}_{R,M,N,\iota}(t)$ at $i$ is equal to the left tensor product action of $M$ on the linear map $\text{lapply}_i$ applied to $t$. That is, \[ \text{finsuppRight}_{R,M,N,\iota}(t)(i) = \text{lTensor}_M(\text{lapply}_i)(t). \]

TensorProduct.finsuppRight_symm_apply_single theorem

 (i : ι) (m : M) (n : N) : (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = m ⊗ₜ[R] Finsupp.single i n

Full source

@[simp]
lemma finsuppRight_symm_apply_single (i : ι) (m : M) (n : N) :
    (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) =
      m ⊗ₜ[R] Finsupp.single i n := by
  simp [finsuppRight, Finsupp.lsum]

Inverse of Tensor-Finsupp Equivalence on Basis Elements

Informal description

For any index $i \in \iota$ and elements $m \in M$, $n \in N$, the inverse of the linear equivalence `finsuppRight` maps the finitely supported function $\text{single}_i(m \otimes_R n)$ to the tensor product $m \otimes_R \text{single}_i(n)$. Here: - $\text{single}_i$ denotes the finitely supported function that is $1$ at $i$ and $0$ elsewhere - $\otimes_R$ denotes the tensor product over the ring $R$ - $\text{finsuppRight}$ is the linear equivalence between $M \otimes_R (\iota \to_{\text{f}} N)$ and $\iota \to_{\text{f}} (M \otimes_R N)$

TensorProduct.finsuppLeft_smul' theorem

(s : S) (t : (ι →₀ M) ⊗[R] N) : finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t

Full source

lemma finsuppLeft_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) :
    finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t := by
  induction t with
  | zero => simp
  | add x y hx hy => simp [hx, hy]
  | tmul p n => ext; simp [smul_tmul', finsuppLeft_apply_tmul_apply]

Scalar Multiplication Commutes with Tensor-Finsupp Equivalence: $\text{finsuppLeft}(s \cdot t) = s \cdot \text{finsuppLeft}(t)$

Informal description

For any scalar $s \in S$ and any element $t$ in the tensor product $(\iota \to_{\text{f}} M) \otimes_R N$, the linear equivalence $\text{finsuppLeft}_{R,M,N,\iota}$ satisfies \[ \text{finsuppLeft}_{R,M,N,\iota}(s \cdot t) = s \cdot \text{finsuppLeft}_{R,M,N,\iota}(t). \] Here $\to_{\text{f}}$ denotes finitely supported functions and $\otimes_R$ denotes the tensor product over the ring $R$.

TensorProduct.finsuppLeft' definition

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

Full source

/-- When `M` is also an `S`-module, then `TensorProduct.finsuppLeft R M N``
  is an `S`-linear equiv -/
noncomputable def finsuppLeft' :
    (ι →₀ M) ⊗[R] N(ι →₀ M) ⊗[R] N ≃ₗ[S] ι →₀ M ⊗[R] N where
  __ := finsuppLeft R M N ι
  map_smul' := finsuppLeft_smul'

$S$-linear equivalence between tensor product of finitely supported functions and finitely supported tensor products

Informal description

When $M$ is also an $S$-module, the linear equivalence between the tensor product $(\iota \to_{\text{f}} M) \otimes_R N$ and the space of finitely supported functions $\iota \to_{\text{f}} (M \otimes_R N)$ is also $S$-linear. Here: - $\to_{\text{f}}$ denotes finitely supported functions - $\otimes_R$ denotes the tensor product over the ring $R$ - The equivalence is given by $\text{finsuppLeft}_{R,M,N,\iota}$ in the $R$-linear case

TensorProduct.finsuppLeft'_apply theorem

(x : (ι →₀ M) ⊗[R] N) : finsuppLeft' R M N ι S x = finsuppLeft R M N ι x

Full source

lemma finsuppLeft'_apply (x : (ι →₀ M) ⊗[R] N) :
    finsuppLeft' R M N ι S x = finsuppLeft R M N ι x := rfl

Equality of Finsupp-Tensor Equivalences: $\text{finsuppLeft}' = \text{finsuppLeft}$

Informal description

For any element $x$ in the tensor product $(\iota \to_{\text{f}} M) \otimes_R N$, the application of the $S$-linear equivalence $\text{finsuppLeft}'_{R,M,N,\iota,S}$ to $x$ is equal to the application of the $R$-linear equivalence $\text{finsuppLeft}_{R,M,N,\iota}$ to $x$. Here: - $\to_{\text{f}}$ denotes finitely supported functions - $\otimes_R$ denotes the tensor product over the ring $R$

TensorProduct.finsuppScalarLeft definition

: (ι →₀ R) ⊗[R] N ≃ₗ[R] ι →₀ N

Full source

/-- The tensor product of `ι →₀ R` and `N` is linearly equivalent to `ι →₀ N` -/
noncomputable def finsuppScalarLeft :
    (ι →₀ R) ⊗[R] N(ι →₀ R) ⊗[R] N ≃ₗ[R] ι →₀ N :=
  finsuppLeftfinsuppLeft R R N ι ≪≫ₗ (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))

Linear equivalence between tensor product of scalar finitely supported functions and finitely supported functions

Informal description

The tensor product of the space of finitely supported functions $\iota \to R$ with an $R$-module $N$ is linearly equivalent to the space of finitely supported functions $\iota \to N$. More precisely, there exists a linear equivalence between $(\iota \to_{\text{f}} R) \otimes_R N$ and $\iota \to_{\text{f}} N$, where $\to_{\text{f}}$ denotes finitely supported functions.

TensorProduct.finsuppScalarLeft_apply_tmul_apply theorem

(p : ι →₀ R) (n : N) (i : ι) : finsuppScalarLeft R N ι (p ⊗ₜ[R] n) i = p i • n

Full source

@[simp]
lemma finsuppScalarLeft_apply_tmul_apply (p : ι →₀ R) (n : N) (i : ι) :
    finsuppScalarLeft R N ι (p ⊗ₜ[R] n) i = p i • n := by
  simp [finsuppScalarLeft]

Evaluation of Scalar-Tensor-Finsupp Equivalence: $\text{finsuppScalarLeft}(p \otimes n)(i) = p(i) \cdot n$

Informal description

For any finitely supported function $p \colon \iota \to R$, any element $n \in N$, and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppScalarLeft}_{R,N,\iota}$ at the tensor product $p \otimes_R n$ and index $i$ is equal to the scalar multiplication $p(i) \cdot n$. That is, \[ \text{finsuppScalarLeft}_{R,N,\iota}(p \otimes_R n)(i) = p(i) \cdot n. \]

TensorProduct.finsuppScalarLeft_apply_tmul theorem

(p : ι →₀ R) (n : N) : finsuppScalarLeft R N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m • n)

Full source

lemma finsuppScalarLeft_apply_tmul (p : ι →₀ R) (n : N) :
    finsuppScalarLeft R N ι (p ⊗ₜ[R] n) = p.sum fun i m ↦ Finsupp.single i (m • n) := by
  ext i
  rw [finsuppScalarLeft_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Image of Tensor Product under Scalar Finsupp-Tensor Equivalence

Informal description

For any finitely supported function $p \colon \iota \to R$ and any element $n \in N$, the image of the tensor product $p \otimes_R n$ under the linear equivalence $\text{finsuppScalarLeft}_{R,N,\iota}$ is equal to the sum over all indices $i \in \iota$ of the finitely supported functions $\text{single}_i (p(i) \cdot n)$. In mathematical notation: \[ \text{finsuppScalarLeft}_{R,N,\iota}(p \otimes_R n) = \sum_{i \in \iota} \text{single}_i (p(i) \cdot n). \]

TensorProduct.finsuppScalarLeft_apply theorem

 (pn : (ι →₀ R) ⊗[R] N) (i : ι) : finsuppScalarLeft R N ι pn i = TensorProduct.lid R N ((Finsupp.lapply i).rTensor N pn)

Full source

lemma finsuppScalarLeft_apply (pn : (ι →₀ R) ⊗[R] N) (i : ι) :
    finsuppScalarLeft R N ι pn i = TensorProduct.lid R N ((Finsupp.lapply i).rTensor N pn) := by
  simp [finsuppScalarLeft, finsuppLeft_apply]

Evaluation of Scalar-Tensor-Finsupp Equivalence via Left Identity Map

Informal description

For any element $pn$ in the tensor product $(\iota \to_{\text{f}} R) \otimes_R N$ and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppScalarLeft}_{R,N,\iota}(pn)$ at $i$ is equal to the left identity map $\text{lid}_{R,N}$ applied to the right tensor product of the left application map $\text{lapply}_i$ evaluated at $pn$. That is, \[ \text{finsuppScalarLeft}_{R,N,\iota}(pn)(i) = \text{lid}_{R,N}(\text{rTensor}_N(\text{lapply}_i)(pn)). \]

TensorProduct.finsuppScalarLeft_symm_apply_single theorem

(i : ι) (n : N) : (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = (Finsupp.single i 1) ⊗ₜ[R] n

Full source

@[simp]
lemma finsuppScalarLeft_symm_apply_single (i : ι) (n : N) :
    (finsuppScalarLeft R N ι).symm (Finsupp.single i n) =
      (Finsupp.single i 1) ⊗ₜ[R] n := by
  simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]

Inverse of Scalar Finsupp-Tensor Equivalence on Single Elements

Informal description

For any index $i \in \iota$ and element $n \in N$, the inverse of the linear equivalence $\text{finsuppScalarLeft}_{R,N,\iota}$ maps the finitely supported function $\text{single}_i n$ to the tensor product $\text{single}_i 1 \otimes_R n$ in $(\iota \to_{\text{f}} R) \otimes_R N$. In mathematical notation: $$(\text{finsuppScalarLeft}_{R,N,\iota})^{-1}(\text{single}_i n) = \text{single}_i 1 \otimes_R n.$$

TensorProduct.finsuppScalarRight definition

: M ⊗[R] (ι →₀ R) ≃ₗ[R] ι →₀ M

Full source

/-- The tensor product of `M` and `ι →₀ R` is linearly equivalent to `ι →₀ M` -/
noncomputable def finsuppScalarRight :
    M ⊗[R] (ι →₀ R)M ⊗[R] (ι →₀ R) ≃ₗ[R] ι →₀ M :=
  finsuppRightfinsuppRight R M R ι ≪≫ₗ Finsupp.mapRange.linearEquiv (TensorProduct.rid R M)

Linear equivalence between tensor product with scalar finitely supported functions and finitely supported functions valued in $M$

Informal description

The tensor product $M \otimes_R (\iota \to_{\text{f}} R)$ of an $R$-module $M$ with the space of finitely supported functions $\iota \to_{\text{f}} R$ is linearly equivalent to the space of finitely supported functions $\iota \to_{\text{f}} M$. Here $\iota \to_{\text{f}} R$ denotes functions from $\iota$ to $R$ with finite support, and the equivalence is given by the composition of the linear equivalence `finsuppRight R M R ι` with the linear equivalence induced by the right identity isomorphism `TensorProduct.rid R M`.

TensorProduct.finsuppScalarRight_apply_tmul_apply theorem

(m : M) (p : ι →₀ R) (i : ι) : finsuppScalarRight R M ι (m ⊗ₜ[R] p) i = p i • m

Full source

@[simp]
lemma finsuppScalarRight_apply_tmul_apply (m : M) (p : ι →₀ R) (i : ι) :
    finsuppScalarRight R M ι (m ⊗ₜ[R] p) i = p i • m := by
  simp [finsuppScalarRight]

Evaluation of Scalar Finsupp-Tensor Equivalence: $\text{finsuppScalarRight}(m \otimes p)(i) = p(i) \cdot m$

Informal description

For any element $m$ in an $R$-module $M$, any finitely supported function $p \colon \iota \to_{\text{f}} R$, and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppScalarRight}_{R,M,\iota}$ at the tensor product $m \otimes p$ and index $i$ is equal to the scalar multiplication of $m$ by $p(i)$. That is, \[ \text{finsuppScalarRight}_{R,M,\iota}(m \otimes p)(i) = p(i) \cdot m. \]

TensorProduct.finsuppScalarRight_apply_tmul theorem

(m : M) (p : ι →₀ R) : finsuppScalarRight R M ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m)

Full source

lemma finsuppScalarRight_apply_tmul (m : M) (p : ι →₀ R) :
    finsuppScalarRight R M ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m) := by
  ext i
  rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne) (by simp), Finsupp.single_eq_same]

Linear equivalence $\text{finsuppScalarRight}(m \otimes p) = \sum_i \text{single}_i (p(i) \cdot m)$

Informal description

For any element $m$ in an $R$-module $M$ and any finitely supported function $p \colon \iota \to_{\text{f}} R$, the image of the tensor product $m \otimes p$ under the linear equivalence $\text{finsuppScalarRight}_{R,M,\iota}$ is equal to the finite sum $\sum_{i \in \iota} \text{single}_i (p(i) \cdot m)$, where $\text{single}_i$ denotes the function that takes the value $p(i) \cdot m$ at $i$ and zero elsewhere.

TensorProduct.finsuppScalarRight_apply theorem

 (t : M ⊗[R] (ι →₀ R)) (i : ι) : finsuppScalarRight R M ι t i = TensorProduct.rid R M ((Finsupp.lapply i).lTensor M t)

Full source

lemma finsuppScalarRight_apply (t : M ⊗[R] (ι →₀ R)) (i : ι) :
    finsuppScalarRight R M ι t i = TensorProduct.rid R M ((Finsupp.lapply i).lTensor M t) := by
  simp [finsuppScalarRight, finsuppRight_apply]

Evaluation of Scalar Finsupp-Tensor Equivalence via Right Identity and Left Tensor Action

Informal description

For any element $t$ in the tensor product $M \otimes_R (\iota \to_{\text{f}} R)$ and any index $i \in \iota$, the evaluation of the linear equivalence $\text{finsuppScalarRight}_{R,M,\iota}(t)$ at $i$ is equal to the right identity isomorphism $\text{rid}_{R,M}$ applied to the left tensor product of the linear map $\text{lapply}_i$ with $M$ evaluated at $t$. That is, \[ \text{finsuppScalarRight}_{R,M,\iota}(t)(i) = \text{rid}_{R,M}(\text{lTensor}_M(\text{lapply}_i)(t)). \]

TensorProduct.finsuppScalarRight_symm_apply_single theorem

(i : ι) (m : M) : (finsuppScalarRight R M ι).symm (Finsupp.single i m) = m ⊗ₜ[R] (Finsupp.single i 1)

Full source

@[simp]
lemma finsuppScalarRight_symm_apply_single (i : ι) (m : M) :
    (finsuppScalarRight R M ι).symm (Finsupp.single i m) =
      m ⊗ₜ[R] (Finsupp.single i 1) := by
  simp [finsuppScalarRight, finsuppRight_symm_apply_single]

Inverse of Scalar Finsupp Equivalence Maps Single Function to Tensor Product: $(finsuppScalarRight)^{-1}(\text{single}_i(m)) = m \otimes_R \text{single}_i(1)$

Informal description

For any index $i \in \iota$ and element $m \in M$, the inverse of the linear equivalence `finsuppScalarRight` maps the finitely supported function $\text{single}_i(m)$ to the tensor product $m \otimes_R \text{single}_i(1)$, where $\text{single}_i$ denotes the function that is $1$ at $i$ and $0$ elsewhere, and $\otimes_R$ denotes the tensor product over the ring $R$.

Finsupp.linearCombination_one_tmul theorem

 [DecidableEq ι] {v : ι → M} :
  (linearCombination S ((1 : S) ⊗ₜ[R] v ·)).restrictScalars R =
    (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R S ι).symm

Full source

theorem Finsupp.linearCombination_one_tmul [DecidableEq ι] {v : ι → M} :
    (linearCombination S ((1 : S) ⊗ₜ[R] v ·)).restrictScalars R =
      (linearCombination R v).lTensor S ∘ₗ (finsuppScalarRight R S ι).symm := by
  ext; simp [smul_tmul']

Restriction of Linear Combination with Unit Tensor Equals Tensor Product of Linear Combination Composed with Scalar Finsupp Inverse

Informal description

Let $R$ be a commutative ring, $S$ an $R$-algebra, $M$ an $R$-module, and $\iota$ a type with decidable equality. For any function $v : \iota \to M$, the linear combination map $$(1 \otimes_R v(\cdot)) : \iota \to S \otimes_R M$$ when restricted to $R$-scalars, equals the composition of: 1. The linear combination map $(v(\cdot)) : \iota \to M$ tensored with $S$ on the left, and 2. The inverse of the linear equivalence $S \otimes_R (\iota \to_{\text{f}} R) \simeq \iota \to_{\text{f}} S$. In symbols: $$\text{linearCombination}_S(1 \otimes_R v(\cdot))|_R = (\text{linearCombination}_R(v)) \otimes_R S \circ (\text{finsuppScalarRight } R S \iota)^{-1}$$

finsuppTensorFinsupp definition

: (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N

Full source

/-- The tensor product of `ι →₀ M` and `κ →₀ N` is linearly equivalent to `(ι × κ) →₀ (M ⊗ N)`. -/
def finsuppTensorFinsupp : (ι →₀ M) ⊗[R] (κ →₀ N)(ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[S] ι × κ →₀ M ⊗[R] N :=
  TensorProduct.AlgebraTensorModule.congrTensorProduct.AlgebraTensorModule.congr
    (finsuppLEquivDirectSum S M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ
    ((TensorProduct.directSum R S (fun _ : ι => M) fun _ : κ => N) ≪≫ₗ
      (finsuppLEquivDirectSum S (M ⊗[R] N) (ι × κ)).symm)

Linear equivalence between tensor product of finitely supported functions and finitely supported functions on product index set

Informal description

The tensor product of the spaces of finitely supported functions $\iota \to M$ and $\kappa \to N$ is linearly equivalent to the space of finitely supported functions $\iota \times \kappa \to M \otimes_R N$. More precisely, given a commutative ring $R$, a commutative ring $S$, an $R$-module $M$, an $S$-module $N$, and index types $\iota$ and $\kappa$, there is a linear equivalence between the tensor product $(\iota \to_{\text{f}} M) \otimes_R (\kappa \to_{\text{f}} N)$ and the space of finitely supported functions $(\iota \times \kappa) \to_{\text{f}} (M \otimes_R N)$. This equivalence maps a tensor product of single-element functions $f_i \otimes g_k$ (where $f_i$ is supported at $i \in \iota$ and $g_k$ is supported at $k \in \kappa$) to the single-element function supported at $(i,k)$ with value $f_i \otimes g_k$.

finsuppTensorFinsupp_single theorem

 (i : ι) (m : M) (k : κ) (n : N) :
  finsuppTensorFinsupp R S M N ι κ (Finsupp.single i m ⊗ₜ Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ n)

Full source

@[simp]
theorem finsuppTensorFinsupp_single (i : ι) (m : M) (k : κ) (n : N) :
    finsuppTensorFinsupp R S M N ι κ (Finsupp.singleFinsupp.single i m ⊗ₜ Finsupp.single k n) =
      Finsupp.single (i, k) (m ⊗ₜ n) := by
  simp [finsuppTensorFinsupp]

Tensor Product of Single-Element Functions Maps to Single-Element Function on Product Index

Informal description

For any index $i \in \iota$, element $m \in M$, index $k \in \kappa$, and element $n \in N$, the linear equivalence `finsuppTensorFinsupp` maps the tensor product of the single-element functions $\text{Finsupp.single}(i, m) \otimes \text{Finsupp.single}(k, n)$ to the single-element function $\text{Finsupp.single}((i, k), m \otimes n)$ supported at $(i, k)$ with value $m \otimes n$.

finsuppTensorFinsupp_apply theorem

 (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) : finsuppTensorFinsupp R S M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k

Full source

@[simp]
theorem finsuppTensorFinsupp_apply (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
    finsuppTensorFinsupp R S M N ι κ (f ⊗ₜ g) (i, k) = f i ⊗ₜ g k := by
  induction f using Finsupp.induction_linear with
  | zero => simp
  | add f₁ f₂ hf₁ hf₂ => simp [add_tmul, hf₁, hf₂]
  | single i' m =>
    induction g using Finsupp.induction_linear with
    | zero => simp
    | add g₁ g₂ hg₁ hg₂ => simp [tmul_add, hg₁, hg₂]
    | single k' n =>
      classical
      simp_rw [finsuppTensorFinsupp_single, Finsupp.single_apply, Prod.mk_inj, ite_and]
      split_ifs <;> simp

Evaluation of Tensor Product of Finitely Supported Functions at a Pair of Indices

Informal description

For any finitely supported functions $f \colon \iota \to_{\text{f}} M$ and $g \colon \kappa \to_{\text{f}} N$, and any indices $i \in \iota$ and $k \in \kappa$, the evaluation of the linear equivalence $\text{finsuppTensorFinsupp}$ at the tensor product $f \otimes g$ and the pair $(i,k)$ is equal to the tensor product of the evaluations $f(i) \otimes g(k)$. In mathematical notation: $$\text{finsuppTensorFinsupp}_{R,S,M,N,\iota,\kappa}(f \otimes g)(i,k) = f(i) \otimes g(k).$$

finsuppTensorFinsupp_symm_single theorem

 (i : ι × κ) (m : M) (n : N) :
  (finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m ⊗ₜ n)) = Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 n

Full source

@[simp]
theorem finsuppTensorFinsupp_symm_single (i : ι × κ) (m : M) (n : N) :
    (finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m ⊗ₜ n)) =
      Finsupp.singleFinsupp.single i.1 m ⊗ₜ Finsupp.single i.2 n :=
  Prod.casesOn i fun _ _ =>
    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsupp_single _ _ _ _ _ _ _ _ _ _).symm

Inverse of `finsuppTensorFinsupp` on Single-Element Functions: $\text{Finsupp.single}(i, m \otimes n) \mapsto \text{Finsupp.single}(i_1, m) \otimes \text{Finsupp.single}(i_2, n)$

Informal description

For any pair of indices $i = (i_1, i_2) \in \iota \times \kappa$, elements $m \in M$ and $n \in N$, the inverse of the linear equivalence `finsuppTensorFinsupp` maps the single-element function $\text{Finsupp.single}(i, m \otimes n)$ to the tensor product of the single-element functions $\text{Finsupp.single}(i_1, m) \otimes \text{Finsupp.single}(i_2, n)$.

finsuppTensorFinsuppLid definition

: (ι →₀ R) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ N

Full source

/-- A variant of `finsuppTensorFinsupp` where the first module is the ground ring. -/
def finsuppTensorFinsuppLid : (ι →₀ R) ⊗[R] (κ →₀ N)(ι →₀ R) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ N :=
  finsuppTensorFinsuppfinsuppTensorFinsupp R R R N ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl _) (TensorProduct.lid R N)

Linear equivalence between tensor product of scalar finitely supported functions and finitely supported functions on product index set

Informal description

The tensor product of the space of finitely supported functions $\iota \to R$ and the space of finitely supported functions $\kappa \to N$ is linearly equivalent to the space of finitely supported functions $\iota \times \kappa \to N$ over the ring $R$. More precisely, given a commutative ring $R$, an $R$-module $N$, and index types $\iota$ and $\kappa$, there is a linear equivalence between the tensor product $(\iota \to_{\text{f}} R) \otimes_R (\kappa \to_{\text{f}} N)$ and the space of finitely supported functions $(\iota \times \kappa) \to_{\text{f}} N$. This equivalence maps a tensor product of single-element functions $f_i \otimes g_k$ (where $f_i$ is supported at $i \in \iota$ and $g_k$ is supported at $k \in \kappa$) to the single-element function supported at $(i,k)$ with value $f_i(i) \cdot g_k(k)$ (scalar multiplication in $N$).

finsuppTensorFinsuppLid_apply_apply theorem

 (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) : finsuppTensorFinsuppLid R N ι κ (f ⊗ₜ[R] g) (a, b) = f a • g b

Full source

@[simp]
theorem finsuppTensorFinsuppLid_apply_apply (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) :
    finsuppTensorFinsuppLid R N ι κ (f ⊗ₜ[R] g) (a, b) = f a • g b := by
  simp [finsuppTensorFinsuppLid]

Evaluation of Tensor Product of Scalar Finitely Supported Functions at a Pair of Indices: $f \otimes g \mapsto f(a) \cdot g(b)$

Informal description

For any finitely supported functions $f \colon \iota \to_{\text{f}} R$ and $g \colon \kappa \to_{\text{f}} N$, and any indices $a \in \iota$ and $b \in \kappa$, the evaluation of the linear equivalence $\text{finsuppTensorFinsuppLid}$ at the tensor product $f \otimes_R g$ and the pair $(a,b)$ is equal to the scalar multiplication of $f(a)$ and $g(b)$. In mathematical notation: $$\text{finsuppTensorFinsuppLid}_{R,N,\iota,\kappa}(f \otimes_R g)(a,b) = f(a) \cdot g(b).$$

finsuppTensorFinsuppLid_single_tmul_single theorem

 (a : ι) (b : κ) (r : R) (n : N) :
  finsuppTensorFinsuppLid R N ι κ (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = Finsupp.single (a, b) (r • n)

Full source

@[simp]
theorem finsuppTensorFinsuppLid_single_tmul_single (a : ι) (b : κ) (r : R) (n : N) :
    finsuppTensorFinsuppLid R N ι κ (Finsupp.singleFinsupp.single a r ⊗ₜ[R] Finsupp.single b n) =
      Finsupp.single (a, b) (r • n) := by
  simp [finsuppTensorFinsuppLid]

Tensor product of single-element functions maps to single-element function under scalar action

Informal description

For any index $a \in \iota$, index $b \in \kappa$, scalar $r \in R$, and element $n \in N$, the linear equivalence `finsuppTensorFinsuppLid` maps the tensor product of the single-element functions $\text{Finsupp.single}(a, r) \otimes_R \text{Finsupp.single}(b, n)$ to the single-element function $\text{Finsupp.single}((a, b), r \cdot n)$ supported at $(a, b)$ with value $r \cdot n$.

finsuppTensorFinsuppLid_symm_single_smul theorem

 (i : ι × κ) (r : R) (n : N) :
  (finsuppTensorFinsuppLid R N ι κ).symm (Finsupp.single i (r • n)) = Finsupp.single i.1 r ⊗ₜ Finsupp.single i.2 n

Full source

@[simp]
theorem finsuppTensorFinsuppLid_symm_single_smul (i : ι × κ) (r : R) (n : N) :
    (finsuppTensorFinsuppLid R N ι κ).symm (Finsupp.single i (r • n)) =
      Finsupp.singleFinsupp.single i.1 r ⊗ₜ Finsupp.single i.2 n :=
  Prod.casesOn i fun _ _ =>
    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppLid_single_tmul_single ..).symm

Inverse of Linear Equivalence Maps Scalar Multiple of Single-Element Function to Tensor Product of Single-Element Functions

Informal description

For any pair of indices $i = (a, b) \in \iota \times \kappa$, scalar $r \in R$, and element $n \in N$, the inverse of the linear equivalence `finsuppTensorFinsuppLid` maps the single-element function $\text{Finsupp.single}(i, r \cdot n)$ to the tensor product $\text{Finsupp.single}(a, r) \otimes_R \text{Finsupp.single}(b, n)$.

finsuppTensorFinsuppRid definition

: (ι →₀ M) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ M

Full source

/-- A variant of `finsuppTensorFinsupp` where the second module is the ground ring. -/
def finsuppTensorFinsuppRid : (ι →₀ M) ⊗[R] (κ →₀ R)(ι →₀ M) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ M :=
  finsuppTensorFinsuppfinsuppTensorFinsupp R R M R ι κ ≪≫ₗ Finsupp.lcongr (Equiv.refl _) (TensorProduct.rid R M)

Linear equivalence between tensor product of finitely supported functions and finitely supported functions on product index set (right ground ring case)

Informal description

The tensor product of the space of finitely supported functions $\iota \to M$ and the space of finitely supported functions $\kappa \to R$ is linearly equivalent to the space of finitely supported functions $\iota \times \kappa \to M$. More precisely, given a commutative ring $R$, an $R$-module $M$, and index types $\iota$ and $\kappa$, there is a linear equivalence between the tensor product $(\iota \to_{\text{f}} M) \otimes_R (\kappa \to_{\text{f}} R)$ and the space of finitely supported functions $(\iota \times \kappa) \to_{\text{f}} M$. This equivalence maps a tensor product of single-element functions $f_i \otimes g_k$ (where $f_i$ is supported at $i \in \iota$ and $g_k$ is supported at $k \in \kappa$) to the single-element function supported at $(i,k)$ with value $g_k(k) \cdot f_i(i)$.

finsuppTensorFinsuppRid_apply_apply theorem

 (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) : finsuppTensorFinsuppRid R M ι κ (f ⊗ₜ[R] g) (a, b) = g b • f a

Full source

@[simp]
theorem finsuppTensorFinsuppRid_apply_apply (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) :
    finsuppTensorFinsuppRid R M ι κ (f ⊗ₜ[R] g) (a, b) = g b • f a := by
  simp [finsuppTensorFinsuppRid]

Evaluation of Tensor Product of Finitely Supported Functions at a Pair of Indices (Right Ground Ring Case)

Informal description

For any finitely supported functions $f \colon \iota \to_{\text{f}} M$ and $g \colon \kappa \to_{\text{f}} R$, and any indices $a \in \iota$ and $b \in \kappa$, the evaluation of the linear equivalence $\text{finsuppTensorFinsuppRid}_{R,M,\iota,\kappa}$ at the tensor product $f \otimes g$ and the pair $(a,b)$ is equal to the scalar multiple $g(b) \cdot f(a)$. In mathematical notation: $$\text{finsuppTensorFinsuppRid}_{R,M,\iota,\kappa}(f \otimes g)(a,b) = g(b) \cdot f(a).$$

finsuppTensorFinsuppRid_single_tmul_single theorem

 (a : ι) (b : κ) (m : M) (r : R) :
  finsuppTensorFinsuppRid R M ι κ (Finsupp.single a m ⊗ₜ[R] Finsupp.single b r) = Finsupp.single (a, b) (r • m)

Full source

@[simp]
theorem finsuppTensorFinsuppRid_single_tmul_single (a : ι) (b : κ) (m : M) (r : R) :
    finsuppTensorFinsuppRid R M ι κ (Finsupp.singleFinsupp.single a m ⊗ₜ[R] Finsupp.single b r) =
      Finsupp.single (a, b) (r • m) := by
  simp [finsuppTensorFinsuppRid]

Tensor product of single-element functions maps to scaled single-element function on product index set

Informal description

For any indices $a \in \iota$ and $b \in \kappa$, any element $m \in M$, and any scalar $r \in R$, the linear equivalence `finsuppTensorFinsuppRid` maps the tensor product of the single-element functions $\text{Finsupp.single}(a, m) \otimes \text{Finsupp.single}(b, r)$ to the single-element function $\text{Finsupp.single}((a, b), r \cdot m)$ supported at $(a, b)$ with value $r \cdot m$.

finsuppTensorFinsuppRid_symm_single_smul theorem

 (i : ι × κ) (m : M) (r : R) :
  (finsuppTensorFinsuppRid R M ι κ).symm (Finsupp.single i (r • m)) = Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 r

Full source

@[simp]
theorem finsuppTensorFinsuppRid_symm_single_smul (i : ι × κ) (m : M) (r : R) :
    (finsuppTensorFinsuppRid R M ι κ).symm (Finsupp.single i (r • m)) =
      Finsupp.singleFinsupp.single i.1 m ⊗ₜ Finsupp.single i.2 r :=
  Prod.casesOn i fun _ _ =>
    (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppRid_single_tmul_single ..).symm

Inverse of Tensor-Finsupp Equivalence on Scaled Single-Element Functions

Informal description

For any index pair $i = (a, b) \in \iota \times \kappa$, any element $m \in M$, and any scalar $r \in R$, the inverse of the linear equivalence `finsuppTensorFinsuppRid` maps the single-element function $\text{Finsupp.single}(i, r \cdot m)$ to the tensor product $\text{Finsupp.single}(a, m) \otimes \text{Finsupp.single}(b, r)$.

finsuppTensorFinsupp' definition

: (ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R

Full source

/-- A variant of `finsuppTensorFinsupp` where both modules are the ground ring. -/
def finsuppTensorFinsupp' : (ι →₀ R) ⊗[R] (κ →₀ R)(ι →₀ R) ⊗[R] (κ →₀ R) ≃ₗ[R] ι × κ →₀ R :=
  finsuppTensorFinsuppLid R R ι κ

Linear equivalence between tensor product of scalar finitely supported functions and finitely supported functions on product index set

Informal description

The tensor product of the space of finitely supported functions $\iota \to R$ and the space of finitely supported functions $\kappa \to R$ is linearly equivalent to the space of finitely supported functions $\iota \times \kappa \to R$ over the ring $R$. More precisely, given a commutative ring $R$ and index types $\iota$ and $\kappa$, there is a linear equivalence between the tensor product $(\iota \to_{\text{f}} R) \otimes_R (\kappa \to_{\text{f}} R)$ and the space of finitely supported functions $(\iota \times \kappa) \to_{\text{f}} R$. This equivalence maps a tensor product of single-element functions $f_i \otimes g_k$ (where $f_i$ is supported at $i \in \iota$ and $g_k$ is supported at $k \in \kappa$) to the single-element function supported at $(i,k)$ with value $f_i(i) \cdot g_k(k)$ (multiplication in $R$).

finsuppTensorFinsupp'_apply_apply theorem

 (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) : finsuppTensorFinsupp' R ι κ (f ⊗ₜ[R] g) (a, b) = f a * g b

Full source

@[simp]
theorem finsuppTensorFinsupp'_apply_apply (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) :
    finsuppTensorFinsupp' R ι κ (f ⊗ₜ[R] g) (a, b) = f a * g b :=
  finsuppTensorFinsuppLid_apply_apply R R ι κ f g a b

Evaluation of Tensor Product of Finitely Supported Functions at a Pair of Indices: $f \otimes g \mapsto f(a) \cdot g(b)$

Informal description

For any finitely supported functions $f \colon \iota \to_{\text{f}} R$ and $g \colon \kappa \to_{\text{f}} R$, and any indices $a \in \iota$ and $b \in \kappa$, the evaluation of the linear equivalence $\text{finsuppTensorFinsupp'}$ at the tensor product $f \otimes_R g$ and the pair $(a,b)$ is equal to the product $f(a) \cdot g(b)$ in $R$. In mathematical notation: $$\text{finsuppTensorFinsupp'}_{R,\iota,\kappa}(f \otimes_R g)(a,b) = f(a) \cdot g(b).$$

finsuppTensorFinsupp'_single_tmul_single theorem

 (a : ι) (b : κ) (r₁ r₂ : R) :
  finsuppTensorFinsupp' R ι κ (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)

Full source

@[simp]
theorem finsuppTensorFinsupp'_single_tmul_single (a : ι) (b : κ) (r₁ r₂ : R) :
    finsuppTensorFinsupp' R ι κ (Finsupp.singleFinsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) =
      Finsupp.single (a, b) (r₁ * r₂) :=
  finsuppTensorFinsuppLid_single_tmul_single R R ι κ a b r₁ r₂

Tensor product of single-element functions maps to product-valued single-element function

Informal description

For any indices $a \in \iota$ and $b \in \kappa$, and any scalars $r_1, r_2 \in R$, the linear equivalence `finsuppTensorFinsupp'` maps the tensor product of the single-element functions $\text{single}(a, r_1) \otimes_R \text{single}(b, r_2)$ to the single-element function $\text{single}((a, b), r_1 \cdot r_2)$ supported at $(a, b)$ with value $r_1 \cdot r_2$.

finsuppTensorFinsupp'_symm_single_mul theorem

 (i : ι × κ) (r₁ r₂ : R) :
  (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r₁ * r₂)) = Finsupp.single i.1 r₁ ⊗ₜ Finsupp.single i.2 r₂

Full source

theorem finsuppTensorFinsupp'_symm_single_mul (i : ι × κ) (r₁ r₂ : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r₁ * r₂)) =
      Finsupp.singleFinsupp.single i.1 r₁ ⊗ₜ Finsupp.single i.2 r₂ :=
  finsuppTensorFinsuppLid_symm_single_smul R R ι κ i r₁ r₂

Inverse Linear Equivalence Maps Product-Valued Single-Element Function to Tensor Product of Single-Element Functions

Informal description

For any pair of indices $i = (a, b) \in \iota \times \kappa$ and any scalars $r_1, r_2 \in R$, the inverse of the linear equivalence `finsuppTensorFinsupp'` maps the single-element function supported at $i$ with value $r_1 \cdot r_2$ to the tensor product of the single-element functions $\text{single}(a, r_1) \otimes_R \text{single}(b, r_2)$. In symbols: $$(finsuppTensorFinsupp'\, R\, \iota\, \kappa)^{-1}(\text{single}(i, r_1 \cdot r_2)) = \text{single}(a, r_1) \otimes_R \text{single}(b, r_2)$$

finsuppTensorFinsupp'_symm_single_eq_single_one_tmul theorem

 (i : ι × κ) (r : R) :
  (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ Finsupp.single i.2 r

Full source

theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul (i : ι × κ) (r : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) =
      Finsupp.singleFinsupp.single i.1 1 ⊗ₜ Finsupp.single i.2 r := by
  nth_rw 1 [← one_mul r]
  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Inverse Linear Equivalence Maps Single-Element Function to Tensor Product with Unit Coefficient

Informal description

For any pair of indices $i = (a, b) \in \iota \times \kappa$ and any scalar $r \in R$, the inverse of the linear equivalence $\text{finsuppTensorFinsupp'}$ maps the single-element function supported at $i$ with value $r$ to the tensor product of the single-element functions $\text{single}(a, 1) \otimes_R \text{single}(b, r)$. In symbols: $$(\text{finsuppTensorFinsupp'}\, R\, \iota\, \kappa)^{-1}(\text{single}(i, r)) = \text{single}(a, 1) \otimes_R \text{single}(b, r)$$

finsuppTensorFinsupp'_symm_single_eq_tmul_single_one theorem

 (i : ι × κ) (r : R) :
  (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ Finsupp.single i.2 1

Full source

theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one (i : ι × κ) (r : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) =
      Finsupp.singleFinsupp.single i.1 r ⊗ₜ Finsupp.single i.2 1 := by
  nth_rw 1 [← mul_one r]
  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

Inverse Tensor Equivalence Maps Single-Element Function to Tensor Product with Unit Function

Informal description

For any pair of indices $i = (a, b) \in \iota \times \kappa$ and any scalar $r \in R$, the inverse of the linear equivalence $\text{finsuppTensorFinsupp}'$ maps the single-element function supported at $i$ with value $r$ to the tensor product of the single-element function $\text{single}(a, r)$ and the single-element function $\text{single}(b, 1)$. In symbols: $$(\text{finsuppTensorFinsupp}'\, R\, \iota\, \kappa)^{-1}(\text{single}(i, r)) = \text{single}(a, r) \otimes_R \text{single}(b, 1)$$

finsuppTensorFinsuppLid_self theorem

: finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ

Full source

theorem finsuppTensorFinsuppLid_self :
    finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ := rfl

Equality of Linear Equivalences: $\text{finsuppTensorFinsuppLid} = \text{finsuppTensorFinsupp'}$ for Scalar Case

Informal description

For a commutative ring $R$ and index types $\iota$ and $\kappa$, the linear equivalence $\text{finsuppTensorFinsuppLid}$ between $(\iota \to_{\text{f}} R) \otimes_R (\kappa \to_{\text{f}} R)$ and $\iota \times \kappa \to_{\text{f}} R$ coincides with the linear equivalence $\text{finsuppTensorFinsupp'}$ when both are specialized to the case where the module $N$ is $R$ itself.

finsuppTensorFinsuppRid_self theorem

: finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ

Full source

theorem finsuppTensorFinsuppRid_self :
    finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ := by
  rw [finsuppTensorFinsupp', finsuppTensorFinsuppLid, finsuppTensorFinsuppRid,
    TensorProduct.lid_eq_rid]

Equality of Right Ground Ring Tensor Product and Scalar Tensor Product for Finitely Supported Functions

Informal description

For a commutative ring $R$ and index types $\iota$ and $\kappa$, the linear equivalence $\text{finsuppTensorFinsuppRid}_{R,R,\iota,\kappa}$ between $(\iota \to_{\text{f}} R) \otimes_R (\kappa \to_{\text{f}} R)$ and $\iota \times \kappa \to_{\text{f}} R$ coincides with the linear equivalence $\text{finsuppTensorFinsupp}'_{R,\iota,\kappa}$.

Mathlib.LinearAlgebra.DirectSum.Finsupp

Case of MvPolynomial

Case of `Polynomial`

TODO

Case of MvPolynomial

Case of Polynomial

TODO

Case of `Polynomial`