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.

is_basis R v states that the vector family v is a basis, i.e. it is linearly independent and spans the entire space.
is_basis.repr hv x is the basis version of linear_independent.repr hv x. It returns the linear combination representing x : M on a basis v of M (using classical choice). The argument hv must be a proof that is_basis R v. is_basis.repr hv is given as a linear map as well.
is_basis.constr hv f constructs a linear map M₁ →ₗ[R] M₂ given the values f : ι → M₂ at the basis v : ι → M₁, given hv : is_basis R v.

Main statements #

is_basis.ext states that two linear maps are equal if they coincide on a basis.
exists_is_basis states 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) :

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) :

function.injective 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) :

M →ₗ[R] ι →₀ R

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) :

hv.repr.ker = ⊥

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

@[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') :

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) :

⇑(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'} :

(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) :

M ≃ₗ[R] ι →₀ R

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.

Equations

linear_equiv_of_is_basis hv hv' e = {to_fun := (hv.constr (v' ∘ ⇑e)).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(hv'.constr (v ∘ ⇑(e.symm))), left_inv := _, right_inv := _}

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.

Equations

linear_equiv_of_is_basis' f g hv hv' hf hg hgf hfg = {to_fun := (hv.constr (f ∘ v)).to_fun, map_add' := _, map_smul' := _, inv_fun := ⇑(hv'.constr (g ∘ v')), left_inv := _, right_inv := _}

@[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'))

@[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] :

no_zero_smul_divisors R M

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') :

is_basis R (⇑f ∘ v)

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

h.equiv_fun = (module_equiv_finsupp h).trans {to_fun := coe_fn finsupp.has_coe_to_fun, 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] :

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) :

⇑(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] :

is_complemented (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 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) :

nonempty ((p.quotient × ↥p) ≃ₗ[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