# Linear structures on function with finite support ι →₀ M#

This file contains results on the R-module structure on functions of finite support from a type ι to an R-module M, in particular in the case that R is a field.

theorem Finsupp.linearIndependent_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring R] [] [Module R M] {φ : ιType u_4} {f : (ι : ι) → φ ιM} (hf : ∀ (i : ι), LinearIndependent R (f i)) :
LinearIndependent R fun (ix : (i : ι) × φ i) => Finsupp.single ix.fst (f ix.fst ix.snd)
def Finsupp.basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {φ : ιType u_4} (b : (i : ι) → Basis (φ i) R M) :
Basis ((i : ι) × φ i) R (ι →₀ M)

The basis on ι →₀ M with basis vectors fun ⟨i, x⟩ ↦ single i (b i x).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Finsupp.basis_repr {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {φ : ιType u_4} (b : (i : ι) → Basis (φ i) R M) (g : ι →₀ M) (ix : (i : ι) × φ i) :
(().repr g) ix = ((b ix.fst).repr (g ix.fst)) ix.snd
@[simp]
theorem Finsupp.coe_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [] [] [Module R M] {φ : ιType u_4} (b : (i : ι) → Basis (φ i) R M) :
() = fun (ix : (i : ι) × φ i) => Finsupp.single ix.fst ((b ix.fst) ix.snd)
@[simp]
theorem Finsupp.basisSingleOne_repr {R : Type u_1} {ι : Type u_3} [] :
Finsupp.basisSingleOne.repr = LinearEquiv.refl R (ι →₀ R)
def Finsupp.basisSingleOne {R : Type u_1} {ι : Type u_3} [] :
Basis ι R (ι →₀ R)

The basis on ι →₀ M with basis vectors fun i ↦ single i 1.

Equations
Instances For
@[simp]
theorem Finsupp.coe_basisSingleOne {R : Type u_1} {ι : Type u_3} [] :
Finsupp.basisSingleOne = fun (i : ι) =>
noncomputable def DFinsupp.basis {ι : Type u_1} {R : Type u_2} {M : ιType u_3} [] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {η : ιType u_4} (b : (i : ι) → Basis (η i) R (M i)) :
Basis ((i : ι) × η i) R (Π₀ (i : ι), M i)

The direct sum of free modules is free.

Note that while this is stated for DFinsupp not DirectSum, the types are defeq.

Equations
Instances For

TODO: move this section to an earlier file.

theorem Finset.sum_single_ite {R : Type u_1} {n : Type u_3} [] [] [] (a : R) (i : n) :
(Finset.univ.sum fun (x : n) => Finsupp.single x (if i = x then a else 0)) =
theorem Basis.equivFun_symm_stdBasis {R : Type u_1} {M : Type u_2} {n : Type u_3} [] [] [] [Module R M] [] (b : Basis n R M) (i : n) :
b.equivFun.symm ((LinearMap.stdBasis R (fun (x : n) => R) i) 1) = b i