Documentation

Mathlib.Algebra.DirectSum.Finsupp

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 ι.
source
🔸 coverage
def finsuppLEquivDirectSum (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] :
(ι →₀ M) ≃ₗ[R] DirectSum ι fun (x : ι) => M

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

Equations
    Instances For
      source
      📐 coverage
      @[simp]
      theorem finsuppLEquivDirectSum_single (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid 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
      source
      📐 coverage
      @[simp]
      theorem finsuppLEquivDirectSum_apply (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] (m : ι →₀ M) (i : ι) :
      ((finsuppLEquivDirectSum R M ι) m) i = m i
      source
      📐 coverage
      @[simp]
      theorem finsuppLEquivDirectSum_symm_lof (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] (i : ι) (m : M) :
      (finsuppLEquivDirectSum R M ι).symm ((DirectSum.lof R ι (fun (x : ι) => M) i) m) = fun₀ | i => m
      source
      📐 coverage
      theorem lmap_finsuppLEquivDirectSum_eq (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] (ι : Type u_1) [DecidableEq ι] {N : Type u_2} [AddCommMonoid N] [Module R N] (ε : M →ₗ[R] N) (m : ι →₀ M) :
      (DirectSum.lmap fun (x : ι) => ε) ((finsuppLEquivDirectSum R M ι) m) = (finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)