Bases in a vector space #
This file provides results for bases of a vector space.
Some of these results should be merged with the results on free modules. We state these results in a separate file to the results on modules to avoid an import cycle.
Main statements #
Basis.ofVectorSpace
states that every vector space has a basis.Module.Free.of_divisionRing
states that every vector space is a free module.
Tags #
basis, bases
If s
is a linear independent set of vectors, we can extend it to a basis.
Equations
- Basis.extend hs = Basis.mk ⋯ ⋯
Instances For
Auxiliary definition: the index for the new basis vectors in Basis.sumExtend
.
The specific value of this definition should be considered an implementation detail.
Equations
- Basis.sumExtendIndex hs = ⋯.extend ⋯ \ Set.range v
Instances For
If v
is a linear independent family of vectors, extend it to a basis indexed by a sum type.
Equations
- Basis.sumExtend hs = (Basis.extend ⋯).reindex (Trans.trans ((Equiv.ofInjective v ⋯).sumCongr (Equiv.refl ↑(⋯.extend ⋯ \ Set.range v))) (Equiv.Set.sumDiffSubset ⋯)).symm
Instances For
A set used to index Basis.ofVectorSpace
.
Equations
- Basis.ofVectorSpaceIndex K V = ⋯.extend ⋯
Instances For
Each vector space has a basis.
Equations
- Basis.ofVectorSpace K V = Basis.extend ⋯
Instances For
Equations
- ⋯ = ⋯
For a module over a division ring, the span of a nonzero element is an atom of the lattice of submodules.
The atoms of the lattice of submodules of a module over a division ring are the submodules equal to the span of a nonzero element of the module.
The lattice of submodules of a module over a division ring is atomistic.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Any linear map f : p →ₗ[K] V'
defined on a subspace p
can be extended to the whole
space.
If p < ⊤
is a subspace of a vector space V
, then there exists a nonzero linear map
f : V →ₗ[K] K
such that p ≤ ker f
.