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] [AddCommGroup M] [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} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} (b : (i : ι) → Basis (φ i) R M) : Basis ((i : ι) × φ i) R (ι →₀ M)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Finsupp.basis_repr {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} (b : (i : ι) → Basis (φ i) R M) (g : ι →₀ M) (ix : (i : ι) × φ i) : ((Finsupp.basis b).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} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} (b : (i : ι) → Basis (φ i) R M) : ⇑(Finsupp.basis b) = 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} [Semiring R] : Finsupp.basisSingleOne.repr = LinearEquiv.refl R (ι →₀ R)

def Finsupp.basisSingleOne {R : Type u_1} {ι : Type u_3} [Semiring R] : Basis ι R (ι →₀ R)

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

Equations

• Finsupp.basisSingleOne = { repr := LinearEquiv.refl R (ι →₀ R) }

@[simp]

theorem Finsupp.coe_basisSingleOne {R : Type u_1} {ι : Type u_3} [Semiring R] : ⇑Finsupp.basisSingleOne = fun (i : ι) => Finsupp.single i 1

noncomputable def DFinsupp.basis {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [Semiring R] [(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

• DFinsupp.basis b = { repr := LinearEquiv.trans (DFinsupp.mapRange.linearEquiv fun (i : ι) => (b i).repr) (LinearEquiv.symm (sigmaFinsuppLequivDFinsupp R)) }

TODO: move this section to an earlier file.

theorem Finset.sum_single_ite {R : Type u_1} {n : Type u_3} [DecidableEq n] [Fintype n] [Semiring R] (a : R) (i : n) : (Finset.sum Finset.univ fun (x : n) => Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a

theorem Basis.equivFun_symm_stdBasis {R : Type u_1} {M : Type u_2} {n : Type u_3} [DecidableEq n] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis n R M) (i : n) : (LinearEquiv.symm (Basis.equivFun b)) ((LinearMap.stdBasis R (fun (x : n) => R) i) 1) = b i