Results on direct sums and finitely supported functions.

1. The linear equivalence between finitely supported functions ι →₀ M and the direct sum of copies of M indexed by ι.

def finsuppLEquivDirectSum (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (ι : Type u_1) [DecidableEq ι] : (ι →₀ M) ≃ₗ[R] ⨁ (x : ι), M

The finitely supported functions ι →₀ M are in linear equivalence with the direct sum of copies of M indexed by ι.

Equations

• finsuppLEquivDirectSum R M ι = finsuppLequivDFinsupp R

@[simp]

theorem finsuppLEquivDirectSum_single (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (ι : Type u_1) [DecidableEq ι] (i : ι) (m : M) : (↑(finsuppLEquivDirectSum R M ι) fun₀ | i => m) = ↑(DirectSum.lof R ι (fun i => M) i) m

@[simp]

theorem finsuppLEquivDirectSum_symm_lof (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M] (ι : Type u_1) [DecidableEq ι] (i : ι) (m : M) : ↑(LinearEquiv.symm (finsuppLEquivDirectSum R M ι)) (↑(DirectSum.lof R ι (fun x => M) i) m) = fun₀ | i => m