Bases
This file defines 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.
is_basis R v
states that the vector familyv
is a basis, i.e. it is linearly independent and spans the entire space.is_basis.repr hv x
is the basis version oflinear_independent.repr hv x
. It returns the linear combination representingx : M
on a basisv
ofM
(using classical choice). The argumenthv
must be a proof thatis_basis R v
.is_basis.repr hv
is given as a linear map as well.is_basis.constr hv f
constructs a linear mapM₁ →ₗ[R] M₂
given the valuesf : ι → M₂
at the basisv : ι → M₁
, givenhv : is_basis R v
.
Main statements
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.
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 ι
.
Tags
basis, bases
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) = ⊤)
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 _)
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)
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
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.
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
.
Equations
- h.equiv_fun = (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 := _}
A module over a finite ring that admits a finite basis is finite.
Equations
- module.fintype_of_fintype h = fintype.of_equiv (ι → R) h.equiv_fun.to_equiv.symm
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
.