mathlib documentation

linear_algebra.linear_independent

Linear independence #

This file defines linear independence in a module or vector space.

It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.

We define linear_independent R v as ker (finsupp.total ι M R v) = ⊥. Here finsupp.total is the linear map sending a function f : ι →₀ R with finite support to the linear combination of vectors from v with these coefficients. Then we prove that several other statements are equivalent to this one, including injectivity of finsupp.total ι M R v and some versions with explicitly written linear combinations.

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 #

We prove several specialized tests for linear independence of families of vectors and of sets of vectors.

In many cases we additionally provide dot-style operations (e.g., linear_independent.union) to make the linear independence tests usable as hv.insert ha etc.

We also prove that any family of vectors includes a linear independent subfamily spanning the same submodule.

Implementation notes #

We use families instead of sets because it allows us to say that two identical vectors are linearly dependent.

If you want to use sets, use the family (λ x, x : s → M) given a set s : set M. The lemmas linear_independent.to_subtype_range and linear_independent.of_subtype_range connect those two worlds.

Tags #

linearly dependent, linear dependence, linearly independent, linear independence

def linear_independent {ι : Type u_1} (R : Type u_3) {M : Type u_5} (v : ι → M) [semiring R] [add_comm_monoid M] [semimodule R M] :
Prop

linear_independent R v states the family of vectors v is linearly independent over R.

Equations
theorem linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] :
linear_independent R v ∀ (l : ι →₀ R), (finsupp.total ι M R v) l = 0l = 0
theorem linear_independent_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] :
linear_independent R v ∀ (s : finset ι) (g : ι → R), ∑ (i : ι) in s, g i v i = 0∀ (i : ι), i sg i = 0
theorem linear_independent_iff'' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] :
linear_independent R v ∀ (s : finset ι) (g : ι → R), (∀ (i : ι), i sg i = 0)∑ (i : ι) in s, g i v i = 0∀ (i : ι), g i = 0
theorem linear_dependent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] :
¬linear_independent R v ∃ (s : finset ι) (g : ι → R), ∑ (i : ι) in s, g i v i = 0 ∃ (i : ι) (H : i s), g i 0
theorem fintype.linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] [fintype ι] :
linear_independent R v ∀ (g : ι → R), ∑ (i : ι), g i v i = 0∀ (i : ι), g i = 0
theorem linear_independent_empty_type {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] (h : ¬nonempty ι) :
theorem linear_independent.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] [nontrivial R] (i : ι) (hv : linear_independent R v) :
v i 0
theorem linear_independent.comp {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] (h : linear_independent R v) (f : ι' → ι) (hf : function.injective f) :

A subfamily of a linearly independent family (i.e., a composition with an injective map) is a linearly independent family.

theorem linear_independent.map {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [semimodule R M] [semimodule R M'] (hv : linear_independent R v) {f : M →ₗ[R] M'} (hf_inj : disjoint (submodule.span R (set.range v)) f.ker) :

If v is a linearly independent family of vectors and the kernel of a linear map f is disjoint with the sumodule spaned by the vectors of v, then f ∘ v is a linearly independent family of vectors. See also linear_independent.map' for a special case assuming ker f = ⊥.

theorem linear_independent.map' {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [semimodule R M] [semimodule R M'] (hv : linear_independent R v) (f : M →ₗ[R] M') (hf_inj : f.ker = ) :

An injective linear map sends linearly independent families of vectors to linearly independent families of vectors. See also linear_independent.map for a more general statement.

theorem linear_independent.of_comp {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [semimodule R M] [semimodule R M'] (f : M →ₗ[R] M') (hfv : linear_independent R (f v)) :

If the image of a family of vectors under a linear map is linearly independent, then so is the original family.

theorem linear_map.linear_independent_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} {M' : Type u_6} {v : ι → M} [semiring R] [add_comm_monoid M] [add_comm_monoid M'] [semimodule R M] [semimodule R M'] (f : M →ₗ[R] M') (hf_inj : f.ker = ) :

If f is an injective linear map, then the family f ∘ v is linearly independent if and only if the family v is linearly independent.

theorem linear_independent_of_subsingleton {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] [subsingleton R] :
theorem linear_independent_equiv {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] (e : ι ι') {f : ι' → M} :
theorem linear_independent_equiv' {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] (e : ι ι') {f : ι' → M} {g : ι → M} (h : f e = g) :
theorem linear_independent_subtype_range {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Type u_1} {f : ι → M} (hf : function.injective f) :
theorem linear_independent.of_subtype_range {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Type u_1} {f : ι → M} (hf : function.injective f) :

Alias of linear_independent_subtype_range.

theorem linear_independent_image {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {ι : Type u_1} {s : set ι} {f : ι → M} (hf : set.inj_on f s) :
linear_independent R (λ (x : s), f x) linear_independent R (λ (x : (f '' s)), x)
theorem linear_independent_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] (hs : linear_independent R v) :
linear_independent R (λ (i : ι), v i, _⟩)

The following lemmas use the subtype defined by a set in M as the index set ι.

theorem linear_independent_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set ι} :
linear_independent R (v coe) ∀ (l : ι →₀ R), l finsupp.supported R R s(finsupp.total ι M R v) l = 0l = 0
theorem linear_independent_subtype {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} :
linear_independent R (λ (x : s), x) ∀ (l : M →₀ R), l finsupp.supported R R s(finsupp.total M M R id) l = 0l = 0
theorem linear_independent_comp_subtype_disjoint {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set ι} :
theorem linear_independent_subtype_disjoint {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} :
theorem linear_independent_iff_total_on {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set M} :
theorem linear_independent.restrict_of_comp_subtype {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set ι} (hs : linear_independent R (v coe)) :
theorem linear_independent_empty (R : Type u_3) (M : Type u_5) [semiring R] [add_comm_monoid M] [semimodule R M] :
theorem linear_independent.mono {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {t s : set M} (h : t s) :
linear_independent R (λ (x : s), x)linear_independent R (λ (x : t), x)
theorem linear_independent_of_finite {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] (s : set M) (H : ∀ (t : set M), t st.finitelinear_independent R (λ (x : t), x)) :
linear_independent R (λ (x : s), x)
theorem linear_independent_Union_of_directed {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {η : Type u_1} {s : η → set M} (hs : directed has_subset.subset s) (h : ∀ (i : η), linear_independent R (λ (x : (s i)), x)) :
linear_independent R (λ (x : ⋃ (i : η), s i), x)
theorem linear_independent_sUnion_of_directed {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {s : set (set M)} (hs : directed_on has_subset.subset s) (h : ∀ (a : set M), a slinear_independent R (λ (x : a), x)) :
theorem linear_independent_bUnion_of_directed {R : Type u_3} {M : Type u_5} [semiring R] [add_comm_monoid M] [semimodule R M] {η : Type u_1} {s : set η} {t : η → set M} (hs : directed_on (t ⁻¹'o has_subset.subset) s) (h : ∀ (a : η), a slinear_independent R (λ (x : (t a)), x)) :
linear_independent R (λ (x : ⋃ (a : η) (H : a s), t a), x)

Properties which require ring R #

theorem linear_independent_iff_injective_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] :
theorem linear_independent.injective_total {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] :

Alias of linear_independent_iff_injective_total.

theorem linear_independent.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 : linear_independent R v) :
theorem linear_independent.to_subtype_range {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {f : ι → M} (hf : linear_independent R f) :
theorem linear_independent.to_subtype_range' {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {f : ι → M} (hf : linear_independent R f) {t : set M} (ht : set.range f = t) :
theorem linear_independent.image {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {s : set ι} {f : ι → M} (hs : linear_independent R (λ (x : s), f x)) :
linear_independent R (λ (x : (f '' s)), x)

The following lemmas use the subtype defined by a set in M as the index set ι.

theorem linear_independent.disjoint_span_image {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) {s t : set ι} (hs : disjoint s t) :
theorem linear_independent_sum {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {v : ι ι' → M} :
theorem linear_independent.sum_type {ι : 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] {v' : ι' → M} (hv : linear_independent R v) (hv' : linear_independent R v') (h : disjoint (submodule.span R (set.range v)) (submodule.span R (set.range v'))) :
theorem linear_independent.union {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {s t : set M} (hs : linear_independent R (λ (x : s), x)) (ht : linear_independent R (λ (x : t), x)) (hst : disjoint (submodule.span R s) (submodule.span R t)) :
linear_independent R (λ (x : (s t)), x)
theorem linear_independent_Union_finite_subtype {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {ι : Type u_1} {f : ι → set M} (hl : ∀ (i : ι), linear_independent R (λ (x : (f i)), x)) (hd : ∀ (i : ι) (t : set ι), t.finitei tdisjoint (submodule.span R (f i)) (⨆ (i : ι) (H : i t), submodule.span R (f i))) :
linear_independent R (λ (x : ⋃ (i : ι), f i), x)
theorem linear_independent_Union_finite {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] {η : Type u_1} {ιs : η → Type u_2} {f : Π (j : η), ιs j → M} (hindep : ∀ (j : η), linear_independent R (f j)) (hd : ∀ (i : η) (t : set η), t.finitei tdisjoint (submodule.span R (set.range (f i))) (⨆ (i : η) (H : i t), submodule.span R (set.range (f i)))) :
linear_independent R (λ (ji : Σ (j : η), ιs j), f ji.fst ji.snd)
def linear_independent.total_equiv {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :

Canonical isomorphism between linear combinations and the span of linearly independent vectors.

Equations
def linear_independent.repr {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) :

Linear combination representing a vector in the span of linearly independent vectors.

Given a family of linearly independent vectors, we can represent any vector in their span as a linear combination of these vectors. These are provided by this linear map. It is simply one direction of linear_independent.total_equiv.

Equations
theorem linear_independent.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 : linear_independent R v) (x : (submodule.span R (set.range v))) :
(finsupp.total ι M R v) ((hv.repr) x) = x
theorem linear_independent.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 : linear_independent R v) :
theorem linear_independent.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 : linear_independent R v) :
theorem linear_independent.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 : linear_independent R v) :
theorem linear_independent.repr_eq {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] (hv : linear_independent R v) {l : ι →₀ R} {x : (submodule.span R (set.range v))} (eq : (finsupp.total ι M R v) l = x) :
(hv.repr) x = l
theorem linear_independent.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 : linear_independent R v) (i : ι) (x : (submodule.span R (set.range v))) (hx : x = v i) :
theorem linear_independent_iff_not_smul_mem_span {ι : Type u_1} {R : Type u_3} {M : Type u_5} {v : ι → M} [ring R] [add_comm_group M] [module R M] :
linear_independent R v ∀ (i : ι) (a : R), a v i submodule.span R (v '' (set.univ \ {i}))a = 0
theorem surjective_of_linear_independent_of_span {ι : 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] [nontrivial R] (hv : linear_independent R v) (f : ι' ι) (hss : set.range v (submodule.span R (set.range (v f)))) :
theorem eq_of_linear_independent_of_span_subtype {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] {s t : set M} (hs : linear_independent R (λ (x : s), x)) (h : t s) (hst : s (submodule.span R t)) :
s = t
theorem linear_independent.image_subtype {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'] {s : set M} {f : M →ₗ[R] M'} (hs : linear_independent R (λ (x : s), x)) (hf_inj : disjoint (submodule.span R s) f.ker) :
linear_independent R (λ (x : (f '' s)), x)
theorem linear_independent.inl_union_inr {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'] {s : set M} {t : set M'} (hs : linear_independent R (λ (x : s), x)) (ht : linear_independent R (λ (x : t), x)) :
linear_independent R (λ (x : ((linear_map.inl R M M') '' s (linear_map.inr R M M') '' t)), x)
theorem linear_independent_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 : linear_independent R v) (hv' : linear_independent R v') :
theorem linear_independent_monoid_hom (G : Type u_1) [monoid G] (L : Type u_2) [comm_ring L] [no_zero_divisors L] :
linear_independent L (λ (f : G →* L), f)

Dedekind's linear independence of characters

theorem le_of_span_le_span {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] {s t u : set M} (hl : linear_independent R coe) (hsu : s u) (htu : t u) (hst : submodule.span R s submodule.span R t) :
s t
theorem span_le_span_iff {R : Type u_3} {M : Type u_5} [ring R] [add_comm_group M] [module R M] [nontrivial R] {s t u : set M} (hl : linear_independent R coe) (hsu : s u) (htu : t u) :

Properties which require division_ring K #

These can be considered generalizations of properties of linear independence in vector_spaces.

theorem mem_span_insert_exchange {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {s : set V} {x y : V} :
theorem linear_independent_iff_not_mem_span {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {v : ι → V} :
linear_independent K v ∀ (i : ι), v i submodule.span K (v '' (set.univ \ {i}))
theorem linear_independent_unique_iff {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {v : ι → V} [unique ι] :
theorem linear_independent_unique {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {v : ι → V} [unique ι] :
v (default ι) 0linear_independent K v

Alias of linear_independent_unique_iff.

theorem linear_independent_singleton {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {x : V} (hx : x 0) :
linear_independent K (λ (x_1 : {x}), x_1)
theorem linear_independent_option' {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {v : ι → V} {x : V} :
theorem linear_independent.option {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {v : ι → V} {x : V} (hv : linear_independent K v) (hx : x submodule.span K (set.range v)) :
linear_independent K (λ (o : option ι), o.cases_on' x v)
theorem linear_independent_option {ι : Type u_1} {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {v : option ι → V} :
theorem linear_independent.insert {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {s : set V} {x : V} (hs : linear_independent K (λ (b : s), b)) (hx : x submodule.span K s) :
linear_independent K (λ (b : (insert x s)), b)
theorem linear_independent_insert' {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {ι : Type u_1} {s : set ι} {a : ι} {f : ι → V} (has : a s) :
linear_independent K (λ (x : (insert a s)), f x) linear_independent K (λ (x : s), f x) f a submodule.span K (f '' s)
theorem linear_independent_insert {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {s : set V} {x : V} (hxs : x s) :
linear_independent K (λ (b : (insert x s)), b) linear_independent K (λ (b : s), b) x submodule.span K s
theorem linear_independent_pair {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {x y : V} (hx : x 0) (hy : ∀ (a : K), a x y) :
theorem linear_independent_fin_cons {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {x : V} {n : } {v : fin n → V} :
theorem linear_independent.fin_cons {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {x : V} {n : } {v : fin n → V} (hv : linear_independent K v) (hx : x submodule.span K (set.range v)) :
theorem linear_independent_fin_succ {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {n : } {v : fin (n + 1) → V} :
theorem linear_independent_fin2 {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {f : fin 2 → V} :
linear_independent K f f 1 0 ∀ (a : K), a f 1 f 0
theorem exists_linear_independent {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {s t : set V} (hs : linear_independent K (λ (x : s), x)) (hst : s t) :
∃ (b : set V) (H : b t), s b t (submodule.span K b) linear_independent K (λ (x : b), x)
theorem exists_of_linear_independent_of_finite_span {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {s : set V} {t : finset V} (hs : linear_independent K (λ (x : s), x)) (hst : s (submodule.span K t)) :
∃ (t' : finset V), t' s t s t' t'.card = t.card
theorem exists_finite_card_le_of_finite_of_linear_independent_of_span {K : Type u_4} {V : Type u} [division_ring K] [add_comm_group V] [semimodule K V] {s t : set V} (ht : t.finite) (hs : linear_independent K (λ (x : s), x)) (hst : s (submodule.span K t)) :