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.
Furthermore, it contains some facts about isomorphisms of vector spaces from equality of dimension.
TODO #
Move the second half of this file to more appropriate other files.
theorem
finsupp.linear_independent_single
{R : Type u_1}
{M : Type u_2}
{ι : Type u_3}
[ring R]
[add_comm_group M]
[module R M]
{φ : ι → Type u_4}
{f : Π (ι : ι), φ ι → M}
(hf : ∀ (i : ι), linear_independent R (f i)) :
linear_independent R (λ (ix : Σ (i : ι), φ i), finsupp.single ix.fst (f ix.fst ix.snd))
@[protected]
noncomputable
def
finsupp.basis
{R : Type u_1}
{M : Type u_2}
{ι : Type u_3}
[semiring R]
[add_comm_monoid M]
[module R M]
{φ : ι → Type u_4}
(b : Π (i : ι), basis (φ i) R M) :
The basis on ι →₀ M with basis vectors λ ⟨i, x⟩, single i (b i x).
Equations
- finsupp.basis b = {repr := {to_fun := λ (g : ι →₀ M), {support := g.support.sigma (λ (i : ι), (⇑((b i).repr) (⇑g i)).support), to_fun := λ (ix : Σ (i : ι), φ i), ⇑(⇑((b ix.fst).repr) (⇑g ix.fst)) ix.snd, mem_support_to_fun := _}, map_add' := _, map_smul' := _, inv_fun := λ (g : (Σ (i : ι), φ i) →₀ R), {support := finset.image sigma.fst g.support, to_fun := λ (i : ι), ⇑((b i).repr.symm) (finsupp.comap_domain (sigma.mk i) g _), mem_support_to_fun := _}, left_inv := _, right_inv := _}}
@[protected]
The basis on ι →₀ M with basis vectors λ i, single i 1.
Equations
- finsupp.basis_single_one = {repr := linear_equiv.refl R (ι →₀ R) (finsupp.module ι R)}
@[simp]
theorem
finsupp.basis_single_one_repr
{R : Type u_1}
{ι : Type u_3}
[semiring R] :
finsupp.basis_single_one.repr = linear_equiv.refl R (ι →₀ R)
@[simp]
theorem
finsupp.coe_basis_single_one
{R : Type u_1}
{ι : Type u_3}
[semiring R] :
⇑finsupp.basis_single_one = λ (i : ι), finsupp.single i 1
theorem
finsupp.dim_eq
{K : Type u}
{V ι : Type v}
[field K]
[add_comm_group V]
[module K V] :
module.rank K (ι →₀ V) = cardinal.mk ι * module.rank K V
theorem
equiv_of_dim_eq_lift_dim
{K : Type u}
{V : Type v}
{V' : Type w}
[field K]
[add_comm_group V]
[module K V]
[add_comm_group V']
[module K V']
(h : (module.rank K V).lift = (module.rank K V').lift) :
noncomputable
def
equiv_of_dim_eq_dim
{K : Type u}
{V₁ V₂ : Type v}
[field K]
[add_comm_group V₁]
[module K V₁]
[add_comm_group V₂]
[module K V₂]
(h : module.rank K V₁ = module.rank K V₂) :
Two K-vector spaces are equivalent if their dimension is the same.
Equations
noncomputable
def
fin_dim_vectorspace_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[module K V]
(n : ℕ)
(hn : module.rank K V = ↑n) :
An n-dimensional K-vector space is equivalent to fin n → K.
Equations
theorem
finset.sum_single_ite
{R : Type u_1}
{n : Type u_3}
[decidable_eq n]
[fintype n]
[semiring R]
(a : R)
(i : n) :
finset.univ.sum (λ (x : n), finsupp.single x (ite (i = x) a 0)) = finsupp.single i a
@[simp]
theorem
basis.equiv_fun_symm_std_basis
{R : Type u_1}
{M : Type u_2}
{n : Type u_3}
[decidable_eq n]
[fintype n]
[semiring R]
[add_comm_monoid M]
[module R M]
(b : basis n R M)
(i : n) :