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.
All definitions are given for families of vectors, i.e. v : ι → M where M is the module or vectorspace and ι : Type* is an arbitrary indexing type.
linear_independent R v states that the elements of the family v are linear independent
linear_independent.repr hv x returns the linear combination representing x : span R (range v) on the linear independent vectors v, given hv : linear_independent R v (using classical choice). linear_independent.repr hv is provided as a linear map.
is_basis R v states that the vector family v is a basis, i.e. it is linear independent and spans the entire space
is_basis.repr hv x is the basis version of linear_independent.repr hv x. It returns the linear combination representing x : M on a basis v of M (using classical choice). The argument hv must be a proof that is_basis R v. is_basis.repr hv is given as a linear map as well.
is_basis.constr hv f constructs a linear map M₁ →ₗ[R] M₂ given the values f : ι → M₂ at the basis v : ι → M₁, given hv : is_basis R v.
is_basis.ext states that two linear maps are equal if they coincide on a basis.
exists_is_basis states that every vector space has a basis.
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.
linearly dependent, linear dependence, linearly independent, linear independence, basis
Linearly independent family of vectors
Canonical isomorphism between linear combinations and the span of linearly independent vectors.
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
Dedekind's linear independence of characters
A family of vectors is a basis if it is linearly independent and all vectors are in the span.
Construct a linear map given the value at the basis.
Canonical equivalence between a module and the linear combinations of basis vectors.
Isomorphism between the two modules, given two modules M and M' with respective bases v and v' and a bijection between the two bases.
A module over R with a finite basis is linearly equivalent to functions from its basis to R.