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.

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 : ι) → Module.Basis (η i) R (M i)) : Module.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 := (DFinsupp.mapRange.linearEquiv fun (i : ι) => (b i).repr) ≪≫ₗ (sigmaFinsuppLequivDFinsupp R).symm }

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)

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)

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)

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)

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)

noncomputable 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 : ι) → Module.Basis (φ i) R M) : Module.Basis ((i : ι) × φ i) R (ι →₀ M)

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

Equations

• Finsupp.basis b = { repr := finsuppLequivDFinsupp R ≪≫ₗ ((DFinsupp.mapRange.linearEquiv fun (i : ι) => (b i).repr) ≪≫ₗ (sigmaFinsuppLequivDFinsupp R).symm) }

@[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 : ι) → Module.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 : ι) → Module.Basis (φ i) R M) : ⇑(Finsupp.basis b) = fun (ix : (i : ι) × φ i) => single ix.fst ((b ix.fst) ix.snd)

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)

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

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

Equations

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

@[simp]

theorem Finsupp.basisSingleOne_repr {R : Type u_1} {ι : Type u_3} [Semiring R] : 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 : ι) => single i 1

theorem Finsupp.linearIndependent_single_one (R : Type u_1) (ι : Type u_3) [Semiring R] : LinearIndependent R fun (i : ι) => single i 1

theorem Finsupp.isCompl_range_lmapDomain_span {R : Type u_1} {ι : Type u_3} [Semiring R] {α : Type u_4} {β : Type u_5} {u : α → ι} {v : β → ι} (huv : IsCompl (Set.range u) (Set.range v)) : IsCompl (lmapDomain R R u).range (Submodule.span R (Set.range fun (x : β) => single (v x) 1))

theorem Finsupp.linearIndependent_single_of_ne_zero {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring R] [AddCommGroup M] [IsDomain R] [Module R M] [Module.IsTorsionFree R M] {v : ι → M} (hv : ∀ (i : ι), v i ≠ 0) : LinearIndependent R fun (i : ι) => single i (v i)

theorem Finsupp.lcomapDomain_eq_linearProjOfIsCompl {R : Type u_1} {ι : Type u_3} [Ring R] {α : Type u_4} {β : Type u_5} {u : α → ι} {v : β → ι} (hu : Function.Injective u) (h : IsCompl (Set.range u) (Set.range v)) : lcomapDomain u hu = LinearMap.linearProjOfIsCompl (Submodule.span R (Set.range fun (x : β) => single (v x) 1)) (lmapDomain R R u) ⋯ ⋯

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.

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 : Module.Basis n R M) (i : n) : b.equivFun.symm (Pi.single i 1) = b i

theorem Module.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) .

instance FreeAbelianGroup.instFreeInt {σ : Type u_1} : Module.Free ℤ (FreeAbelianGroup σ)

instance AddMonoidAlgebra.instFree {M : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] [Module R S] [Module.Free R S] : Module.Free R (AddMonoidAlgebra S M)

instance MonoidAlgebra.instFree {M : Type u_1} {R : Type u_2} {S : Type u_3} [Semiring R] [Semiring S] [Module R S] [Module.Free R S] : Module.Free R (MonoidAlgebra S M)

instance Polynomial.instFree {R : Type u_1} [Semiring R] : Module.Free R (Polynomial R)