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 => fun₀ | 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 => fun₀ | 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 => fun₀ | 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 => fun₀ | x => if i = x then a else 0) = fun₀ | i => a

@[simp]

theorem Finset.sum_univ_ite {R : Type u_1} {M : Type u_2} {n : Type u_3} [DecidableEq n] [Fintype n] [Semiring R] [AddCommMonoid M] [Module R M] (b : n → M) (i : n) : (Finset.sum Finset.univ fun x => (if i = x then 1 else 0) • b x) = b i

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 => R) i) 1) = ↑b i