# Results on finitely supported functions. #

• TensorProduct.finsuppLeft, the tensor product of ι →₀ M and N is linearly equivalent to ι →₀ M ⊗[R] N

• TensorProduct.finsuppScalarLeft, the tensor product of ι →₀ R and N is linearly equivalent to ι →₀ N

• TensorProduct.finsuppRight, the tensor product of M and ι →₀ N is linearly equivalent to ι →₀ M ⊗[R] N

• TensorProduct.finsuppScalarRight, the tensor product of M and ι →₀ R is linearly equivalent to ι →₀ N

• TensorProduct.finsuppLeft', if M is an S-module, then the tensor product of ι →₀ M and N is S-linearly equivalent to ι →₀ M ⊗[R] N

• finsuppTensorFinsupp, the tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).

## Case of MvPolynomial #

These functions apply to MvPolynomial, one can define

noncomputable def MvPolynomial.rTensor' :
MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) :=
TensorProduct.finsuppLeft'

noncomputable def MvPolynomial.rTensor :
MvPolynomial σ R ⊗[R] N ≃ₗ[R] (σ →₀ ℕ) →₀ N :=
TensorProduct.finsuppScalarLeft


However, to be actually usable, these definitions need lemmas to be given in companion PR.

## Case of Polynomial#

Polynomial is a structure containing a Finsupp, so these functions can't be applied directly to Polynomial.

Some linear equivs need to be added to mathlib for that. This belongs to a companion PR.

## TODO #

• generalize to MonoidAlgebra, AlgHom

• reprove TensorProduct.finsuppLeft' using existing heterobasic version of TensorProduct.congr

noncomputable def TensorProduct.finsuppLeft (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_4) [] :

The tensor product of ι →₀ M and N is linearly equivalent to ι →₀ M ⊗[R] N

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TensorProduct.finsuppLeft_apply_tmul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (p : ι →₀ M) (n : N) :
() (p ⊗ₜ[R] n) = p.sum fun (i : ι) (m : M) => Finsupp.single i (m ⊗ₜ[R] n)
@[simp]
theorem TensorProduct.finsuppLeft_apply_tmul_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (p : ι →₀ M) (n : N) (i : ι) :
(() (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n
theorem TensorProduct.finsuppLeft_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (t : TensorProduct R (ι →₀ M) N) (i : ι) :
(() t) i = () t
@[simp]
theorem TensorProduct.finsuppLeft_symm_apply_single {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (i : ι) (m : M) (n : N) :
().symm (Finsupp.single i (m ⊗ₜ[R] n)) = ⊗ₜ[R] n
noncomputable def TensorProduct.finsuppRight (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_4) [] :

The tensor product of M and ι →₀ N is linearly equivalent to ι →₀ M ⊗[R] N

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TensorProduct.finsuppRight_apply_tmul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (m : M) (p : ι →₀ N) :
() (m ⊗ₜ[R] p) = p.sum fun (i : ι) (n : N) => Finsupp.single i (m ⊗ₜ[R] n)
@[simp]
theorem TensorProduct.finsuppRight_apply_tmul_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (m : M) (p : ι →₀ N) (i : ι) :
(() (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i
theorem TensorProduct.finsuppRight_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (t : TensorProduct R M (ι →₀ N)) (i : ι) :
(() t) i = () t
@[simp]
theorem TensorProduct.finsuppRight_symm_apply_single {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (i : ι) (m : M) (n : N) :
().symm (Finsupp.single i (m ⊗ₜ[R] n)) = m ⊗ₜ[R]
theorem TensorProduct.finsuppLeft_smul' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] {S : Type u_5} [] [Algebra R S] [Module S M] [] (s : S) (t : TensorProduct R (ι →₀ M) N) :
() (s t) = s () t
noncomputable def TensorProduct.finsuppLeft' (R : Type u_1) [] (M : Type u_2) [] [Module R M] (N : Type u_3) [] [Module R N] (ι : Type u_4) [] (S : Type u_5) [] [Algebra R S] [Module S M] [] :

When M is also an S-module, then TensorProduct.finsuppLeft R M N is an S-linear equiv

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem TensorProduct.finsuppLeft'_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] {S : Type u_5} [] [Algebra R S] [Module S M] [] (x : TensorProduct R (ι →₀ M) N) :
() x = () x
noncomputable def TensorProduct.finsuppScalarLeft (R : Type u_1) [] (N : Type u_3) [] [Module R N] (ι : Type u_4) [] :

The tensor product of ι →₀ R and N is linearly equivalent to ι →₀ N

Equations
• = ().trans
Instances For
@[simp]
theorem TensorProduct.finsuppScalarLeft_apply_tmul_apply {R : Type u_1} [] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (p : ι →₀ R) (n : N) (i : ι) :
(() (p ⊗ₜ[R] n)) i = p i n
theorem TensorProduct.finsuppScalarLeft_apply_tmul {R : Type u_1} [] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (p : ι →₀ R) (n : N) :
() (p ⊗ₜ[R] n) = p.sum fun (i : ι) (m : R) => Finsupp.single i (m n)
theorem TensorProduct.finsuppScalarLeft_apply {R : Type u_1} [] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (pn : TensorProduct R (ι →₀ R) N) (i : ι) :
(() pn) i = () (() pn)
@[simp]
theorem TensorProduct.finsuppScalarLeft_symm_apply_single {R : Type u_1} [] {N : Type u_3} [] [Module R N] {ι : Type u_4} [] (i : ι) (n : N) :
().symm () = ⊗ₜ[R] n
noncomputable def TensorProduct.finsuppScalarRight (R : Type u_1) [] (M : Type u_2) [] [Module R M] (ι : Type u_4) [] :

The tensor product of M and ι →₀ R is linearly equivalent to ι →₀ N

Equations
• = ().trans
Instances For
@[simp]
theorem TensorProduct.finsuppScalarRight_apply_tmul_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_4} [] (m : M) (p : ι →₀ R) (i : ι) :
(() (m ⊗ₜ[R] p)) i = p i m
theorem TensorProduct.finsuppScalarRight_apply_tmul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_4} [] (m : M) (p : ι →₀ R) :
() (m ⊗ₜ[R] p) = p.sum fun (i : ι) (n : R) => Finsupp.single i (n m)
theorem TensorProduct.finsuppScalarRight_apply {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_4} [] (t : TensorProduct R M (ι →₀ R)) (i : ι) :
(() t) i = () (() t)
@[simp]
theorem TensorProduct.finsuppScalarRight_symm_apply_single {R : Type u_1} [] {M : Type u_2} [] [Module R M] {ι : Type u_4} [] (i : ι) (m : M) :
().symm () = m ⊗ₜ[R]
def finsuppTensorFinsupp (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] [] [Module R N] [] [Algebra R S] [Module S M] [] :
TensorProduct R (ι →₀ M) (κ →₀ N) ≃ₗ[S] ι × κ →₀

The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem finsuppTensorFinsupp_single (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] [] [Module R N] [] [Algebra R S] [Module S M] [] (i : ι) (m : M) (k : κ) (n : N) :
(finsuppTensorFinsupp R S M N ι κ) ( ⊗ₜ[R] ) = Finsupp.single (i, k) (m ⊗ₜ[R] n)
@[simp]
theorem finsuppTensorFinsupp_apply (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] [] [Module R N] [] [Algebra R S] [Module S M] [] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
((finsuppTensorFinsupp R S M N ι κ) (f ⊗ₜ[R] g)) (i, k) = f i ⊗ₜ[R] g k
@[simp]
theorem finsuppTensorFinsupp_symm_single (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] [] [Module R N] [] [Algebra R S] [Module S M] [] (i : ι × κ) (m : M) (n : N) :
def finsuppTensorFinsuppLid (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R N] :
TensorProduct R (ι →₀ R) (κ →₀ N) ≃ₗ[R] ι × κ →₀ N

A variant of finsuppTensorFinsupp where the first module is the ground ring.

Equations
Instances For
@[simp]
theorem finsuppTensorFinsuppLid_apply_apply (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) :
(() (f ⊗ₜ[R] g)) (a, b) = f a g b
@[simp]
theorem finsuppTensorFinsuppLid_single_tmul_single (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R N] (a : ι) (b : κ) (r : R) (n : N) :
() ( ⊗ₜ[R] ) = Finsupp.single (a, b) (r n)
@[simp]
theorem finsuppTensorFinsuppLid_symm_single_smul (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [] [] [Module R N] (i : ι × κ) (r : R) (n : N) :
().symm (Finsupp.single i (r n)) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 n
def finsuppTensorFinsuppRid (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] :
TensorProduct R (ι →₀ M) (κ →₀ R) ≃ₗ[R] ι × κ →₀ M

A variant of finsuppTensorFinsupp where the second module is the ground ring.

Equations
Instances For
@[simp]
theorem finsuppTensorFinsuppRid_apply_apply (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) :
(() (f ⊗ₜ[R] g)) (a, b) = g b f a
@[simp]
theorem finsuppTensorFinsuppRid_single_tmul_single (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] (a : ι) (b : κ) (m : M) (r : R) :
() ( ⊗ₜ[R] ) = Finsupp.single (a, b) (r m)
@[simp]
theorem finsuppTensorFinsuppRid_symm_single_smul (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [] [] [Module R M] (i : ι × κ) (m : M) (r : R) :
().symm (Finsupp.single i (r m)) = Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 r
def finsuppTensorFinsupp' (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] :
TensorProduct R (ι →₀ R) (κ →₀ R) ≃ₗ[R] ι × κ →₀ R

A variant of finsuppTensorFinsupp` where both modules are the ground ring.

Equations
Instances For
@[simp]
theorem finsuppTensorFinsupp'_apply_apply (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) :
(() (f ⊗ₜ[R] g)) (a, b) = f a * g b
@[simp]
theorem finsuppTensorFinsupp'_single_tmul_single (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] (a : ι) (b : κ) (r₁ : R) (r₂ : R) :
() ( ⊗ₜ[R] ) = Finsupp.single (a, b) (r₁ * r₂)
theorem finsuppTensorFinsupp'_symm_single_mul (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] (i : ι × κ) (r₁ : R) (r₂ : R) :
().symm (Finsupp.single i (r₁ * r₂)) = Finsupp.single i.1 r₁ ⊗ₜ[R] Finsupp.single i.2 r₂
theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] (i : ι × κ) (r : R) :
().symm () = Finsupp.single i.1 1 ⊗ₜ[R] Finsupp.single i.2 r
theorem finsuppTensorFinsupp'_symm_single_eq_tmul_single_one (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] (i : ι × κ) (r : R) :
().symm () = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1
theorem finsuppTensorFinsuppLid_self (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] :
=
theorem finsuppTensorFinsuppRid_self (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [] :
=