Bases
This file defines bases in a module or vector space.
It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.
Main definitions
All definitions are given for families of vectors, i.e. v : ι → M where M is the module or
vector space and ι : Type* is an arbitrary indexing type.
is_basis R vstates that the vector familyvis a basis, i.e. it is linearly independent and spans the entire space.is_basis.repr hv xis the basis version oflinear_independent.repr hv x. It returns the linear combination representingx : Mon a basisvofM(using classical choice). The argumenthvmust be a proof thatis_basis R v.is_basis.repr hvis given as a linear map as well.is_basis.constr hv fconstructs a linear mapM₁ →ₗ[R] M₂given the valuesf : ι → M₂at the basisv : ι → M₁, givenhv : is_basis R v.
Main statements
is_basis.extstates that two linear maps are equal if they coincide on a basis.exists_is_basisstates that every vector space has a basis.
Implementation notes
We use families instead of sets because it allows us to say that two identical vectors are linearly
dependent. For bases, this is useful as well because we can easily derive ordered bases by using an
ordered index type ι.
Tags
basis, bases
def
is_basis
{ι : Type u_1}
(R : Type u_3)
{M : Type u_5}
(v : ι → M)
[ring R]
[add_comm_group M]
[module R M] :
Prop
A family of vectors is a basis if it is linearly independent and all vectors are in the span.
Equations
- is_basis R v = (linear_independent R v ∧ submodule.span R (set.range v) = ⊤)
theorem
is_basis.mem_span
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(x : M) :
x ∈ submodule.span R (set.range v)
theorem
is_basis.comp
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(f : ι' → ι)
(hf : function.bijective f) :
theorem
is_basis.injective
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[nontrivial R]
(hv : is_basis R v) :
theorem
is_basis.range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
def
is_basis.repr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
Given a basis, any vector can be written as a linear combination of the basis vectors. They are
given by this linear map. This is one direction of module_equiv_finsupp.
Equations
- hv.repr = _.repr.comp (linear_map.cod_restrict (submodule.span R (set.range v)) linear_map.id _)
theorem
is_basis.total_repr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(x : M) :
⇑(finsupp.total ι M R v) (⇑(hv.repr) x) = x
theorem
is_basis.total_comp_repr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
(finsupp.total ι M R v).comp hv.repr = linear_map.id
theorem
is_basis.ext
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{f g : M →ₗ[R] M'}
(hv : is_basis R v)
(h : ∀ (i : ι), ⇑f (v i) = ⇑g (v i)) :
f = g
theorem
is_basis.repr_ker
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
theorem
is_basis.repr_range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
hv.repr.range = finsupp.supported R R set.univ
theorem
is_basis.repr_total
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(x : ι →₀ R)
(hx : x ∈ finsupp.supported R R set.univ) :
⇑(hv.repr) (⇑(finsupp.total ι M R v) x) = x
theorem
is_basis.repr_eq_single
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
{i : ι} :
⇑(hv.repr) (v i) = finsupp.single i 1
theorem
is_basis.repr_eq_iff
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
{f : M →ₗ[R] ι →₀ R} :
theorem
is_basis.repr_apply_eq
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
{f : M → ι → R}
(hadd : ∀ (x y : M), f (x + y) = f x + f y)
(hsmul : ∀ (c : R) (x : M), f (c • x) = c • f x)
(f_eq : ∀ (i : ι), f (v i) = ⇑(finsupp.single i 1))
(x : M)
(i : ι) :
theorem
is_basis.range_repr_self
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(i : ι) :
⇑(_.repr) (v i) = finsupp.single ⟨v i, _⟩ 1
def
is_basis.constr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(f : ι → M') :
Construct a linear map given the value at the basis.
Equations
- hv.constr f = (finsupp.total M' M' R id).comp ((finsupp.lmap_domain R R f).comp hv.repr)
theorem
is_basis.constr_apply
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(f : ι → M')
(x : M) :
@[simp]
theorem
constr_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{f : ι → M'}
{i : ι}
(hv : is_basis R v) :
theorem
constr_self
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(f : M →ₗ[R] M') :
theorem
constr_zero
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v) :
theorem
constr_add
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{g f : ι → M'}
(hv : is_basis R v) :
theorem
constr_neg
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{f : ι → M'}
(hv : is_basis R v) :
theorem
constr_sub
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
{g f : ι → M'}
(hs : is_basis R v) :
theorem
constr_range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
[nonempty ι]
(hv : is_basis R v)
{f : ι → M'} :
(hv.constr f).range = submodule.span R (set.range f)
def
module_equiv_finsupp
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
Canonical equivalence between a module and the linear combinations of basis vectors.
Equations
- module_equiv_finsupp hv = (_.total_equiv.trans (linear_equiv.of_top (submodule.span R (set.range v)) _)).symm
@[simp]
theorem
module_equiv_finsupp_apply_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(i : ι) :
⇑(module_equiv_finsupp hv) (v i) = finsupp.single i 1
def
linear_equiv_of_is_basis
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{v : ι → M}
{v' : ι' → M'}
(hv : is_basis R v)
(hv' : is_basis R v')
(e : ι ≃ ι') :
Isomorphism between the two modules, given two modules M and M' with respective bases
v and v' and a bijection between the indexing sets of the two bases.
def
linear_equiv_of_is_basis'
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{v : ι → M}
{v' : ι' → M'}
(f : M → M')
(g : M' → M)
(hv : is_basis R v)
(hv' : is_basis R v')
(hf : ∀ (i : ι), f (v i) ∈ set.range v')
(hg : ∀ (i : ι'), g (v' i) ∈ set.range v)
(hgf : ∀ (i : ι), g (f (v i)) = v i)
(hfg : ∀ (i : ι'), f (g (v' i)) = v' i) :
Isomorphism between the two modules, given two modules M and M' with respective bases
v and v' and a bijection between the two bases.
@[simp]
theorem
linear_equiv_of_is_basis_comp
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{M'' : Type u_7}
[ring R]
[add_comm_group M]
[add_comm_group M']
[add_comm_group M'']
[module R M]
[module R M']
[module R M'']
{ι'' : Type u_4}
{v : ι → M}
{v' : ι' → M'}
{v'' : ι'' → M''}
(hv : is_basis R v)
(hv' : is_basis R v')
(hv'' : is_basis R v'')
(e : ι ≃ ι')
(f : ι' ≃ ι'') :
(linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv'' f) = linear_equiv_of_is_basis hv hv'' (e.trans f)
@[simp]
theorem
linear_equiv_of_is_basis_refl
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
linear_equiv_of_is_basis hv hv (equiv.refl ι) = linear_equiv.refl R M
theorem
linear_equiv_of_is_basis_trans_symm
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(e : ι ≃ ι')
{v' : ι' → M'}
(hv' : is_basis R v') :
(linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv e.symm) = linear_equiv.refl R M
theorem
linear_equiv_of_is_basis_symm_trans
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(e : ι ≃ ι')
{v' : ι' → M'}
(hv' : is_basis R v') :
(linear_equiv_of_is_basis hv' hv e.symm).trans (linear_equiv_of_is_basis hv hv' e) = linear_equiv.refl R M'
theorem
is_basis_inl_union_inr
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{v : ι → M}
{v' : ι' → M'}
(hv : is_basis R v)
(hv' : is_basis R v') :
is_basis R (sum.elim (⇑(linear_map.inl R M M') ∘ v) (⇑(linear_map.inr R M M') ∘ v'))
theorem
is_basis_singleton_one
{ι : Type u_1}
(R : Type u_2)
[unique ι]
[ring R] :
is_basis R (λ (_x : ι), 1)
theorem
linear_equiv.is_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hs : is_basis R v)
(f : M ≃ₗ[R] M') :
theorem
is_basis_span
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hs : linear_independent R v) :
theorem
is_basis_empty
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
(h_empty : ¬nonempty ι)
(h : ∀ (x : M), x = 0) :
is_basis R (λ (x : ι), 0)
theorem
is_basis_empty_bot
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
(h_empty : ¬nonempty ι) :
is_basis R (λ (_x : ι), 0)
def
is_basis.equiv_fun
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v) :
A module over R with a finite basis is linearly equivalent to functions from its basis to R.
Equations
- h.equiv_fun = (module_equiv_finsupp h).trans {to_fun := finsupp.to_fun (mul_zero_class.to_has_zero R), map_add' := _, map_smul' := _, inv_fun := finsupp.equiv_fun_on_fintype.inv_fun, left_inv := _, right_inv := _}
def
module.fintype_of_fintype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v)
[fintype R] :
fintype M
A module over a finite ring that admits a finite basis is finite.
Equations
- module.fintype_of_fintype h = fintype.of_equiv (ι → R) h.equiv_fun.to_equiv.symm
theorem
module.card_fintype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v)
[fintype R]
[fintype M] :
fintype.card M = fintype.card R ^ fintype.card ι
@[simp]
theorem
is_basis.equiv_fun_symm_apply
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v)
(x : ι → R) :
Given a basis v indexed by ι, the canonical linear equivalence between ι → R and M maps
a function x : ι → R to the linear combination ∑_i x i • v i.
@[simp]
theorem
is_basis.constr_apply_fintype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
[fintype ι]
(h : is_basis R v)
(f : ι → M')
(x : M) :
theorem
exists_subset_is_basis
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{s : set V}
(hs : linear_independent K (λ (x : ↥s), ↑x)) :
theorem
exists_sum_is_basis
{ι : Type u_1}
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{v : ι → V}
(hs : linear_independent K v) :
theorem
exists_is_basis
(K : Type u_4)
(V : Type u)
[field K]
[add_comm_group V]
[vector_space K V] :
theorem
linear_map.exists_left_inverse_of_injective
{K : Type u_4}
{V : Type u}
{V' : Type u_8}
[field K]
[add_comm_group V]
[add_comm_group V']
[vector_space K V]
[vector_space K V']
(f : V →ₗ[K] V')
(hf_inj : f.ker = ⊥) :
∃ (g : V' →ₗ[K] V), g.comp f = linear_map.id
theorem
submodule.exists_is_compl
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
(p : submodule K V) :
theorem
linear_map.exists_right_inverse_of_surjective
{K : Type u_4}
{V : Type u}
{V' : Type u_8}
[field K]
[add_comm_group V]
[add_comm_group V']
[vector_space K V]
[vector_space K V']
(f : V →ₗ[K] V')
(hf_surj : f.range = ⊤) :
∃ (g : V' →ₗ[K] V), f.comp g = linear_map.id
theorem
quotient_prod_linear_equiv
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
(p : submodule K V) :
theorem
vector_space.card_fintype
(K : Type u_4)
(V : Type u)
[field K]
[add_comm_group V]
[vector_space K V]
[fintype K]
[fintype V] :
∃ (n : ℕ), fintype.card V = fintype.card K ^ n
theorem
pi.linear_independent_std_basis
{R : Type u_3}
{η : Type u_9}
{ιs : η → Type u_10}
{Ms : η → Type u_11}
[ring R]
[Π (i : η), add_comm_group (Ms i)]
[Π (i : η), module R (Ms i)]
[decidable_eq η]
(v : Π (j : η), ιs j → Ms j)
(hs : ∀ (i : η), linear_independent R (v i)) :
linear_independent R (λ (ji : Σ (j : η), ιs j), ⇑(linear_map.std_basis R Ms ji.fst) (v ji.fst ji.snd))
theorem
pi.is_basis_std_basis
{R : Type u_3}
{η : Type u_9}
{ιs : η → Type u_10}
{Ms : η → Type u_11}
[ring R]
[Π (i : η), add_comm_group (Ms i)]
[Π (i : η), module R (Ms i)]
[fintype η]
[decidable_eq η]
(s : Π (j : η), ιs j → Ms j)
(hs : ∀ (j : η), is_basis R (s j)) :
theorem
pi.is_basis_fun₀
(R : Type u_3)
(η : Type u_9)
[ring R]
[fintype η]
[decidable_eq η] :
is_basis R (λ (ji : Σ (j : η), unit), ⇑(linear_map.std_basis R (λ (i : η), R) ji.fst) 1)
theorem
pi.is_basis_fun
(R : Type u_3)
(η : Type u_9)
[ring R]
[fintype η]
[decidable_eq η] :
is_basis R (λ (i : η), ⇑(linear_map.std_basis R (λ (i : η), R) i) 1)
@[simp]
theorem
pi.is_basis_fun_repr
(R : Type u_3)
(η : Type u_9)
[ring R]
[fintype η]
[decidable_eq η]
(x : η → R)
(i : η) :