Documentation

Mathlib.LinearAlgebra.Finsupp.VectorSpace

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.

source
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
      source
      instance Module.Free.dfinsupp {ι : Type u_1} (R : Type u_2) (M : ι → Type u_3) [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), Free R (M i)] :
      Free R (Π₀ (i : ι), M i)
      source
      theorem DFinsupp.linearIndependent_single {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] {φ : ι → Type u_4} (f : (i : ι) → φ i → M i) (hf : ∀ (i : ι), LinearIndependent R (f i)) :
      LinearIndependent R fun (ix : (i : ι) × φ i) => single ix.fst (f ix.fst ix.snd)
      source
      theorem DFinsupp.linearIndependent_single_iff {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] {φ : ι → Type u_4} (f : (i : ι) → φ i → M i) :
      (LinearIndependent R fun (ix : (i : ι) × φ i) => single ix.fst (f ix.fst ix.snd)) ↔ ∀ (i : ι), LinearIndependent R (f i)
      source
      theorem Finsupp.linearIndependent_single {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} (f : (i : ι) → φ i → M) (hf : ∀ (i : ι), LinearIndependent R (f i)) :
      LinearIndependent R fun (ix : (i : ι) × φ i) => single ix.fst (f ix.fst ix.snd)
      source
      theorem Finsupp.linearIndependent_single_iff {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ι → Type u_4} {f : (i : ι) → φ i → M} :
      (LinearIndependent R fun (ix : (i : ι) × φ i) => single ix.fst (f ix.fst ix.snd)) ↔ ∀ (i : ι), LinearIndependent R (f i)
      source
      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
        Instances For
          source
          @[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
          source
          @[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) => single ix.fst ((b ix.fst) ix.snd)
          source
          instance Module.Free.finsupp (R : Type u_1) (M : Type u_2) (ι : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Free R M] :
          Free R (ι →₀ M)
          source
          def Finsupp.basisSingleOne {R : Type u_1} {ι : Type u_3} [Semiring R] :
          Basis ι R (ι →₀ R)

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

          Equations
            Instances For
              source
              @[simp]
              theorem Finsupp.basisSingleOne_repr {R : Type u_1} {ι : Type u_3} [Semiring R] :
              Finsupp.basisSingleOne.repr = LinearEquiv.refl R (ι →₀ R)
              source
              @[simp]
              theorem Finsupp.coe_basisSingleOne {R : Type u_1} {ι : Type u_3} [Semiring R] :
              ⇑Finsupp.basisSingleOne = fun (i : ι) => single i 1
              source
              theorem Finsupp.linearIndependent_single_one (R : Type u_1) (ι : Type u_3) [Semiring R] :
              LinearIndependent R fun (i : ι) => single i 1
              source
              theorem Finsupp.linearIndependent_single_of_ne_zero {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {v : ι → M} (hv : ∀ (i : ι), v i ≠ 0) :
              LinearIndependent R fun (i : ι) => single i (v i)
              source
              theorem Module.Free.trans {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Free S M] [Free R S] :
              Free R M

              TODO: move this section to an earlier file.

              source
              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
              source
              @[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
              source
              theorem Basis.repr_smul' {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_3} (B : Basis ι R S) (i : ι) (r : R) (s : S) :
              (B.repr ((algebraMap R S) r * s)) i = r * (B.repr s) i

              For any r : R, s : S, we have B.repr ((algebra_map R S r) * s) i = r * (B.repr s i) .