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 => 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.
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 => 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
    Instances For
      @[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
      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] [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 : nM) (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