mathlib documentation

linear_algebra.direct_sum.finsupp

Results on finitely supported functions. #

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

source
noncomputable def finsupp_tensor_finsupp (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] :
(ι →₀ M) ⊗ (κ →₀ N) ≃ₗ[R] ι × κ →₀ M ⊗ N

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

Equations
source
@[simp]
theorem finsupp_tensor_finsupp_single (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (i : ι) (m : M) (k : κ) (n : N) :
⇑(finsupp_tensor_finsupp R M N ι κ) (finsupp.single i m ⊗ₜ[R] finsupp.single k n) = finsupp.single (i, k) (m ⊗ₜ[R] n)
source
@[simp]
theorem finsupp_tensor_finsupp_apply (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (f : ι →₀ M) (g : κ →₀ N) (i : ι) (k : κ) :
⇑(⇑(finsupp_tensor_finsupp R M N ι κ) (f ⊗ₜ[R] g)) (i, k) = ⇑f i ⊗ₜ[R] ⇑g k
source
@[simp]
theorem finsupp_tensor_finsupp_symm_single (R : Type u_1) (M : Type u_2) (N : Type u_3) (ι : Type u_4) (κ : Type u_5) [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (i : ι × κ) (m : M) (n : N) :
⇑((finsupp_tensor_finsupp R M N ι κ).symm) (finsupp.single i (m ⊗ₜ[R] n)) = finsupp.single i.fst m ⊗ₜ[R] finsupp.single i.snd n
source
noncomputable def finsupp_tensor_finsupp' (S : Type u_1) [comm_ring S] (α : Type u_2) (β : Type u_3) :
(α →₀ S) ⊗ (β →₀ S) ≃ₗ[S] α × β →₀ S

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

Equations
source
@[simp]
theorem finsupp_tensor_finsupp'_apply_apply (S : Type u_1) [comm_ring S] (α : Type u_2) (β : Type u_3) (f : α →₀ S) (g : β →₀ S) (a : α) (b : β) :
⇑(⇑(finsupp_tensor_finsupp' S α β) (f ⊗ₜ[S] g)) (a, b) = (⇑f a) * ⇑g b
source
@[simp]
theorem finsupp_tensor_finsupp'_single_tmul_single (S : Type u_1) [comm_ring S] (α : Type u_2) (β : Type u_3) (a : α) (b : β) (r₁ r₂ : S) :
⇑(finsupp_tensor_finsupp' S α β) (finsupp.single a r₁ ⊗ₜ[S] finsupp.single b r₂) = finsupp.single (a, b) (r₁ * r₂)