Results on finitely supported functions. #
TensorProduct.finsuppLeft, the tensor product ofι →₀ MandNis linearly equivalent toι →₀ M ⊗[R] NTensorProduct.finsuppScalarLeft, the tensor product ofι →₀ RandNis linearly equivalent toι →₀ NTensorProduct.finsuppRight, the tensor product ofMandι →₀ Nis linearly equivalent toι →₀ M ⊗[R] NTensorProduct.finsuppScalarRight, the tensor product ofMandι →₀ Ris linearly equivalent toι →₀ NTensorProduct.finsuppLeft', ifMis anS-module, then the tensor product ofι →₀ MandNisS-linearly equivalent toι →₀ M ⊗[R] NfinsuppTensorFinsupp, the tensor product ofι →₀ Mandκ →₀ Nis linearly equivalent to(ι × κ) →₀ (M ⊗ N).
noncomputable def
TensorProduct.finsuppLeft
(R : Type u_1)
(S : Type u_2)
[CommSemiring R]
[Semiring S]
[Algebra R S]
(M : Type u_3)
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
(N : Type u_4)
[AddCommMonoid N]
[Module R N]
(ι : Type u_5)
[DecidableEq ι]
:
The tensor product of ι →₀ M and N is linearly equivalent to ι →₀ M ⊗[R] N
Equations
Instances For
theorem
TensorProduct.finsuppLeft_apply_tmul
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(p : ι →₀ M)
(n : N)
:
@[simp]
theorem
TensorProduct.finsuppLeft_apply_tmul_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(p : ι →₀ M)
(n : N)
(i : ι)
:
theorem
TensorProduct.finsuppLeft_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(t : TensorProduct R (ι →₀ M) N)
(i : ι)
:
@[simp]
theorem
TensorProduct.finsuppLeft_symm_apply_single
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(i : ι)
(m : M)
(n : N)
:
noncomputable def
TensorProduct.finsuppRight
(R : Type u_1)
(S : Type u_2)
[CommSemiring R]
[Semiring S]
[Algebra R S]
(M : Type u_3)
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
(N : Type u_4)
[AddCommMonoid N]
[Module R N]
(ι : Type u_5)
[DecidableEq ι]
:
The tensor product of M and ι →₀ N is linearly equivalent to ι →₀ M ⊗[R] N
Equations
Instances For
theorem
TensorProduct.finsuppRight_apply_tmul
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(m : M)
(p : ι →₀ N)
:
@[simp]
theorem
TensorProduct.finsuppRight_apply_tmul_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(m : M)
(p : ι →₀ N)
(i : ι)
:
theorem
TensorProduct.finsuppRight_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(t : TensorProduct R M (ι →₀ N))
(i : ι)
:
@[simp]
theorem
TensorProduct.finsuppRight_tmul_single
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(i : ι)
(m : M)
(n : N)
:
@[simp]
theorem
TensorProduct.finsuppRight_symm_apply_single
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(i : ι)
(m : M)
(n : N)
:
theorem
TensorProduct.finsuppLeft_smul'
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(s : S)
(t : TensorProduct R (ι →₀ M) N)
:
@[deprecated TensorProduct.finsuppLeft (since := "2026-01-01")]
def
TensorProduct.finsuppLeft'
(R : Type u_1)
(S : Type u_2)
[CommSemiring R]
[Semiring S]
[Algebra R S]
(M : Type u_3)
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
(N : Type u_4)
[AddCommMonoid N]
[Module R N]
(ι : Type u_5)
[DecidableEq ι]
:
Alias of TensorProduct.finsuppLeft.
The tensor product of ι →₀ M and N is linearly equivalent to ι →₀ M ⊗[R] N
Equations
Instances For
@[deprecated "is syntactic rfl now" (since := "2026-01-01")]
theorem
TensorProduct.finsuppLeft'_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(x : TensorProduct R (ι →₀ M) N)
:
noncomputable def
TensorProduct.finsuppScalarLeft
(R : Type u_1)
[CommSemiring R]
(N : Type u_4)
[AddCommMonoid N]
[Module R N]
(ι : Type u_5)
[DecidableEq ι]
:
The tensor product of ι →₀ R and N is linearly equivalent to ι →₀ N
Equations
Instances For
@[simp]
theorem
TensorProduct.finsuppScalarLeft_apply_tmul_apply
{R : Type u_1}
[CommSemiring R]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(p : ι →₀ R)
(n : N)
(i : ι)
:
theorem
TensorProduct.finsuppScalarLeft_apply_tmul
{R : Type u_1}
[CommSemiring R]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(p : ι →₀ R)
(n : N)
:
theorem
TensorProduct.finsuppScalarLeft_apply
{R : Type u_1}
[CommSemiring R]
{N : Type u_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[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_4}
[AddCommMonoid N]
[Module R N]
{ι : Type u_5}
[DecidableEq ι]
(i : ι)
(n : N)
:
noncomputable def
TensorProduct.finsuppScalarRight
(R : Type u_1)
(S : Type u_2)
[CommSemiring R]
[Semiring S]
[Algebra R S]
(M : Type u_3)
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
(ι : Type u_5)
[DecidableEq ι]
:
The tensor product of M and ι →₀ R is linearly equivalent to ι →₀ M
Equations
Instances For
@[simp]
theorem
TensorProduct.finsuppScalarRight_apply_tmul_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{ι : Type u_5}
[DecidableEq ι]
(m : M)
(p : ι →₀ R)
(i : ι)
:
theorem
TensorProduct.finsuppScalarRight_apply_tmul
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{ι : Type u_5}
[DecidableEq ι]
(m : M)
(p : ι →₀ R)
:
theorem
TensorProduct.finsuppScalarRight_apply
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{ι : Type u_5}
[DecidableEq ι]
(t : TensorProduct R M (ι →₀ R))
(i : ι)
:
((finsuppScalarRight R S M ι) t) i = (AlgebraTensorModule.rid R S M) ((LinearMap.lTensor M (Finsupp.lapply i)) t)
@[simp]
theorem
TensorProduct.finsuppScalarRight_symm_apply_single
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{ι : Type u_5}
[DecidableEq ι]
(i : ι)
(m : M)
:
theorem
TensorProduct.finsuppScalarRight_smul
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{ι : Type u_5}
[DecidableEq ι]
(s : S)
(t : TensorProduct R M (ι →₀ R))
:
@[deprecated TensorProduct.finsuppScalarRight (since := "2026-01-01")]
def
TensorProduct.finsuppScalarRight'
(R : Type u_1)
(S : Type u_2)
[CommSemiring R]
[Semiring S]
[Algebra R S]
(M : Type u_3)
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
(ι : Type u_5)
[DecidableEq ι]
:
Alias of TensorProduct.finsuppScalarRight.
The tensor product of M and ι →₀ R is linearly equivalent to ι →₀ M
Equations
Instances For
@[deprecated "is syntactic rfl now" (since := "2026-01-01")]
theorem
TensorProduct.coe_finsuppScalarRight'
{R : Type u_1}
{S : Type u_2}
[CommSemiring R]
[Semiring S]
[Algebra R S]
{M : Type u_3}
[AddCommMonoid M]
[Module R M]
[Module S M]
[IsScalarTower R S M]
{ι : Type u_5}
[DecidableEq ι]
:
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 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]
:
The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).
Equations
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)
[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)
:
@[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 : κ)
:
@[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)
:
def
finsuppTensorFinsuppLid
(R : Type u_1)
(N : Type u_4)
(ι : Type u_5)
(κ : Type u_6)
[CommSemiring R]
[AddCommMonoid N]
[Module 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)
[CommSemiring R]
[AddCommMonoid N]
[Module R N]
(f : ι →₀ R)
(g : κ →₀ N)
(a : ι)
(b : κ)
:
@[simp]
@[simp]
def
finsuppTensorFinsuppRid
(R : Type u_1)
(M : Type u_3)
(ι : Type u_5)
(κ : Type u_6)
[CommSemiring R]
[AddCommMonoid M]
[Module 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)
[CommSemiring R]
[AddCommMonoid M]
[Module R M]
(f : ι →₀ M)
(g : κ →₀ R)
(a : ι)
(b : κ)
:
@[simp]
@[simp]
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)
[CommSemiring R]
(f : ι →₀ R)
(g : κ →₀ R)
(a : ι)
(b : κ)
:
theorem
finsuppTensorFinsuppLid_self
(R : Type u_1)
(ι : Type u_5)
(κ : Type u_6)
[CommSemiring R]
:
theorem
finsuppTensorFinsuppRid_self
(R : Type u_1)
(ι : Type u_5)
(κ : Type u_6)
[CommSemiring R]
: