Results on direct sums and finitely supported functions.
The linear equivalence between finitely supported functions
ι →₀ Mand the direct sum of copies ofMindexed byι.The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).
def
finsupp_lequiv_direct_sum
(R : Type u)
(M : Type v)
[ring R]
[add_comm_group M]
[module R M]
(ι : Type u_1)
[decidable_eq ι] :
(ι →₀ M) ≃ₗ[R] direct_sum ι (λ (i : ι), M)
The finitely supported functions ι →₀ M are in linear equivalence with the direct sum of copies of M indexed by ι.
Equations
- finsupp_lequiv_direct_sum R M ι = linear_equiv.of_linear (finsupp.lsum (direct_sum.lof R ι (λ (_x : ι), M))) (direct_sum.to_module R ι (ι →₀ M) finsupp.lsingle) _ _
@[simp]
theorem
finsupp_lequiv_direct_sum_single
(R : Type u)
(M : Type v)
[ring R]
[add_comm_group M]
[module R M]
(ι : Type u_1)
[decidable_eq ι]
(i : ι)
(m : M) :
⇑(finsupp_lequiv_direct_sum R M ι) (finsupp.single i m) = ⇑(direct_sum.lof R ι (λ (i : ι), M) i) m
@[simp]
theorem
finsupp_lequiv_direct_sum_symm_lof
(R : Type u)
(M : Type v)
[ring R]
[add_comm_group M]
[module R M]
(ι : Type u_1)
[decidable_eq ι]
(i : ι)
(m : M) :
⇑((finsupp_lequiv_direct_sum R M ι).symm) (⇑(direct_sum.lof R ι (λ (i : ι), M) i) m) = finsupp.single i m
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] :
tensor_product R (ι →₀ M) (κ →₀ N) ≃ₗ[R] ι × κ →₀ tensor_product R M N
The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N).
Equations
- finsupp_tensor_finsupp R M N ι κ = (tensor_product.congr (finsupp_lequiv_direct_sum R M ι) (finsupp_lequiv_direct_sum R N κ)).trans ((tensor_product.direct_sum R ι κ (λ (_x : ι), M) (λ (_x : κ), N)).trans (finsupp_lequiv_direct_sum R (tensor_product R M N) (ι × κ)).symm)
@[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)
@[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