Linear independence and bases
This file defines linear independence and bases in a module or vector space.
It is inspired by Isabelle/HOL's linear algebra, and hence indirectly by HOL Light.
Main definitions
All definitions are given for families of vectors, i.e. v : ι → M where M is the module or
vector space and ι : Type* is an arbitrary indexing type.
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.is_basis R vstates that the vector familyvis a basis, i.e. it is linearly independent and spans the entire space.is_basis.repr hv xis the basis version oflinear_independent.repr hv x. It returns the linear combination representingx : Mon a basisvofM(using classical choice). The argumenthvmust be a proof thatis_basis R v.is_basis.repr hvis given as a linear map as well.is_basis.constr hv fconstructs a linear mapM₁ →ₗ[R] M₂given the valuesf : ι → M₂at the basisv : ι → M₁, givenhv : is_basis R v.
Main statements
is_basis.extstates that two linear maps are equal if they coincide on a basis.exists_is_basisstates that every vector space has a basis.
Implementation notes
We use families instead of sets because it allows us to say that two identical vectors are linearly
dependent. For bases, this is useful as well because we can easily derive ordered bases by using an
ordered index type ι.
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, basis
def
linear_independent
{ι : Type u_1}
(R : Type u_3)
{M : Type u_5}
(v : ι → M)
[ring R]
[add_comm_group M]
[module R M] :
Prop
Linearly independent family of vectors
Equations
- linear_independent R v = ((finsupp.total ι M R v).ker = ⊥)
theorem
linear_independent_iff
{ι : 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 ↔ ∀ (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}
[ring R]
[add_comm_group M]
[module R M] :
theorem
linear_independent_iff''
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
theorem
linear_dependent_iff
{ι : 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_empty_type
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
¬nonempty ι → linear_independent R v
theorem
linear_independent.ne_zero
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[nontrivial R]
{i : ι} :
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}
[ring R]
[add_comm_group M]
[module R M]
(h : linear_independent R v)
(f : ι' → ι) :
function.injective f → linear_independent R (v ∘ f)
theorem
linear_independent_of_zero_eq_one
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
0 = 1 → linear_independent R v
theorem
linear_independent.unique
{ι : 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₁ l₂ : ι →₀ R} :
⇑(finsupp.total ι M R v) l₁ = ⇑(finsupp.total ι M R v) l₂ → l₁ = l₂
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] :
linear_independent R v → function.injective v
theorem
linear_independent_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 → 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}
[ring R]
[add_comm_group 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_independent_subtype
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group 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}
[ring R]
[add_comm_group M]
[module R M]
{s : set ι} :
linear_independent R (v ∘ coe) ↔ disjoint (finsupp.supported R R s) (finsupp.total ι M R v).ker
theorem
linear_independent_subtype_disjoint
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
{s : set M} :
linear_independent R (λ (x : ↥s), ↑x) ↔ disjoint (finsupp.supported R R s) (finsupp.total M M R id).ker
theorem
linear_independent_iff_total_on
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
{s : set M} :
linear_independent R (λ (x : ↥s), ↑x) ↔ (finsupp.total_on M M R id s).ker = ⊥
theorem
linear_independent.to_subtype_range
{ι : 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 → linear_independent R (λ (x : ↥(set.range v)), ↑x)
theorem
linear_independent.of_subtype_range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
function.injective v → linear_independent R (λ (x : ↥(set.range v)), ↑x) → linear_independent R v
theorem
linear_independent.restrict_of_comp_subtype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
{s : set ι} :
linear_independent R (v ∘ coe) → linear_independent R (set.restrict v s)
theorem
linear_independent_empty
(R : Type u_3)
(M : Type u_5)
[ring R]
[add_comm_group M]
[module R M] :
linear_independent R (λ (x : ↥∅), ↑x)
theorem
linear_independent.mono
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
{t s : set M} :
t ⊆ s → linear_independent R (λ (x : ↥s), ↑x) → linear_independent R (λ (x : ↥t), ↑x)
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} :
linear_independent R (λ (x : ↥s), ↑x) → linear_independent R (λ (x : ↥t), ↑x) → disjoint (submodule.span R s) (submodule.span R t) → linear_independent R (λ (x : ↥(s ∪ t)), ↑x)
theorem
linear_independent_of_finite
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M]
(s : set M) :
(∀ (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}
[ring R]
[add_comm_group M]
[module R M]
{η : Type u_1}
{s : η → set M} :
directed has_subset.subset s → (∀ (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}
[ring R]
[add_comm_group M]
[module R M]
{s : set (set M)} :
directed_on has_subset.subset s → (∀ (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}
[ring R]
[add_comm_group M]
[module R M]
{η : Type u_1}
{s : set η}
{t : η → set M} :
directed_on (t ⁻¹'o has_subset.subset) s → (∀ (a : η), a ∈ s → linear_independent R (λ (x : ↥(t a)), ↑x)) → linear_independent R (λ (x : ↥⋃ (a : η) (H : a ∈ s), t a), ↑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} :
(∀ (i : ι), linear_independent R (λ (x : ↥(f i)), ↑x)) → (∀ (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} :
(∀ (j : η), linear_independent R (f j)) → (∀ (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)
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] :
linear_independent R v → ((ι →₀ R) ≃ₗ[R] ↥(submodule.span R (set.range 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_1) _ linear_independent.total_equiv._proof_3
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] :
linear_independent 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 linear_independent.total_equiv.
Equations
- hv.repr = ↑(hv.total_equiv.symm)
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) :
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))} :
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))) :
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 : ι' ↪ ι) :
set.range v ⊆ ↑(submodule.span R (set.range (v ∘ ⇑f))) → function.surjective ⇑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} :
linear_independent R (λ (x : ↥s), ↑x) → t ⊆ s → s ⊆ ↑(submodule.span R t) → s = t
theorem
linear_independent.image
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : linear_independent R v)
{f : M →ₗ[R] M'} :
disjoint (submodule.span R (set.range v)) f.ker → linear_independent R (⇑f ∘ v)
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'} :
linear_independent R (λ (x : ↥s), ↑x) → 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'} :
linear_independent R (λ (x : ↥s), ↑x) → 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'} :
linear_independent R v → 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)
[integral_domain 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} :
linear_independent R coe → s ⊆ u → t ⊆ u → 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} :
linear_independent R coe → s ⊆ u → t ⊆ u → (submodule.span R s ≤ submodule.span R t ↔ s ⊆ t)
def
is_basis
{ι : Type u_1}
(R : Type u_3)
{M : Type u_5}
(v : ι → M)
[ring R]
[add_comm_group M]
[module R M] :
Prop
A family of vectors is a basis if it is linearly independent and all vectors are in the span.
Equations
- is_basis R v = (linear_independent R v ∧ submodule.span R (set.range v) = ⊤)
theorem
is_basis.mem_span
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(x : M) :
x ∈ submodule.span R (set.range v)
theorem
is_basis.comp
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(f : ι' → ι) :
function.bijective f → is_basis R (v ∘ f)
theorem
is_basis.injective
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[nontrivial R] :
is_basis R v → function.injective v
theorem
is_basis.range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
def
is_basis.repr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
Given a basis, any vector can be written as a linear combination of the basis vectors. They are
given by this linear map. This is one direction of module_equiv_finsupp.
Equations
- hv.repr = _.repr.comp (linear_map.cod_restrict (submodule.span R (set.range v)) linear_map.id _)
theorem
is_basis.total_repr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(x : M) :
⇑(finsupp.total ι M R v) (⇑(hv.repr) x) = x
theorem
is_basis.total_comp_repr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
(finsupp.total ι M R v).comp hv.repr = linear_map.id
theorem
is_basis.repr_ker
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
theorem
is_basis.repr_range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
hv.repr.range = finsupp.supported R R set.univ
theorem
is_basis.repr_total
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(x : ι →₀ R) :
x ∈ finsupp.supported R R set.univ → ⇑(hv.repr) (⇑(finsupp.total ι M R v) x) = x
theorem
is_basis.repr_eq_single
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
{i : ι} :
⇑(hv.repr) (v i) = finsupp.single i 1
def
is_basis.constr
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M'] :
Construct a linear map given the value at the basis.
Equations
- hv.constr f = (finsupp.total M' M' R id).comp ((finsupp.lmap_domain R R f).comp hv.repr)
theorem
is_basis.constr_apply
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(f : ι → M')
(x : M) :
theorem
is_basis.ext
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{f g : M →ₗ[R] M'} :
@[simp]
theorem
constr_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{f : ι → M'}
{i : ι}
(hv : is_basis R v) :
theorem
constr_self
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(f : M →ₗ[R] M') :
theorem
constr_zero
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v) :
theorem
constr_add
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{g f : ι → M'}
(hv : is_basis R v) :
theorem
constr_neg
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{f : ι → M'}
(hv : is_basis R v) :
theorem
constr_sub
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
{g f : ι → M'}
(hs : is_basis R v) :
theorem
constr_range
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
[nonempty ι]
(hv : is_basis R v)
{f : ι → M'} :
(hv.constr f).range = submodule.span R (set.range f)
def
module_equiv_finsupp
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
Canonical equivalence between a module and the linear combinations of basis vectors.
Equations
- module_equiv_finsupp hv = (_.total_equiv.trans (linear_equiv.of_top (submodule.span R (set.range v)) _)).symm
@[simp]
theorem
module_equiv_finsupp_apply_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v)
(i : ι) :
⇑(module_equiv_finsupp hv) (v i) = finsupp.single i 1
def
equiv_of_is_basis
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{v : ι → M}
{v' : ι' → M'} :
Isomorphism between the two modules, given two modules M and M' with respective bases
v and v' and a bijection between the indexing sets of the two bases.
def
equiv_of_is_basis'
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{v : ι → M}
{v' : ι' → M'}
(f : M → M')
(g : M' → M) :
Isomorphism between the two modules, given two modules M and M' with respective bases
v and v' and a bijection between the two bases.
@[simp]
theorem
equiv_of_is_basis_comp
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{M'' : Type u_7}
[ring R]
[add_comm_group M]
[add_comm_group M']
[add_comm_group M'']
[module R M]
[module R M']
[module R M'']
{ι'' : Type u_4}
{v : ι → M}
{v' : ι' → M'}
{v'' : ι'' → M''}
(hv : is_basis R v)
(hv' : is_basis R v')
(hv'' : is_basis R v'')
(e : ι ≃ ι')
(f : ι' ≃ ι'') :
(equiv_of_is_basis hv hv' e).trans (equiv_of_is_basis hv' hv'' f) = equiv_of_is_basis hv hv'' (e.trans f)
@[simp]
theorem
equiv_of_is_basis_refl
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
(hv : is_basis R v) :
equiv_of_is_basis hv hv (equiv.refl ι) = linear_equiv.refl R M
theorem
equiv_of_is_basis_trans_symm
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(e : ι ≃ ι')
{v' : ι' → M'}
(hv' : is_basis R v') :
(equiv_of_is_basis hv hv' e).trans (equiv_of_is_basis hv' hv e.symm) = linear_equiv.refl R M
theorem
equiv_of_is_basis_symm_trans
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hv : is_basis R v)
(e : ι ≃ ι')
{v' : ι' → M'}
(hv' : is_basis R v') :
(equiv_of_is_basis hv' hv e.symm).trans (equiv_of_is_basis hv hv' e) = linear_equiv.refl R M'
theorem
is_basis_inl_union_inr
{ι : Type u_1}
{ι' : Type u_2}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
{v : ι → M}
{v' : ι' → M'} :
is_basis R v → is_basis R v' → is_basis R (sum.elim (⇑(linear_map.inl R M M') ∘ v) (⇑(linear_map.inr R M M') ∘ v'))
theorem
is_basis_singleton_one
{ι : Type u_1}
(R : Type u_2)
[unique ι]
[ring R] :
is_basis R (λ (_x : ι), 1)
theorem
linear_equiv.is_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{M' : Type u_6}
{v : ι → M}
[ring R]
[add_comm_group M]
[add_comm_group M']
[module R M]
[module R M']
(hs : is_basis R v)
(f : M ≃ₗ[R] M') :
theorem
is_basis_span
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M] :
linear_independent R v → is_basis R (λ (i : ι), ⟨v i, _⟩)
theorem
is_basis_empty
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M] :
theorem
is_basis_empty_bot
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
[ring R]
[add_comm_group M]
[module R M] :
def
equiv_fun_basis
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι] :
A module over R with a finite basis is linearly equivalent to functions from its basis to R.
Equations
- equiv_fun_basis h = (module_equiv_finsupp h).trans {to_fun := finsupp.to_fun (mul_zero_class.to_has_zero R), map_add' := _, map_smul' := _, inv_fun := finsupp.equiv_fun_on_fintype.inv_fun, left_inv := _, right_inv := _}
def
module.fintype_of_fintype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v)
[fintype R] :
fintype M
A module over a finite ring that admits a finite basis is finite.
Equations
- module.fintype_of_fintype h = fintype.of_equiv (ι → R) (equiv_fun_basis h).to_equiv.symm
theorem
module.card_fintype
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v)
[fintype R]
[fintype M] :
fintype.card M = fintype.card R ^ fintype.card ι
@[simp]
theorem
equiv_fun_basis_symm_apply
{ι : Type u_1}
{R : Type u_3}
{M : Type u_5}
{v : ι → M}
[ring R]
[add_comm_group M]
[module R M]
[fintype ι]
(h : is_basis R v)
(x : ι → R) :
⇑((equiv_fun_basis h).symm) x = finset.univ.sum (λ (i : ι), x i • v i)
Given a basis v indexed by ι, the canonical linear equivalence between ι → R and M maps
a function x : ι → R to the linear combination ∑_i x i • v i.
theorem
mem_span_insert_exchange
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space 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}
{v : ι → V}
[field K]
[add_comm_group V]
[vector_space K V] :
linear_independent K v ↔ ∀ (i : ι), v i ∉ submodule.span K (v '' (set.univ \ {i}))
theorem
linear_independent_unique
{ι : Type u_1}
{K : Type u_4}
{V : Type u}
{v : ι → V}
[field K]
[add_comm_group V]
[vector_space K V]
[unique ι] :
v (inhabited.default ι) ≠ 0 → linear_independent K v
theorem
linear_independent_singleton
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{x : V} :
x ≠ 0 → linear_independent K (λ (x_1 : ↥{x}), ↑x_1)
theorem
disjoint_span_singleton
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{p : submodule K V}
{x : V} :
x ≠ 0 → (disjoint p (submodule.span K {x}) ↔ x ∉ p)
theorem
linear_independent.insert
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{s : set V}
{x : V} :
linear_independent K (λ (b : ↥s), ↑b) → x ∉ submodule.span K s → linear_independent K (λ (b : ↥(has_insert.insert x s)), ↑b)
theorem
exists_linear_independent
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{s t : set V} :
linear_independent K (λ (x : ↥s), ↑x) → s ⊆ t → (∃ (b : set V) (H : b ⊆ t), s ⊆ b ∧ t ⊆ ↑(submodule.span K b) ∧ linear_independent K (λ (x : ↥b), ↑x))
theorem
exists_subset_is_basis
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{s : set V} :
theorem
exists_sum_is_basis
{ι : Type u_1}
{K : Type u_4}
{V : Type u}
{v : ι → V}
[field K]
[add_comm_group V]
[vector_space K V] :
linear_independent K v → (∃ (ι' : Type u) (v' : ι' → V), is_basis K (sum.elim v v'))
theorem
exists_is_basis
(K : Type u_4)
(V : Type u)
[field K]
[add_comm_group V]
[vector_space K V] :
theorem
exists_finite_card_le_of_finite_of_linear_independent_of_span
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
{s t : set V}
(ht : t.finite) :
theorem
linear_map.exists_left_inverse_of_injective
{K : Type u_4}
{V : Type u}
{V' : Type u_8}
[field K]
[add_comm_group V]
[add_comm_group V']
[vector_space K V]
[vector_space K V']
(f : V →ₗ[K] V') :
theorem
submodule.exists_is_compl
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
(p : submodule K V) :
theorem
linear_map.exists_right_inverse_of_surjective
{K : Type u_4}
{V : Type u}
{V' : Type u_8}
[field K]
[add_comm_group V]
[add_comm_group V']
[vector_space K V]
[vector_space K V']
(f : V →ₗ[K] V') :
theorem
quotient_prod_linear_equiv
{K : Type u_4}
{V : Type u}
[field K]
[add_comm_group V]
[vector_space K V]
(p : submodule K V) :
theorem
vector_space.card_fintype
(K : Type u_4)
(V : Type u)
[field K]
[add_comm_group V]
[vector_space K V]
[fintype K]
[fintype V] :
∃ (n : ℕ), fintype.card V = fintype.card K ^ n
theorem
pi.linear_independent_std_basis
{R : Type u_3}
{η : Type u_9}
{ιs : η → Type u_10}
{Ms : η → Type u_11}
[ring R]
[Π (i : η), add_comm_group (Ms i)]
[Π (i : η), module R (Ms i)]
(v : Π (j : η), ιs j → Ms j) :
(∀ (i : η), linear_independent R (v i)) → linear_independent R (λ (ji : Σ (j : η), ιs j), ⇑(linear_map.std_basis R Ms ji.fst) (v ji.fst ji.snd))
theorem
pi.is_basis_std_basis
{R : Type u_3}
{η : Type u_9}
{ιs : η → Type u_10}
{Ms : η → Type u_11}
[ring R]
[Π (i : η), add_comm_group (Ms i)]
[Π (i : η), module R (Ms i)]
[fintype η]
(s : Π (j : η), ιs j → Ms j) :
theorem
pi.is_basis_fun₀
(R : Type u_3)
(η : Type u_9)
[ring R]
[fintype η] :
is_basis R (λ (ji : Σ (j : η), unit), ⇑(linear_map.std_basis R (λ (i : η), R) ji.fst) 1)
theorem
pi.is_basis_fun
(R : Type u_3)
(η : Type u_9)
[ring R]
[fintype η] :
is_basis R (λ (i : η), ⇑(linear_map.std_basis R (λ (i : η), R) i) 1)