mathlib documentation

linear_algebra.basis

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.

Main statements #

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
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) :
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) :
is_basis R (v 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) :
is_basis R (λ (x : (set.range v)), x)
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
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) :
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) :
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
@[simp]
theorem is_basis.repr_self_apply {ι : 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 j : ι) :
((hv.repr) (v i)) j = ite (i = j) 1 0
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} :
hv.repr = f ∀ (i : ι), f (v i) = finsupp.single i 1
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 : ι) :
((hv.repr) x) i = f x 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
@[simp]
theorem is_basis.range_repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] {x : M} (hv : is_basis R v) (i : ι) :
((_.repr) x) v i, _⟩ = ((hv.repr) x) i
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') :
M →ₗ[R] M'

Construct a linear map given the value at the basis.

Equations
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) :
(hv.constr f) x = ((hv.repr) x).sum (λ (b : ι) (a : R), a f b)
@[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) :
(hv.constr f) (v i) = f i
theorem constr_eq {ι : 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 : ι → M'} {f : M →ₗ[R] M'} (hv : is_basis R v) (h : ∀ (i : ι), g i = f (v i)) :
hv.constr g = f
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') :
hv.constr (λ (i : ι), f (v i)) = f
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) :
hv.constr (λ (i : ι), 0) = 0
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) :
hv.constr (λ (i : ι), f i + g i) = hv.constr f + hv.constr g
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) :
hv.constr (λ (i : ι), -f i) = -hv.constr f
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) :
hv.constr (λ (i : ι), f i - g i) = hs.constr f - hs.constr g
theorem constr_smul {ι : Type u_1} {R : Type u_2} {M : Type u_3} [comm_ring R] [add_comm_group M] [module R M] {v : ι → R} {f : ι → M} {a : R} (hv : is_basis R v) :
hv.constr (λ (b : ι), a f b) = a hv.constr f
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'} :
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
@[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 : ι) :
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 : ι ι') :
M ≃ₗ[R] M'

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.

Equations
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) :
M ≃ₗ[R] M'

Isomorphism between the two modules, given two modules M and M' with respective bases v and v' and a bijection between the two bases.

Equations
@[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 : ι' ι'') :
@[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) :
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') :
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') :
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') :
@[simp]
theorem is_basis.repr_eq_zero {ι : 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} :
(hv.repr) x = 0 x = 0
theorem is_basis.ext_elem {ι : 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 y : M} (h : ∀ (i : ι), ((hv.repr) x) i = ((hv.repr) y) i) :
x = y
theorem is_basis.no_zero_smul_divisors {ι : 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) [no_zero_divisors R] :
theorem is_basis.smul_eq_zero {ι : 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) [no_zero_divisors R] {c : R} {x : M} :
c x = 0 c = 0 x = 0
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) :
is_basis R (λ (i : ι), v i, _⟩)
theorem is_basis_empty {ι : Type u_1} {R : Type u_3} (M : Type u_5) [ring R] [add_comm_group M] [module R M] [subsingleton 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) :
M ≃ₗ[R] ι → R

A module over R with a finite basis is linearly equivalent to functions from its basis to R.

Equations
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] :

A module over a finite ring that admits a finite basis is finite.

Equations
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] :
@[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) :
(h.equiv_fun.symm) x = ∑ (i : ι), x i v i

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.

theorem is_basis.equiv_fun_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) (u : M) :
(h.equiv_fun) u = ((h.repr) u)
theorem is_basis.equiv_fun_total {ι : 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) (u : M) :
∑ (i : ι), (h.equiv_fun) u i v i = u
@[simp]
theorem is_basis.equiv_fun_self {ι : 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) (i j : ι) :
(h.equiv_fun) (v i) j = ite (i = j) 1 0
@[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) :
(h.constr f) x = ∑ (i : ι), (h.equiv_fun) x i f i
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)) :
∃ (b : set V), s b is_basis K coe
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) :
∃ (ι' : Type u) (v' : ι' → V), is_basis K (sum.elim v v')
theorem exists_is_basis (K : Type u_4) (V : Type u) [field K] [add_comm_group V] [vector_space K V] :
∃ (b : set V), is_basis K (λ (i : b), i)
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) :
∃ (q : submodule K V), is_compl p q
@[instance]
def vector_space.submodule.is_complemented {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [vector_space 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 linear_map.exists_extend {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'] {p : submodule K V} (f : p →ₗ[K] V') :
∃ (g : V →ₗ[K] V'), g.comp p.subtype = f

Any linear map f : p →ₗ[K] V' defined on a subspace p can be extended to the whole space.

theorem submodule.exists_le_ker_of_lt_top {K : Type u_4} {V : Type u} [field K] [add_comm_group V] [vector_space K V] (p : submodule K V) (hp : p < ) :
∃ (f : V →ₗ[K] K) (H : f 0), p f.ker

If p < ⊤ is a subspace of a vector space V, then there exists a nonzero linear map f : V →ₗ[K] K such that p ≤ ker f.

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