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) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] : TensorProduct R (ι →₀ M) N ≃ₗ[R] ι →₀ TensorProduct R M N

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.

theorem TensorProduct.finsuppLeft_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ M) (n : N) : (finsuppLeft R M 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} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ M) (n : N) (i : ι) : ((finsuppLeft R M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n

theorem TensorProduct.finsuppLeft_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (t : TensorProduct R (ι →₀ M) N) (i : ι) : ((finsuppLeft R M N ι) t) i = (LinearMap.rTensor N (Finsupp.lapply i)) t

@[simp]

theorem TensorProduct.finsuppLeft_symm_apply_single {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (i : ι) (m : M) (n : N) : (finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i m ⊗ₜ[R] n

noncomputable def TensorProduct.finsuppRight (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] : TensorProduct R M (ι →₀ N) ≃ₗ[R] ι →₀ TensorProduct R M N

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.

theorem TensorProduct.finsuppRight_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ N) : (finsuppRight R M 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} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ N) (i : ι) : ((finsuppRight R M N ι) (m ⊗ₜ[R] p)) i = m ⊗ₜ[R] p i

theorem TensorProduct.finsuppRight_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (t : TensorProduct R M (ι →₀ N)) (i : ι) : ((finsuppRight R M N ι) t) i = (LinearMap.lTensor M (Finsupp.lapply i)) t

@[simp]

theorem TensorProduct.finsuppRight_symm_apply_single {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (i : ι) (m : M) (n : N) : (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = m ⊗ₜ[R] Finsupp.single i n

theorem TensorProduct.finsuppLeft_smul' {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] {S : Type u_5} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (s : S) (t : TensorProduct R (ι →₀ M) N) : (finsuppLeft R M N ι) (s • t) = s • (finsuppLeft R M N ι) t

noncomputable def TensorProduct.finsuppLeft' (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] (S : Type u_5) [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] : TensorProduct R (ι →₀ M) N ≃ₗ[S] ι →₀ TensorProduct R M N

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.

theorem TensorProduct.finsuppLeft'_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] {S : Type u_5} [CommSemiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (x : TensorProduct R (ι →₀ M) N) : (finsuppLeft' R M N ι S) x = (finsuppLeft R M N ι) x

noncomputable def TensorProduct.finsuppScalarLeft (R : Type u_1) [CommSemiring R] (N : Type u_3) [AddCommMonoid N] [Module R N] (ι : Type u_4) [DecidableEq ι] : TensorProduct R (ι →₀ R) N ≃ₗ[R] ι →₀ N

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

Equations

• TensorProduct.finsuppScalarLeft R N ι = (TensorProduct.finsuppLeft R R N ι).trans (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))

@[simp]

theorem TensorProduct.finsuppScalarLeft_apply_tmul_apply {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ R) (n : N) (i : ι) : ((finsuppScalarLeft R N ι) (p ⊗ₜ[R] n)) i = p i • n

theorem TensorProduct.finsuppScalarLeft_apply_tmul {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (p : ι →₀ R) (n : N) : (finsuppScalarLeft R N ι) (p ⊗ₜ[R] n) = p.sum fun (i : ι) (m : R) => Finsupp.single i (m • n)

theorem TensorProduct.finsuppScalarLeft_apply {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (pn : TensorProduct R (ι →₀ R) N) (i : ι) : ((finsuppScalarLeft R N ι) pn) i = (TensorProduct.lid R N) ((LinearMap.rTensor N (Finsupp.lapply i)) pn)

@[simp]

theorem TensorProduct.finsuppScalarLeft_symm_apply_single {R : Type u_1} [CommSemiring R] {N : Type u_3} [AddCommMonoid N] [Module R N] {ι : Type u_4} [DecidableEq ι] (i : ι) (n : N) : (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = Finsupp.single i 1 ⊗ₜ[R] n

noncomputable def TensorProduct.finsuppScalarRight (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (ι : Type u_4) [DecidableEq ι] : TensorProduct R M (ι →₀ R) ≃ₗ[R] ι →₀ M

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

Equations

• TensorProduct.finsuppScalarRight R M ι = (TensorProduct.finsuppRight R M R ι).trans (Finsupp.mapRange.linearEquiv (TensorProduct.rid R M))

@[simp]

theorem TensorProduct.finsuppScalarRight_apply_tmul_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ R) (i : ι) : ((finsuppScalarRight R M ι) (m ⊗ₜ[R] p)) i = p i • m

theorem TensorProduct.finsuppScalarRight_apply_tmul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (m : M) (p : ι →₀ R) : (finsuppScalarRight R M ι) (m ⊗ₜ[R] p) = p.sum fun (i : ι) (n : R) => Finsupp.single i (n • m)

theorem TensorProduct.finsuppScalarRight_apply {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (t : TensorProduct R M (ι →₀ R)) (i : ι) : ((finsuppScalarRight R M ι) t) i = (TensorProduct.rid R M) ((LinearMap.lTensor M (Finsupp.lapply i)) t)

@[simp]

theorem TensorProduct.finsuppScalarRight_symm_apply_single {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {ι : Type u_4} [DecidableEq ι] (i : ι) (m : M) : (finsuppScalarRight R M ι).symm (Finsupp.single i m) = m ⊗ₜ[R] Finsupp.single i 1

theorem Finsupp.linearCombination_one_tmul (R : Type u_1) (S : Type u_2) (M : Type u_3) (ι : Type u_5) [CommSemiring R] [AddCommMonoid M] [Module R M] [Semiring S] [Algebra R S] [DecidableEq ι] {v : ι → M} : ↑R (linearCombination S fun (x : ι) => 1 ⊗ₜ[R] v x) = LinearMap.lTensor S (linearCombination R v) ∘ₗ ↑(TensorProduct.finsuppScalarRight R S ι).symm

def finsuppTensorFinsupp (R : Type u_1) (S : Type u_2) (M : Type u_3) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] : TensorProduct R (ι →₀ M) (κ →₀ N) ≃ₗ[S] ι × κ →₀ TensorProduct R M N

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.

@[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) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι) (m : M) (k : κ) (n : N) : (finsuppTensorFinsupp R S M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = 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) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R 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) [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Semiring S] [Algebra R S] [Module S M] [IsScalarTower R S M] (i : ι × κ) (m : M) (n : N) : (finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i.1 m ⊗ₜ[R] Finsupp.single i.2 n

def finsuppTensorFinsuppLid (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] : TensorProduct R (ι →₀ R) (κ →₀ N) ≃ₗ[R] ι × κ →₀ N

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

Equations

• finsuppTensorFinsuppLid R N ι κ = (finsuppTensorFinsupp R R R N ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.lid R N))

@[simp]

theorem finsuppTensorFinsuppLid_apply_apply (R : Type u_1) (N : Type u_4) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid N] [Module R N] (f : ι →₀ R) (g : κ →₀ N) (a : ι) (b : κ) : ((finsuppTensorFinsuppLid R N ι κ) (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) [CommSemiring R] [AddCommMonoid N] [Module R N] (a : ι) (b : κ) (r : R) (n : N) : (finsuppTensorFinsuppLid R N ι κ) (Finsupp.single a r ⊗ₜ[R] Finsupp.single b n) = 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) [CommSemiring R] [AddCommMonoid N] [Module R N] (i : ι × κ) (r : R) (n : N) : (finsuppTensorFinsuppLid R 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) [CommSemiring R] [AddCommMonoid M] [Module R M] : TensorProduct R (ι →₀ M) (κ →₀ R) ≃ₗ[R] ι × κ →₀ M

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

Equations

• finsuppTensorFinsuppRid R M ι κ = (finsuppTensorFinsupp R R M R ι κ).trans (Finsupp.lcongr (Equiv.refl (ι × κ)) (TensorProduct.rid R M))

@[simp]

theorem finsuppTensorFinsuppRid_apply_apply (R : Type u_1) (M : Type u_3) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] [AddCommMonoid M] [Module R M] (f : ι →₀ M) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsuppRid R M ι κ) (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) [CommSemiring R] [AddCommMonoid M] [Module R M] (a : ι) (b : κ) (m : M) (r : R) : (finsuppTensorFinsuppRid R M ι κ) (Finsupp.single a m ⊗ₜ[R] Finsupp.single b 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) [CommSemiring R] [AddCommMonoid M] [Module R M] (i : ι × κ) (m : M) (r : R) : (finsuppTensorFinsuppRid R M ι κ).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) [CommSemiring R] : TensorProduct R (ι →₀ R) (κ →₀ R) ≃ₗ[R] ι × κ →₀ R

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

Equations

• finsuppTensorFinsupp' R ι κ = finsuppTensorFinsuppLid R R ι κ

@[simp]

theorem finsuppTensorFinsupp'_apply_apply (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (f : ι →₀ R) (g : κ →₀ R) (a : ι) (b : κ) : ((finsuppTensorFinsupp' R ι κ) (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) [CommSemiring R] (a : ι) (b : κ) (r₁ r₂ : R) : (finsuppTensorFinsupp' R ι κ) (Finsupp.single a r₁ ⊗ₜ[R] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)

theorem finsuppTensorFinsupp'_symm_single_mul (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] (i : ι × κ) (r₁ r₂ : R) : (finsuppTensorFinsupp' 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) [CommSemiring R] (i : ι × κ) (r : R) : (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = 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) [CommSemiring R] (i : ι × κ) (r : R) : (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 r ⊗ₜ[R] Finsupp.single i.2 1

theorem finsuppTensorFinsuppLid_self (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsuppLid R R ι κ = finsuppTensorFinsupp' R ι κ

theorem finsuppTensorFinsuppRid_self (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [CommSemiring R] : finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ