mathlib3 documentation

algebra.direct_sum.finsupp

Results on direct sums and finitely supported functions. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

  1. The linear equivalence between finitely supported functions ι →₀ M and the direct sum of copies of M indexed by ι.
source
noncomputable 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
source
@[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
source
@[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