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
- One or more equations did not get rendered due to their size.
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 = LinearIndependent.extend (_ : LinearIndependent K Subtype.val) (_ : Set.range v ⊆ Set.univ) \ 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
- One or more equations did not get rendered due to their size.
Instances For
A set used to index Basis.ofVectorSpace
.
Equations
- Basis.ofVectorSpaceIndex K V = LinearIndependent.extend (_ : LinearIndependent K fun x => ↑x) (_ : ∅ ⊆ Set.univ)
Instances For
Each vector space has a basis.
Equations
- Basis.ofVectorSpace K V = Basis.extend (_ : LinearIndependent K fun x => ↑x)
Instances For
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.
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
.