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))
theorem
finsupp.is_basis_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 : ι), is_basis R (f i)) :
is_basis R (λ (ix : Σ (i : ι), φ i), finsupp.single ix.fst (f ix.fst ix.snd))
theorem
finsupp.is_basis_single_one
{R : Type u_1}
{ι : Type u_3}
[ring R] :
is_basis R (λ (i : ι), finsupp.single i 1)
theorem
finsupp.is_basis.tensor_product
{R : Type u_1}
{M : Type u_2}
{N : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
[comm_ring R]
[add_comm_group M]
[module R M]
[add_comm_group N]
[module R N]
{b : ι → M}
(hb : is_basis R b)
{c : κ → N}
(hc : is_basis R c) :
If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.
theorem
finsupp.dim_eq
{K : Type u}
{V ι : Type v}
[field K]
[add_comm_group V]
[vector_space K V] :
vector_space.dim K (ι →₀ V) = (# ι) * vector_space.dim K V
theorem
equiv_of_dim_eq_lift_dim
{K : Type u}
{V : Type v}
{V' : Type w}
[field K]
[add_comm_group V]
[vector_space K V]
[add_comm_group V']
[vector_space K V']
(h : (vector_space.dim K V).lift = (vector_space.dim K V').lift) :
def
equiv_of_dim_eq_dim
{K : Type u}
{V₁ V₂ : Type v}
[field K]
[add_comm_group V₁]
[vector_space K V₁]
[add_comm_group V₂]
[vector_space K V₂]
(h : vector_space.dim K V₁ = vector_space.dim K V₂) :
Two K-vector spaces are equivalent if their dimension is the same.
Equations
def
fin_dim_vectorspace_equiv
{K : Type u}
{V : Type v}
[field K]
[add_comm_group V]
[vector_space K V]
(n : ℕ)
(hn : vector_space.dim 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]
[vector_space K V]
[finite_dimensional K V] :
# V = # K ^ vector_space.dim K V
theorem
cardinal_lt_omega_of_finite_dimensional
(K V : Type u)
[field K]
[add_comm_group V]
[vector_space K V]
[fintype K]
[finite_dimensional K V] :
# V < cardinal.omega