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 as well as the cardinality of finite dimensional vector spaces.
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}
[ring R]
[add_comm_group 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 := _}}
@[simp]
theorem
finsupp.coe_basis
{R : Type u_1}
{M : Type u_2}
{ι : Type u_3}
[ring R]
[add_comm_group M]
[module R M]
{φ : ι → Type u_4}
(b : Π (i : ι), basis (φ i) R M) :
⇑(finsupp.basis b) = λ (ix : Σ (i : ι), φ i), finsupp.single ix.fst (⇑(b ix.fst) ix.snd)
@[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}
[ring 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}
[ring 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) = (# ι) * 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
cardinal_mk_eq_cardinal_mk_field_pow_dim
(K V : Type u)
[field K]
[add_comm_group V]
[module K V]
[finite_dimensional K V] :
# V = # K ^ module.rank K V
theorem
cardinal_lt_omega_of_finite_dimensional
(K V : Type u)
[field K]
[add_comm_group V]
[module K V]
[fintype K]
[finite_dimensional K V] :