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 LinearIndependent R v as Function.Injective (Finsupp.linearCombination R v). Here
Finsupp.linearCombination 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 ker (Finsupp.linearCombination 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.
LinearIndependent R vstates that the elements of the familyvare linearly independent.LinearIndependent.repr hv xreturns the linear combination representingx : span R (range v)on the linearly independent vectorsv, givenhv : LinearIndependent R v(using classical choice).LinearIndependent.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.linearIndependent_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 ι;linearIndependent_empty_type: a family indexed by an empty type is linearly independent;linearIndependent_unique_iff: ifιis a singleton, thenLinearIndependent K vis equivalent tov default ≠ 0;linearIndependent_option,linearIndependent_sum,linearIndependent_fin_cons,linearIndependent_fin_succ: type-specific tests for linear independence of families of vector fields;linearIndependent_insert,linearIndependent_union,linearIndependent_pair,linearIndependent_singleton: linear independence tests for set operations.
In many cases we additionally provide dot-style operations (e.g., LinearIndependent.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 (fun x ↦ x : s → M) given a set s : Set M. The lemmas
LinearIndependent.to_subtype_range and LinearIndependent.of_subtype_range connect those two
worlds.
TODO #
Rework proofs to hold in semirings, by avoiding the path through
ker (Finsupp.linearCombination R v) = ⊥.
Tags #
linearly dependent, linear dependence, linearly independent, linear independence
def
LinearIndependent
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
(v : ι → M)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearIndependent R v states the family of vectors v is linearly independent over R.
Equations
Instances For
Delaborator for LinearIndependent that suggests pretty printing with type hints
in case the family of vectors is over a Set.
Type hints look like LinearIndependent fun (v : ↑s) => ↑v or LinearIndependent (ι := ↑s) f,
depending on whether the family is a lambda expression or not.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
linearIndependent_iff_injective_linearCombination
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
LinearIndependent.injective_linearCombination
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearIndependent R v → Function.Injective ⇑(Finsupp.linearCombination R v)
Alias of the forward direction of linearIndependent_iff_injective_linearCombination.
theorem
LinearIndependent.ne_zero
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Nontrivial R]
(i : ι)
(hv : LinearIndependent R v)
:
v i ≠ 0
theorem
linearIndependent_empty_type
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[IsEmpty ι]
:
theorem
linearIndependent_empty
(R : Type u_2)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearIndependent R fun (x : ↑∅) => ↑x
theorem
LinearIndependent.comp
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(h : LinearIndependent R v)
(f : ι' → ι)
(hf : Function.Injective f)
:
LinearIndependent R (v ∘ f)
A subfamily of a linearly independent family (i.e., a composition with an injective map) is a linearly independent family.
theorem
LinearIndependent.restrict_scalars
{ι : Type u'}
{R : Type u_2}
{K : Type u_3}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring K]
[SMulWithZero R K]
[Module K M]
[IsScalarTower R K M]
(hinj : Function.Injective fun (r : R) => r • 1)
(li : LinearIndependent 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 LinearIndependent.restrict_scalars_algebras.
theorem
linearIndependent_iff_ker
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
LinearIndependent R v ↔ LinearMap.ker (Finsupp.linearCombination R v) = ⊥
theorem
linearIndependent_iff
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
LinearIndependent R v ↔ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0
theorem
linearIndependent_iff'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
theorem
linearIndependent_iff''
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
theorem
Fintype.linearIndependent_iff
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Fintype ι]
:
LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0
theorem
Fintype.linearIndependent_iff'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Fintype ι]
[DecidableEq ι]
:
LinearIndependent R v ↔ LinearMap.ker ((LinearMap.lsum R (fun (x : ι) => R) ℕ) fun (i : ι) => LinearMap.id.smulRight (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
LinearIndependent.eq_zero_of_pair
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x : M}
{y : M}
(h : LinearIndependent R ![x, y])
{s : R}
{t : R}
(h' : s • x + t • y = 0)
:
theorem
LinearIndependent.pair_iff
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x : M}
{y : M}
:
Also see LinearIndependent.pair_iff' for a simpler version over fields.
theorem
linearIndependent_iff_finset_linearIndependent
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
LinearIndependent R v ↔ ∀ (s : Finset ι), LinearIndependent R (v ∘ Subtype.val)
A family is linearly independent if and only if all of its finite subfamily is linearly independent.
theorem
LinearIndependent.coe_range
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(i : LinearIndependent R v)
:
LinearIndependent R Subtype.val
theorem
LinearIndependent.map
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
(hv : LinearIndependent R v)
{f : M →ₗ[R] M'}
(hf_inj : Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f))
:
LinearIndependent 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 LinearIndependent.map' for a special case assuming ker f = ⊥.
theorem
Submodule.range_ker_disjoint
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
{f : M →ₗ[R] M'}
(hv : LinearIndependent R (⇑f ∘ v))
:
Disjoint (Submodule.span R (Set.range v)) (LinearMap.ker f)
If v is an injective family of vectors such that f ∘ v is linearly independent, then v
spans a submodule disjoint from the kernel of f
theorem
LinearIndependent.map'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
(hv : LinearIndependent R v)
(f : M →ₗ[R] M')
(hf_inj : LinearMap.ker f = ⊥)
:
LinearIndependent R (⇑f ∘ v)
An injective linear map sends linearly independent families of vectors to linearly independent
families of vectors. See also LinearIndependent.map for a more general statement.
theorem
LinearIndependent.map_of_injective_injective
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{R' : Type u_6}
{M' : Type u_7}
[Ring R']
[AddCommGroup M']
[Module R' M']
(hv : LinearIndependent R v)
(i : R' → R)
(j : M →+ M')
(hi : ∀ (r : R'), i r = 0 → r = 0)
(hj : ∀ (m : M), j m = 0 → m = 0)
(hc : ∀ (r : R') (m : M), j (i r • m) = r • j m)
:
LinearIndependent R' (⇑j ∘ v)
If M / R and M' / R' are modules, i : R' → R is a map, j : M →+ M' is a monoid map,
such that they send non-zero elements to non-zero elements, and compatible with the scalar
multiplications on M and M', then j sends linearly independent families of vectors to
linearly independent families of vectors. As a special case, taking R = R'
it is LinearIndependent.map'.
theorem
LinearIndependent.map_of_surjective_injective
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{R' : Type u_6}
{M' : Type u_7}
[Ring R']
[AddCommGroup M']
[Module R' M']
(hv : LinearIndependent R v)
(i : ZeroHom R R')
(j : M →+ M')
(hi : Function.Surjective ⇑i)
(hj : ∀ (m : M), j m = 0 → m = 0)
(hc : ∀ (r : R) (m : M), j (r • m) = i r • j m)
:
LinearIndependent R' (⇑j ∘ v)
If M / R and M' / R' are modules, i : R → R' is a surjective map which maps zero to zero,
j : M →+ M' is a monoid map which sends non-zero elements to non-zero elements, such that the
scalar multiplications on M and M' are compatible, then j sends linearly independent families
of vectors to linearly independent families of vectors. As a special case, taking R = R'
it is LinearIndependent.map'.
theorem
LinearIndependent.of_comp
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
(f : M →ₗ[R] M')
(hfv : LinearIndependent 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
LinearMap.linearIndependent_iff
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
(f : M →ₗ[R] M')
(hf_inj : LinearMap.ker f = ⊥)
:
LinearIndependent R (⇑f ∘ v) ↔ LinearIndependent 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
linearIndependent_of_subsingleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Subsingleton R]
:
theorem
linearIndependent_equiv
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(e : ι ≃ ι')
{f : ι' → M}
:
LinearIndependent R (f ∘ ⇑e) ↔ LinearIndependent R f
theorem
linearIndependent_equiv'
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(e : ι ≃ ι')
{f : ι' → M}
{g : ι → M}
(h : f ∘ ⇑e = g)
:
LinearIndependent R g ↔ LinearIndependent R f
theorem
linearIndependent_subtype_range
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : Function.Injective f)
:
LinearIndependent R Subtype.val ↔ LinearIndependent R f
theorem
LinearIndependent.of_subtype_range
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : Function.Injective f)
:
LinearIndependent R Subtype.val → LinearIndependent R f
Alias of the forward direction of linearIndependent_subtype_range.
theorem
linearIndependent_image
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{s : Set ι}
{f : ι → M}
(hf : Set.InjOn f s)
:
(LinearIndependent R fun (x : ↑s) => f ↑x) ↔ LinearIndependent R fun (x : ↑(f '' s)) => ↑x
theorem
linearIndependent_span
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hs : LinearIndependent R v)
:
LinearIndependent R fun (i : ι) => ⟨v i, ⋯⟩
theorem
LinearIndependent.fin_cons'
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{m : ℕ}
(x : M)
(v : Fin m → M)
(hli : LinearIndependent R v)
(x_ortho : ∀ (c : R) (y : ↥(Submodule.span R (Set.range v))), c • x + ↑y = 0 → c = 0)
:
LinearIndependent R (Fin.cons x v)
See LinearIndependent.fin_cons for a family of elements in a vector space.
theorem
linearIndependent_finset_map_embedding_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : Set M)
(li : LinearIndependent R Subtype.val)
(t : Finset ↑s)
:
LinearIndependent R Subtype.val
Every finite subset of a linearly independent set is linearly independent.
theorem
linearIndependent_bounded_of_finset_linearIndependent_bounded
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{n : ℕ}
(H : ∀ (s : Finset M), (LinearIndependent R fun (i : { x : M // x ∈ s }) => ↑i) → s.card ≤ n)
(s : Set M)
:
LinearIndependent R Subtype.val → 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
linearIndependent_comp_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = 0 → l = 0
theorem
linearDependent_comp_subtype'
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0
theorem
linearDependent_comp_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
¬LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ ∃ f ∈ Finsupp.supported R R s, ∑ i ∈ f.support, f i • v i = 0 ∧ f ≠ 0
A version of linearDependent_comp_subtype' with Finsupp.linearCombination unfolded.
theorem
linearIndependent_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ ∀ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R id) l = 0 → l = 0
theorem
linearIndependent_comp_subtype_disjoint
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
:
LinearIndependent (ι := ↑s) R (v ∘ Subtype.val) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
theorem
linearIndependent_subtype_disjoint
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ Disjoint (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R id))
theorem
linearIndependent_iff_linearCombinationOn
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ LinearMap.ker (Finsupp.linearCombinationOn M M R id s) = ⊥
@[deprecated linearIndependent_iff_linearCombinationOn]
theorem
linearIndependent_iff_totalOn
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
:
(LinearIndependent R fun (x : ↑s) => ↑x) ↔ LinearMap.ker (Finsupp.linearCombinationOn M M R id s) = ⊥
theorem
LinearIndependent.restrict_of_comp_subtype
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set ι}
(hs : LinearIndependent (ι := ↑s) R (v ∘ Subtype.val))
:
LinearIndependent (ι := ↑s) R (s.restrict v)
theorem
LinearIndependent.mono
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{t : Set M}
{s : Set M}
(h : t ⊆ s)
:
(LinearIndependent R fun (x : ↑s) => ↑x) → LinearIndependent R fun (x : ↑t) => ↑x
theorem
linearIndependent_of_finite
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : Set M)
(H : ∀ t ⊆ s, t.Finite → LinearIndependent R fun (x : ↑t) => ↑x)
:
LinearIndependent R fun (x : ↑s) => ↑x
theorem
linearIndependent_iUnion_of_directed
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{η : Type u_6}
{s : η → Set M}
(hs : Directed (fun (x1 x2 : Set M) => x1 ⊆ x2) s)
(h : ∀ (i : η), LinearIndependent R fun (x : ↑(s i)) => ↑x)
:
LinearIndependent R fun (x : ↑(⋃ (i : η), s i)) => ↑x
theorem
linearIndependent_sUnion_of_directed
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set (Set M)}
(hs : DirectedOn (fun (x1 x2 : Set M) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndependent R Subtype.val)
:
LinearIndependent R fun (x : ↑(⋃₀ s)) => ↑x
theorem
linearIndependent_biUnion_of_directed
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{η : Type u_6}
{s : Set η}
{t : η → Set M}
(hs : DirectedOn (t ⁻¹'o fun (x1 x2 : Set M) => x1 ⊆ x2) s)
(h : ∀ a ∈ s, LinearIndependent R fun (x : ↑(t a)) => ↑x)
:
LinearIndependent R fun (x : ↑(⋃ a ∈ s, t a)) => ↑x
@[deprecated linearIndependent_iff_injective_linearCombination]
theorem
linearIndependent_iff_injective_total
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
@[deprecated LinearIndependent.injective_linearCombination]
theorem
LinearIndependent.injective_total
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearIndependent R v → Function.Injective ⇑(Finsupp.linearCombination R v)
Alias of the forward direction of linearIndependent_iff_injective_linearCombination.
Alias of the forward direction of linearIndependent_iff_injective_linearCombination.
theorem
LinearIndependent.injective
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
:
theorem
LinearIndependent.to_subtype_range
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : LinearIndependent R f)
:
LinearIndependent R Subtype.val
theorem
LinearIndependent.to_subtype_range'
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → M}
(hf : LinearIndependent R f)
{t : Set M}
(ht : Set.range f = t)
:
LinearIndependent R Subtype.val
theorem
LinearIndependent.image_of_comp
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{ι' : Type u_7}
(s : Set ι)
(f : ι → ι')
(g : ι' → M)
(hs : LinearIndependent R fun (x : ↑s) => g (f ↑x))
:
LinearIndependent R fun (x : ↑(f '' s)) => g ↑x
theorem
LinearIndependent.image
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{s : Set ι}
{f : ι → M}
(hs : LinearIndependent R fun (x : ↑s) => f ↑x)
:
LinearIndependent R fun (x : ↑(f '' s)) => ↑x
theorem
LinearIndependent.group_smul
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{G : Type u_6}
[hG : Group G]
[DistribMulAction G R]
[DistribMulAction G M]
[IsScalarTower G R M]
[SMulCommClass G R M]
{v : ι → M}
(hv : LinearIndependent R v)
(w : ι → G)
:
LinearIndependent R (w • v)
theorem
LinearIndependent.units_smul
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{v : ι → M}
(hv : LinearIndependent R v)
(w : ι → Rˣ)
:
LinearIndependent R (w • v)
theorem
LinearIndependent.eq_zero_of_pair'
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x : M}
{y : M}
(h : LinearIndependent R ![x, y])
{s : R}
{t : R}
(h' : s • x = t • y)
:
theorem
LinearIndependent.linear_combination_pair_of_det_ne_zero
{R : Type u_6}
{M : Type u_7}
[CommRing R]
[NoZeroDivisors R]
[AddCommGroup M]
[Module R M]
{x : M}
{y : M}
(h : LinearIndependent R ![x, y])
{a : R}
{b : R}
{c : R}
{d : R}
(h' : a * d - b * c ≠ 0)
:
If two vectors x and y are linearly independent, so are their linear combinations
a x + b y and c x + d y provided the determinant a * d - b * c is nonzero.
def
LinearIndependent.Maximal
{ι : Type w}
{R : Type u}
[Ring R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{v : ι → M}
(_i : LinearIndependent R v)
:
A linearly independent family is maximal if there is no strictly larger linearly independent family.
Equations
Instances For
theorem
LinearIndependent.maximal_iff
{ι : Type w}
{R : Type u}
[Ring R]
[Nontrivial R]
{M : Type v}
[AddCommGroup M]
[Module R M]
{v : ι → M}
(i : LinearIndependent R v)
:
i.Maximal ↔ ∀ (κ : Type v) (w : κ → M), LinearIndependent 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
LinearIndependent.eq_of_smul_apply_eq_smul_apply
{ι : Type u'}
{R : Type u_2}
[Ring R]
{M : Type u_6}
[AddCommGroup M]
[Module R M]
{v : ι → M}
(li : LinearIndependent R v)
(c : R)
(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
LinearIndependent.disjoint_span_image
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
{s : Set ι}
{t : Set ι}
(hs : Disjoint s t)
:
Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t))
theorem
LinearIndependent.not_mem_span_image
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
{s : Set ι}
{x : ι}
(h : x ∉ s)
:
v x ∉ Submodule.span R (v '' s)
theorem
LinearIndependent.linearCombination_ne_of_not_mem_support
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
{x : ι}
(f : ι →₀ R)
(h : x ∉ f.support)
:
(Finsupp.linearCombination R v) f ≠ v x
@[deprecated LinearIndependent.linearCombination_ne_of_not_mem_support]
theorem
LinearIndependent.total_ne_of_not_mem_support
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
{x : ι}
(f : ι →₀ R)
(h : x ∉ f.support)
:
(Finsupp.linearCombination R v) f ≠ v x
Alias of LinearIndependent.linearCombination_ne_of_not_mem_support.
theorem
linearIndependent_sum
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{v : ι ⊕ ι' → M}
:
LinearIndependent R v ↔ LinearIndependent R (v ∘ Sum.inl) ∧ LinearIndependent R (v ∘ Sum.inr) ∧ Disjoint (Submodule.span R (Set.range (v ∘ Sum.inl))) (Submodule.span R (Set.range (v ∘ Sum.inr)))
theorem
LinearIndependent.sum_type
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
{v' : ι' → M}
(hv : LinearIndependent R v)
(hv' : LinearIndependent R v')
(h : Disjoint (Submodule.span R (Set.range v)) (Submodule.span R (Set.range v')))
:
LinearIndependent R (Sum.elim v v')
theorem
LinearIndependent.union
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{s : Set M}
{t : Set M}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(ht : LinearIndependent R fun (x : ↑t) => ↑x)
(hst : Disjoint (Submodule.span R s) (Submodule.span R t))
:
LinearIndependent R fun (x : ↑(s ∪ t)) => ↑x
theorem
linearIndependent_iUnion_finite_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_6}
{f : ι → Set M}
(hl : ∀ (i : ι), LinearIndependent R fun (x : ↑(f i)) => ↑x)
(hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (Submodule.span R (f i)) (⨆ i ∈ t, Submodule.span R (f i)))
:
LinearIndependent R fun (x : ↑(⋃ (i : ι), f i)) => ↑x
theorem
linearIndependent_iUnion_finite
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{η : Type u_6}
{ιs : η → Type u_7}
{f : (j : η) → ιs j → M}
(hindep : ∀ (j : η), LinearIndependent R (f j))
(hd : ∀ (i : η) (t : Set η),
t.Finite → i ∉ t → Disjoint (Submodule.span R (Set.range (f i))) (⨆ i ∈ t, Submodule.span R (Set.range (f i))))
:
LinearIndependent R fun (ji : (j : η) × ιs j) => f ji.fst ji.snd
@[simp]
theorem
LinearIndependent.linearCombinationEquiv_symm_apply
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
∀ (a : ↥(Submodule.span R (Set.range v))),
hv.linearCombinationEquiv.symm a = ((LinearEquiv.ofInjective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯)
⋯).toEquiv.trans
(LinearEquiv.ofTop
(LinearMap.range
(LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯))
⋯).toEquiv).invFun
a
def
LinearIndependent.linearCombinationEquiv
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
(ι →₀ R) ≃ₗ[R] ↥(Submodule.span R (Set.range v))
Canonical isomorphism between linear combinations and the span of linearly independent vectors.
Equations
- hv.linearCombinationEquiv = LinearEquiv.ofBijective (LinearMap.codRestrict (Submodule.span R (Set.range v)) (Finsupp.linearCombination R v) ⋯) ⋯
Instances For
@[deprecated LinearIndependent.linearCombinationEquiv]
def
LinearIndependent.totalEquiv
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
(ι →₀ R) ≃ₗ[R] ↥(Submodule.span R (Set.range v))
Alias of LinearIndependent.linearCombinationEquiv.
Canonical isomorphism between linear combinations and the span of linearly independent vectors.
Instances For
@[simp]
theorem
LinearIndependent.linearCombinationEquiv_apply_coe
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
(l : ι →₀ R)
:
↑(hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
@[deprecated LinearIndependent.linearCombinationEquiv_apply_coe]
theorem
LinearIndependent.totalEquiv_apply_coe
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
(l : ι →₀ R)
:
↑(hv.linearCombinationEquiv l) = (Finsupp.linearCombination R v) l
Alias of LinearIndependent.linearCombinationEquiv_apply_coe.
def
LinearIndependent.repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
↥(Submodule.span R (Set.range v)) →ₗ[R] ι →₀ R
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 LinearIndependent.linearCombinationEquiv.
Equations
- hv.repr = ↑hv.linearCombinationEquiv.symm
Instances For
@[simp]
theorem
LinearIndependent.linearCombination_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
(x : ↥(Submodule.span R (Set.range v)))
:
(Finsupp.linearCombination R v) (hv.repr x) = ↑x
@[deprecated LinearIndependent.linearCombination_repr]
theorem
LinearIndependent.total_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
(x : ↥(Submodule.span R (Set.range v)))
:
(Finsupp.linearCombination R v) (hv.repr x) = ↑x
Alias of LinearIndependent.linearCombination_repr.
theorem
LinearIndependent.linearCombination_comp_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
Finsupp.linearCombination R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype
@[deprecated LinearIndependent.linearCombination_comp_repr]
theorem
LinearIndependent.total_comp_repr
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
Finsupp.linearCombination R v ∘ₗ hv.repr = (Submodule.span R (Set.range v)).subtype
theorem
LinearIndependent.repr_ker
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
LinearMap.ker hv.repr = ⊥
theorem
LinearIndependent.repr_range
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
LinearMap.range hv.repr = ⊤
theorem
LinearIndependent.repr_eq
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
{l : ι →₀ R}
{x : ↥(Submodule.span R (Set.range v))}
(eq : (Finsupp.linearCombination R v) l = ↑x)
:
hv.repr x = l
theorem
LinearIndependent.repr_eq_single
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
(i : ι)
(x : ↥(Submodule.span R (Set.range v)))
(hx : ↑x = v i)
:
hv.repr x = Finsupp.single i 1
theorem
LinearIndependent.span_repr_eq
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
[Nontrivial R]
(x : ↥(Submodule.span R (Set.range v)))
:
Span.repr R (Set.range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)
theorem
linearIndependent_iff_not_smul_mem_span
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
:
LinearIndependent R v ↔ ∀ (i : ι) (a : R), a • v i ∈ Submodule.span R (v '' (Set.univ \ {i})) → a = 0
theorem
LinearIndependent.independent_span_singleton
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
(hv : LinearIndependent R v)
:
CompleteLattice.Independent fun (i : ι) => Submodule.span R {v i}
See also CompleteLattice.independent_iff_linearIndependent_of_ne_zero.
theorem
exists_maximal_independent'
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : ι → M)
:
∃ (I : Set ι),
(LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ (J : Set ι), I ⊆ J → (LinearIndependent R fun (x : ↑J) => s ↑x) → I = J
theorem
exists_maximal_independent
{ι : Type u'}
(R : Type u_2)
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : ι → M)
:
∃ (I : Set ι),
(LinearIndependent R fun (x : ↑I) => s ↑x) ∧ ∀ i ∉ I, ∃ (a : R), a ≠ 0 ∧ a • s i ∈ Submodule.span R (s '' I)
theorem
surjective_of_linearIndependent_of_span
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{v : ι → M}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
(hv : LinearIndependent R v)
(f : ι' ↪ ι)
(hss : Set.range v ⊆ ↑(Submodule.span R (Set.range (v ∘ ⇑f))))
:
theorem
eq_of_linearIndependent_of_span_subtype
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
{s : Set M}
{t : Set M}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(h : t ⊆ s)
(hst : s ⊆ ↑(Submodule.span R t))
:
s = t
theorem
LinearIndependent.image_subtype
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
{s : Set M}
{f : M →ₗ[R] M'}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(hf_inj : Disjoint (Submodule.span R s) (LinearMap.ker f))
:
LinearIndependent R fun (x : ↑(⇑f '' s)) => ↑x
theorem
LinearIndependent.inl_union_inr
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
{s : Set M}
{t : Set M'}
(hs : LinearIndependent R fun (x : ↑s) => ↑x)
(ht : LinearIndependent R fun (x : ↑t) => ↑x)
:
LinearIndependent R fun (x : ↑(⇑(LinearMap.inl R M M') '' s ∪ ⇑(LinearMap.inr R M M') '' t)) => ↑x
theorem
linearIndependent_inl_union_inr'
{ι : Type u'}
{ι' : Type u_1}
{R : Type u_2}
{M : Type u_4}
{M' : Type u_5}
[Ring R]
[AddCommGroup M]
[AddCommGroup M']
[Module R M]
[Module R M']
{v : ι → M}
{v' : ι' → M'}
(hv : LinearIndependent R v)
(hv' : LinearIndependent R v')
:
LinearIndependent R (Sum.elim (⇑(LinearMap.inl R M M') ∘ v) (⇑(LinearMap.inr R M M') ∘ v'))
theorem
linearIndependent_monoidHom
(G : Type u_6)
[Monoid G]
(L : Type u_7)
[CommRing L]
[NoZeroDivisors L]
:
LinearIndependent L fun (f : G →* L) => ⇑f
Dedekind's linear independence of characters
theorem
linearIndependent_algHom_toLinearMap
(K : Type u_6)
(M : Type u_7)
(L : Type u_8)
[CommSemiring K]
[Semiring M]
[Algebra K M]
[CommRing L]
[IsDomain L]
[Algebra K L]
:
LinearIndependent L AlgHom.toLinearMap
theorem
linearIndependent_algHom_toLinearMap'
(K : Type u_6)
(M : Type u_7)
(L : Type u_8)
[CommRing K]
[Semiring M]
[Algebra K M]
[CommRing L]
[IsDomain L]
[Algebra K L]
[NoZeroSMulDivisors K L]
:
LinearIndependent K AlgHom.toLinearMap
theorem
le_of_span_le_span
{R : Type u_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
{s : Set M}
{t : Set M}
{u : Set M}
(hl : LinearIndependent R Subtype.val)
(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_2}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Nontrivial R]
{s : Set M}
{t : Set M}
{u : Set M}
(hl : LinearIndependent R Subtype.val)
(hsu : s ⊆ u)
(htu : t ⊆ u)
:
Submodule.span R s ≤ Submodule.span R t ↔ s ⊆ t
theorem
linearIndependent_unique_iff
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[Nontrivial R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(v : ι → M)
[Unique ι]
:
LinearIndependent R v ↔ v default ≠ 0
theorem
linearIndependent_unique
{ι : Type u'}
{R : Type u_2}
{M : Type u_4}
[Ring R]
[Nontrivial R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(v : ι → M)
[Unique ι]
:
v default ≠ 0 → LinearIndependent R v
Alias of the reverse direction of linearIndependent_unique_iff.
theorem
linearIndependent_singleton
{R : Type u_2}
{M : Type u_4}
[Ring R]
[Nontrivial R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
{x : M}
(hx : x ≠ 0)
:
LinearIndependent R fun (x_1 : ↑{x}) => ↑x_1
Properties which require DivisionRing K #
These can be considered generalizations of properties of linear independence in vector spaces.
theorem
mem_span_insert_exchange
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
{y : V}
:
x ∈ Submodule.span K (insert y s) → x ∉ Submodule.span K s → y ∈ Submodule.span K (insert x s)
theorem
linearIndependent_iff_not_mem_span
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
:
LinearIndependent K v ↔ ∀ (i : ι), v i ∉ Submodule.span K (v '' (Set.univ \ {i}))
theorem
LinearIndependent.insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hs : LinearIndependent K fun (b : ↑s) => ↑b)
(hx : x ∉ Submodule.span K s)
:
LinearIndependent K fun (b : ↑(insert x s)) => ↑b
theorem
linearIndependent_option'
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{x : V}
:
(LinearIndependent K fun (o : Option ι) => o.casesOn' x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
theorem
LinearIndependent.option
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : ι → V}
{x : V}
(hv : LinearIndependent K v)
(hx : x ∉ Submodule.span K (Set.range v))
:
LinearIndependent K fun (o : Option ι) => o.casesOn' x v
theorem
linearIndependent_option
{ι : Type u'}
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{v : Option ι → V}
:
LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ Submodule.span K (Set.range (v ∘ some))
theorem
linearIndependent_insert'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{ι : Type u_6}
{s : Set ι}
{a : ι}
{f : ι → V}
(has : a ∉ s)
:
(LinearIndependent K fun (x : ↑(insert a s)) => f ↑x) ↔ (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ Submodule.span K (f '' s)
theorem
linearIndependent_insert
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{x : V}
(hxs : x ∉ s)
:
(LinearIndependent K fun (b : ↑(insert x s)) => ↑b) ↔ (LinearIndependent K fun (b : ↑s) => ↑b) ∧ x ∉ Submodule.span K s
theorem
linearIndependent_pair
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{y : V}
(hx : x ≠ 0)
(hy : ∀ (a : K), a • x ≠ y)
:
LinearIndependent K Subtype.val
theorem
LinearIndependent.pair_iff'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{y : V}
(hx : x ≠ 0)
:
LinearIndependent K ![x, y] ↔ ∀ (a : K), a • x ≠ y
Also see LinearIndependent.pair_iff for the version over arbitrary rings.
theorem
linearIndependent_fin_cons
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
:
LinearIndependent K (Fin.cons x v) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
theorem
linearIndependent_fin_snoc
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
:
LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
theorem
LinearIndependent.fin_cons
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{n : ℕ}
{v : Fin n → V}
(hv : LinearIndependent K v)
(hx : x ∉ Submodule.span K (Set.range v))
:
LinearIndependent K (Fin.cons x v)
See LinearIndependent.fin_cons' for an uglier version that works if you
only have a module over a semiring.
theorem
linearIndependent_fin_succ
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
{v : Fin (n + 1) → V}
:
LinearIndependent K v ↔ LinearIndependent K (Fin.tail v) ∧ v 0 ∉ Submodule.span K (Set.range (Fin.tail v))
theorem
linearIndependent_fin_succ'
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{n : ℕ}
{v : Fin (n + 1) → V}
:
LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ Submodule.span K (Set.range (Fin.init v))
def
equiv_linearIndependent
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(n : ℕ)
:
{ s : Fin (n + 1) → V // LinearIndependent K s } ≃ (s : { s : Fin n → V // LinearIndependent K s }) × ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ
Equivalence between k + 1 vectors of length n and k vectors of length n along with a
vector in the complement of their span.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
linearIndependent_fin2
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{f : Fin 2 → V}
:
theorem
exists_linearIndependent_extension
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K Subtype.val)
(hst : s ⊆ t)
:
∃ b ⊆ t, s ⊆ b ∧ t ⊆ ↑(Submodule.span K b) ∧ LinearIndependent K Subtype.val
theorem
exists_linearIndependent
(K : Type u_3)
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(t : Set V)
:
∃ b ⊆ t, Submodule.span K b = Submodule.span K t ∧ LinearIndependent K Subtype.val
noncomputable def
LinearIndependent.extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
Set V
LinearIndependent.extend adds vectors to a linear independent set s ⊆ t until it spans
all elements of t.
Equations
- hs.extend hst = Classical.choose ⋯
Instances For
theorem
LinearIndependent.extend_subset
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
hs.extend hst ⊆ t
theorem
LinearIndependent.subset_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
s ⊆ hs.extend hst
theorem
LinearIndependent.subset_span_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
t ⊆ ↑(Submodule.span K (hs.extend hst))
theorem
LinearIndependent.span_extend_eq_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
Submodule.span K (hs.extend hst) = Submodule.span K t
theorem
LinearIndependent.linearIndependent_extend
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ t)
:
LinearIndependent K Subtype.val
theorem
exists_of_linearIndependent_of_finite_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Finset V}
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ ↑(Submodule.span K ↑t))
:
theorem
exists_finite_card_le_of_finite_of_linearIndependent_of_span
{K : Type u_3}
{V : Type u}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Set V}
{t : Set V}
(ht : t.Finite)
(hs : LinearIndependent K fun (x : ↑s) => ↑x)
(hst : s ⊆ ↑(Submodule.span K t))
:
∃ (h : s.Finite), h.toFinset.card ≤ ht.toFinset.card