Documentation

Mathlib.LinearAlgebra.FinsuppVectorSpace

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 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} [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
    Instances For
      @[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
      Instances For

        TODO: move this section to an earlier file.

        theorem Finset.sum_single_ite {R : Type u_1} {n : Type u_3} [DecidableEq n] [Semiring R] [Fintype n] (a : R) (i : n) :
        x : n, Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
        @[simp]
        theorem Basis.equivFun_symm_single {R : Type u_1} {M : Type u_2} {n : Type u_3} [DecidableEq n] [Semiring R] [AddCommMonoid M] [Module R M] [Finite n] (b : Basis n R M) (i : n) :
        b.equivFun.symm (Pi.single i 1) = b i
        @[deprecated Basis.equivFun_symm_single]
        theorem Basis.equivFun_symm_stdBasis {R : Type u_1} {M : Type u_2} {n : Type u_3} [DecidableEq n] [Semiring R] [AddCommMonoid M] [Module R M] [Finite n] (b : Basis n R M) (i : n) :
        b.equivFun.symm ((LinearMap.stdBasis R (fun (x : n) => R) i) 1) = b i