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
- One or more equations did not get rendered due to their size.
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
- One or more equations did not get rendered due to their size.
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
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
- TensorProduct.finsuppScalarLeft R N ι = (TensorProduct.finsuppLeft R R R N ι).trans (Finsupp.mapRange.linearEquiv (TensorProduct.lid R N))
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
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
- 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)
[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 : κ)
:
@[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]
:
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))
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]
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]
:
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))
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]
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
A variant of finsuppTensorFinsupp where both modules are the ground ring.
Equations
- finsuppTensorFinsupp' R ι κ = finsuppTensorFinsuppLid R R ι κ
Instances For
@[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]
:
theorem
finsuppTensorFinsuppRid_self
(R : Type u_1)
(ι : Type u_5)
(κ : Type u_6)
[CommSemiring R]
: