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.
-
linear_independent R vstates that the elements of the familyvare linearly independent. -
linear_independent.repr hv xreturns the linear combination representingx : span R (range v)on the linearly independent vectorsv, givenhv : linear_independent R v(using classical choice).linear_independent.repr hvis provided as a linear map.
Main statements #
We prove several specialized tests for linear independence of families of vectors and of sets of vectors.
fintype.linear_independent_iff: ifιis a finite type, then any functionf : ι → Rhas finite support, so we can reformulate the statement using∑ i : ι, f i • v iinstead of a sum over an auxiliarys : finset ι;linear_independent_empty_type: a family indexed by an empty type is linearly independent;linear_independent_unique_iff: ifιis a singleton, thenlinear_independent K vis equivalent tov default ≠ 0;- linear_independent_option
,linear_independent_sum,linear_independent_fin_cons,linear_independent_fin_succ`: type-specific tests for linear independence of families of vector fields; linear_independent_insert,linear_independent_union,linear_independent_pair,linear_independent_singleton: linear independence tests for set operations.
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, when working over a division ring, any family of vectors includes a linear independent subfamily spanning the same subspace.
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]
[module R M] :
Prop
linear_independent R v states the family of vectors v is linearly independent over R.
Equations
- linear_independent R v = (linear_map.ker (finsupp.total ι M R v) = ⊥)
theorem
linear_independent_iff
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M] :
linear_independent R v ↔ ∀ (l : ι →₀ R), ⇑(finsupp.total ι M R v) l = 0 → l = 0
theorem
linear_independent_iff'
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
linear_independent_iff''
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
not_linear_independent_iff
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M] :
theorem
fintype.linear_independent_iff
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M]
[fintype ι] :
linear_independent R v ↔ ∀ (g : ι → R), finset.univ.sum (λ (i : ι), g i • v i) = 0 → ∀ (i : ι), 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]
[module R M]
[fintype ι] :
linear_independent R v ↔ linear_map.ker (⇑(linear_map.lsum R (λ (i : ι), R) ℕ) (λ (i : ι), linear_map.id.smul_right (v i))) = ⊥
A finite family of vectors v i is linear independent iff the linear map that sends
c : ι → R to ∑ i, c i • v i has the trivial kernel.
theorem
fintype.not_linear_independent_iff
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M]
[fintype ι] :
¬linear_independent R v ↔ ∃ (g : ι → R), finset.univ.sum (λ (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]
[module R M]
[is_empty ι] :
theorem
linear_independent.ne_zero
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module 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]
[module R M]
(h : linear_independent R v)
(f : ι' → ι)
(hf : function.injective f) :
linear_independent R (v ∘ f)
A subfamily of a linearly independent family (i.e., a composition with an injective map) is a linearly independent family.
theorem
linear_independent.coe_range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M]
(i : linear_independent R v) :
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']
[module R M]
[module R M']
(hv : linear_independent R v)
{f : M →ₗ[R] M'}
(hf_inj : disjoint (submodule.span R (set.range v)) (linear_map.ker f)) :
linear_independent R (⇑f ∘ v)
If v is a linearly independent family of vectors and the kernel of a linear map f is
disjoint with the submodule spanned 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']
[module R M]
[module R M']
(hv : linear_independent R v)
(f : M →ₗ[R] M')
(hf_inj : linear_map.ker f = ⊥) :
linear_independent R (⇑f ∘ v)
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']
[module R M]
[module 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.
@[protected]
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']
[module R M]
[module R M']
(f : M →ₗ[R] M')
(hf_inj : linear_map.ker f = ⊥) :
linear_independent R (⇑f ∘ v) ↔ linear_independent R v
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]
[module 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]
[module R M]
(e : ι ≃ ι')
{f : ι' → M} :
linear_independent R (f ∘ ⇑e) ↔ linear_independent R f
theorem
linear_independent_equiv'
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
(e : ι ≃ ι')
{f : ι' → M}
{g : ι → M}
(h : f ∘ ⇑e = g) :
linear_independent R g ↔ linear_independent R f
theorem
linear_independent_subtype_range
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module 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]
[module R M]
{ι : Type u_1}
{f : ι → M}
(hf : function.injective f) :
linear_independent R coe → linear_independent R f
Alias of the forward direction of linear_independent_subtype_range.
theorem
linear_independent_image
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module 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]
[module R M]
(hs : linear_independent R v) :
linear_independent R (λ (i : ι), ⟨v i, _⟩)
theorem
linear_independent.fin_cons'
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
{m : ℕ}
(x : M)
(v : fin m → M)
(hli : linear_independent R v)
(x_ortho : ∀ (c : R) (y : ↥(submodule.span R (set.range v))), c • x + ↑y = 0 → c = 0) :
linear_independent R (fin.cons x v)
See linear_independent.fin_cons for a family of elements in a vector space.
theorem
linear_independent.restrict_scalars
{ι : Type u_1}
{R : Type u_3}
{K : Type u_4}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M]
[semiring K]
[smul_with_zero R K]
[module K M]
[is_scalar_tower R K M]
(hinj : function.injective (λ (r : R), r • 1))
(li : linear_independent K v) :
A set of linearly independent vectors in a module M over a semiring K is also linearly
independent over a subring R of K.
The implementation uses minimal assumptions about the relationship between R, K and M.
The version where K is an R-algebra is linear_independent.restrict_scalars_algebras.
theorem
linear_independent_finset_map_embedding_subtype
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
(s : set M)
(li : linear_independent R coe)
(t : finset ↥s) :
Every finite subset of a linearly independent set is linearly independent.
theorem
linear_independent_bounded_of_finset_linear_independent_bounded
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
{n : ℕ}
(H : ∀ (s : finset M), linear_independent R (λ (i : ↥s), ↑i) → s.card ≤ n)
(s : set M) :
linear_independent R coe → cardinal.mk ↥s ≤ ↑n
If every finite set of linearly independent vectors has cardinality at most n,
then the same is true for arbitrary sets of linearly independent vectors.
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]
[module R M]
{s : set ι} :
linear_independent R (v ∘ coe) ↔ ∀ (l : ι →₀ R), l ∈ finsupp.supported R R s → ⇑(finsupp.total ι M R v) l = 0 → l = 0
theorem
linear_dependent_comp_subtype'
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set ι} :
¬linear_independent R (v ∘ coe) ↔ ∃ (f : ι →₀ R), f ∈ finsupp.supported R R s ∧ ⇑(finsupp.total ι M R v) f = 0 ∧ f ≠ 0
theorem
linear_dependent_comp_subtype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set ι} :
A version of linear_dependent_comp_subtype' with finsupp.total unfolded.
theorem
linear_independent_subtype
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module 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 = 0 → l = 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]
[module R M]
{s : set ι} :
linear_independent R (v ∘ coe) ↔ disjoint (finsupp.supported R R s) (linear_map.ker (finsupp.total ι M R v))
theorem
linear_independent_subtype_disjoint
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
linear_independent R (λ (x : ↥s), ↑x) ↔ disjoint (finsupp.supported R R s) (linear_map.ker (finsupp.total M M R id))
theorem
linear_independent_iff_total_on
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
{s : set M} :
linear_independent R (λ (x : ↥s), ↑x) ↔ linear_map.ker (finsupp.total_on M M R id s) = ⊥
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]
[module R M]
{s : set ι}
(hs : linear_independent R (v ∘ coe)) :
linear_independent R (s.restrict v)
theorem
linear_independent_empty
(R : Type u_3)
(M : Type u_5)
[semiring R]
[add_comm_monoid M]
[module R M] :
linear_independent R (λ (x : ↥∅), ↑x)
theorem
linear_independent.mono
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module 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]
[module R M]
(s : set M)
(H : ∀ (t : set M), t ⊆ s → t.finite → linear_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]
[module 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]
[module R M]
{s : set (set M)}
(hs : directed_on has_subset.subset s)
(h : ∀ (a : set M), a ∈ s → linear_independent R (λ (x : ↥a), ↑x)) :
linear_independent R (λ (x : ↥⋃₀ s), ↑x)
theorem
linear_independent_bUnion_of_directed
{R : Type u_3}
{M : Type u_5}
[semiring R]
[add_comm_monoid M]
[module R M]
{η : Type u_1}
{s : set η}
{t : η → set M}
(hs : directed_on (t ⁻¹'o has_subset.subset) s)
(h : ∀ (a : η), a ∈ s → linear_independent R (λ (x : ↥(t a)), ↑x)) :
linear_independent R (λ (x : ↥⋃ (a : η) (H : a ∈ s), t a), ↑x)
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] :
linear_independent R v ↔ function.injective ⇑(finsupp.total ι M R v)
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] :
linear_independent R v → function.injective ⇑(finsupp.total ι M R v)
Alias of the forward direction 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_of_comp
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
{ι : Type u_1}
{ι' : Type u_2}
(s : set ι)
(f : ι → ι')
(g : ι' → M)
(hs : linear_independent R (λ (x : ↥s), g (f ↑x))) :
linear_independent R (λ (x : ↥(f '' s)), g ↑x)
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)
theorem
linear_independent.group_smul
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
{G : Type u_2}
[hG : group G]
[distrib_mul_action G R]
[distrib_mul_action G M]
[is_scalar_tower G R M]
[smul_comm_class G R M]
{v : ι → M}
(hv : linear_independent R v)
(w : ι → G) :
linear_independent R (w • v)
theorem
linear_independent.units_smul
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
{v : ι → M}
(hv : linear_independent R v)
(w : ι → Rˣ) :
linear_independent R (w • v)
@[nolint]
def
linear_independent.maximal
{ι : Type w}
{R : Type u}
[semiring R]
{M : Type v}
[add_comm_monoid M]
[module R M]
{v : ι → M}
(i : linear_independent R v) :
Prop
A linearly independent family is maximal if there is no strictly larger linearly independent family.
theorem
linear_independent.maximal_iff
{ι : Type w}
{R : Type u}
[ring R]
[nontrivial R]
{M : Type v}
[add_comm_group M]
[module R M]
{v : ι → M}
(i : linear_independent R v) :
i.maximal ↔ ∀ (κ : Type v) (w : κ → M), linear_independent R w → ∀ (j : ι → κ), w ∘ j = v → function.surjective j
An alternative characterization of a maximal linearly independent family,
quantifying over types (in the same universe as M) into which the indexing family injects.
theorem
linear_independent.eq_of_smul_apply_eq_smul_apply
{ι : Type u_1}
{R : Type u_3}
[ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{v : ι → M}
(li : linear_independent R v)
(c d : R)
(i j : ι)
(hc : c ≠ 0)
(h : c • v i = d • v j) :
i = j
Linear independent families are injective, even if you multiply either side.
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) :
disjoint (submodule.span R (v '' s)) (submodule.span R (v '' t))
theorem
linear_independent.not_mem_span_image
{ι : 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)
{s : set ι}
{x : ι}
(h : x ∉ s) :
v x ∉ submodule.span R (v '' s)
theorem
linear_independent.total_ne_of_not_mem_support
{ι : 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)
{x : ι}
(f : ι →₀ R)
(h : x ∉ f.support) :
⇑(finsupp.total ι M R v) f ≠ v x
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} :
linear_independent R v ↔ linear_independent R (v ∘ sum.inl) ∧ linear_independent R (v ∘ sum.inr) ∧ disjoint (submodule.span R (set.range (v ∘ sum.inl))) (submodule.span R (set.range (v ∘ sum.inr)))
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'))) :
linear_independent R (sum.elim v 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.finite → i ∉ t → disjoint (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.finite → i ∉ t → disjoint (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)
@[simp]
theorem
linear_independent.total_equiv_apply_coe
{ι : 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)
(ᾰ : ι →₀ R) :
↑(⇑(hv.total_equiv) ᾰ) = ⇑(finsupp.total ι M R v) ᾰ
noncomputable
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
- hv.total_equiv = linear_equiv.of_bijective (linear_map.cod_restrict (submodule.span R (set.range v)) (finsupp.total ι M R v) linear_independent.total_equiv._proof_3) _ linear_independent.total_equiv._proof_7
@[simp]
theorem
linear_independent.total_equiv_symm_apply
{ι : 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)
(ᾰ : ↥(submodule.span R (set.range v))) :
⇑(hv.total_equiv.symm) ᾰ = ((linear_equiv.of_injective (linear_map.cod_restrict (submodule.span R (set.range v)) (finsupp.total ι M R v) linear_independent.total_equiv._proof_3) _).to_equiv.trans (linear_equiv.of_top (linear_map.range (linear_map.cod_restrict (submodule.span R (set.range v)) (finsupp.total ι M R v) linear_independent.total_equiv._proof_3)) _).to_equiv).inv_fun ᾰ
noncomputable
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
- hv.repr = ↑(hv.total_equiv.symm)
@[simp]
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))) :
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) :
(finsupp.total ι M R v).comp hv.repr = (submodule.span R (set.range v)).subtype
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) :
linear_map.ker hv.repr = ⊥
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) :
linear_map.range hv.repr = ⊤
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) :
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) :
⇑(hv.repr) x = finsupp.single i 1
theorem
linear_independent.span_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)
[nontrivial R]
(x : ↥(submodule.span R (set.range v))) :
span.repr R (set.range v) x = finsupp.equiv_map_domain (equiv.of_injective v _) (⇑(hv.repr) x)
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
linear_independent.independent_span_singleton
{ι : 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) :
complete_lattice.independent (λ (i : ι), submodule.span R {v i})
See also complete_lattice.independent_iff_linear_independent_of_ne_zero.
theorem
exists_maximal_independent'
{ι : Type u_1}
(R : Type u_3)
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
(s : ι → M) :
theorem
exists_maximal_independent
{ι : Type u_1}
(R : Type u_3)
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
(s : ι → M) :
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) (linear_map.ker f)) :
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') :
linear_independent R (sum.elim (⇑(linear_map.inl R M M') ∘ v) (⇑(linear_map.inr R M M') ∘ 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) :
submodule.span R s ≤ submodule.span R t ↔ s ⊆ t
theorem
linear_independent_unique_iff
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(v : ι → M)
[unique ι] :
linear_independent R v ↔ v inhabited.default ≠ 0
theorem
linear_independent_unique
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
(v : ι → M)
[unique ι] :
v inhabited.default ≠ 0 → linear_independent R v
Alias of the reverse direction of linear_independent_unique_iff.
theorem
linear_independent_singleton
{R : Type u_3}
{M : Type u_5}
[ring R]
[nontrivial R]
[add_comm_group M]
[module R M]
[no_zero_smul_divisors R M]
{x : M}
(hx : x ≠ 0) :
linear_independent R (λ (x_1 : ↥{x}), ↑x_1)
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]
[module K V]
{s : set V}
{x y : V} :
x ∈ submodule.span K (has_insert.insert y s) → x ∉ submodule.span K s → y ∈ submodule.span K (has_insert.insert x s)
theorem
linear_independent_iff_not_mem_span
{ι : Type u_1}
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{v : ι → V} :
linear_independent K v ↔ ∀ (i : ι), v i ∉ submodule.span K (v '' (set.univ \ {i}))
theorem
linear_independent.insert
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
{x : V}
(hs : linear_independent K (λ (b : ↥s), ↑b))
(hx : x ∉ submodule.span K s) :
linear_independent K (λ (b : ↥(has_insert.insert x s)), ↑b)
theorem
linear_independent_option'
{ι : Type u_1}
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{v : ι → V}
{x : V} :
linear_independent K (λ (o : option ι), o.cases_on' x v) ↔ linear_independent K v ∧ x ∉ submodule.span K (set.range v)
theorem
linear_independent.option
{ι : Type u_1}
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module 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]
[module K V]
{v : option ι → V} :
linear_independent K v ↔ linear_independent K (v ∘ coe) ∧ v option.none ∉ submodule.span K (set.range (v ∘ coe))
theorem
linear_independent_insert'
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{ι : Type u_1}
{s : set ι}
{a : ι}
{f : ι → V}
(has : a ∉ s) :
linear_independent K (λ (x : ↥(has_insert.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]
[module K V]
{s : set V}
{x : V}
(hxs : x ∉ s) :
linear_independent K (λ (b : ↥(has_insert.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]
[module 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]
[module K V]
{x : V}
{n : ℕ}
{v : fin n → V} :
linear_independent K (fin.cons x v) ↔ linear_independent K v ∧ x ∉ submodule.span K (set.range v)
theorem
linear_independent_fin_snoc
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{x : V}
{n : ℕ}
{v : fin n → V} :
linear_independent K (fin.snoc v x) ↔ linear_independent K v ∧ x ∉ submodule.span K (set.range v)
theorem
linear_independent.fin_cons
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{x : V}
{n : ℕ}
{v : fin n → V}
(hv : linear_independent K v)
(hx : x ∉ submodule.span K (set.range v)) :
linear_independent K (fin.cons x v)
See linear_independent.fin_cons' for an uglier version that works if you
only have a module over a semiring.
theorem
linear_independent_fin_succ
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
{v : fin (n + 1) → V} :
linear_independent K v ↔ linear_independent K (fin.tail v) ∧ v 0 ∉ submodule.span K (set.range (fin.tail v))
theorem
linear_independent_fin_succ'
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{n : ℕ}
{v : fin (n + 1) → V} :
linear_independent K v ↔ linear_independent K (fin.init v) ∧ v (fin.last n) ∉ submodule.span K (set.range (fin.init v))
theorem
linear_independent_fin2
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{f : fin 2 → V} :
theorem
exists_linear_independent_extension
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s t : set V}
(hs : linear_independent K coe)
(hst : s ⊆ t) :
∃ (b : set V) (H : b ⊆ t), s ⊆ b ∧ t ⊆ ↑(submodule.span K b) ∧ linear_independent K coe
theorem
exists_linear_independent
(K : Type u_4)
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
(t : set V) :
∃ (b : set V) (H : b ⊆ t), submodule.span K b = submodule.span K t ∧ linear_independent K coe
def
linear_independent.extend
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s t : set V}
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ t) :
set V
linear_independent.extend adds vectors to a linear independent set s ⊆ t until it spans
all elements of t.
Equations
- hs.extend hst = classical.some _
theorem
linear_independent.extend_subset
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s t : set V}
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ t) :
theorem
linear_independent.subset_extend
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s t : set V}
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ t) :
theorem
linear_independent.subset_span_extend
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s t : set V}
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ t) :
t ⊆ ↑(submodule.span K (hs.extend hst))
theorem
linear_independent.linear_independent_extend
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s t : set V}
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ t) :
theorem
exists_of_linear_independent_of_finite_span
{K : Type u_4}
{V : Type u}
[division_ring K]
[add_comm_group V]
[module K V]
{s : set V}
{t : finset V}
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ ↑(submodule.span K ↑t)) :
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]
[module K V]
{s t : set V}
(ht : t.finite)
(hs : linear_independent K (λ (x : ↥s), ↑x))
(hst : s ⊆ ↑(submodule.span K t)) :