# Documentation

Mathlib.LinearAlgebra.Basis.VectorSpace

# 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

noncomputable def Basis.extend {K : Type u_3} {V : Type u_4} [] [] [Module K V] {s : Set V} (hs : LinearIndependent K Subtype.val) :
Basis (↑(LinearIndependent.extend hs (_ : s Set.univ))) K V

If s is a linear independent set of vectors, we can extend it to a basis.

Instances For
theorem Basis.extend_apply_self {K : Type u_3} {V : Type u_4} [] [] [Module K V] {s : Set V} (hs : LinearIndependent K Subtype.val) (x : ↑(LinearIndependent.extend hs (_ : s Set.univ))) :
↑() x = x
@[simp]
theorem Basis.coe_extend {K : Type u_3} {V : Type u_4} [] [] [Module K V] {s : Set V} (hs : LinearIndependent K Subtype.val) :
↑() = Subtype.val
theorem Basis.range_extend {K : Type u_3} {V : Type u_4} [] [] [Module K V] {s : Set V} (hs : LinearIndependent K Subtype.val) :
Set.range ↑() = LinearIndependent.extend hs (_ : s Set.univ)
def Basis.sumExtendIndex {ι : Type u_1} {K : Type u_3} {V : Type u_4} [] [] [Module K V] {v : ιV} (hs : ) :
Set V

Auxiliary definition: the index for the new basis vectors in Basis.sumExtend.

The specific value of this definition should be considered an implementation detail.

Instances For
noncomputable def Basis.sumExtend {ι : Type u_1} {K : Type u_3} {V : Type u_4} [] [] [Module K V] {v : ιV} (hs : ) :
Basis (ι ↑()) K V

If v is a linear independent family of vectors, extend it to a basis indexed by a sum type.

Instances For
theorem Basis.subset_extend {K : Type u_3} {V : Type u_4} [] [] [Module K V] {s : Set V} (hs : LinearIndependent K Subtype.val) :
s LinearIndependent.extend hs (_ : s Set.univ)
noncomputable def Basis.ofVectorSpaceIndex (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
Set V

A set used to index Basis.ofVectorSpace.

Instances For
noncomputable def Basis.ofVectorSpace (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
Basis (↑()) K V

Each vector space has a basis.

Instances For
instance Module.Free.of_divisionRing (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
theorem Basis.ofVectorSpace_apply_self (K : Type u_3) (V : Type u_4) [] [] [Module K V] (x : ↑()) :
↑() x = x
@[simp]
theorem Basis.coe_ofVectorSpace (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
↑() = Subtype.val
theorem Basis.ofVectorSpaceIndex.linearIndependent (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
LinearIndependent K Subtype.val
theorem Basis.range_ofVectorSpace (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
theorem Basis.exists_basis (K : Type u_3) (V : Type u_4) [] [] [Module K V] :
s, Nonempty (Basis (s) K V)
theorem VectorSpace.card_fintype (K : Type u_3) (V : Type u_4) [] [] [Module K V] [] [] :
n, =
theorem nonzero_span_atom {K : Type u_3} {V : Type u_4} [] [] [Module K V] (v : V) (hv : v 0) :

For a module over a division ring, the span of a nonzero element is an atom of the lattice of submodules.

theorem atom_iff_nonzero_span {K : Type u_3} {V : Type u_4} [] [] [Module K V] (W : ) :
v x, W = Submodule.span K {v}

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.

theorem LinearMap.exists_leftInverse_of_injective {K : Type u_3} {V : Type u_4} {V' : Type u_5} [] [] [] [Module K V] [Module K V'] (f : V →ₗ[K] V') (hf_inj : ) :
g, = LinearMap.id
theorem Submodule.exists_isCompl {K : Type u_3} {V : Type u_4} [] [] [Module K V] (p : ) :
q, IsCompl p q
instance Module.Submodule.complementedLattice {K : Type u_3} {V : Type u_4} [] [] [Module K V] :
theorem LinearMap.exists_rightInverse_of_surjective {K : Type u_3} {V : Type u_4} {V' : Type u_5} [] [] [] [Module K V] [Module K V'] (f : V →ₗ[K] V') (hf_surj : ) :
g, = LinearMap.id
theorem LinearMap.exists_extend {K : Type u_3} {V : Type u_4} {V' : Type u_5} [] [] [] [Module K V] [Module K V'] {p : } (f : { x // x p } →ₗ[K] V') :
g, = f

Any linear map f : p →ₗ[K] V' defined on a subspace p can be extended to the whole space.

theorem Submodule.exists_le_ker_of_lt_top {K : Type u_3} {V : Type u_4} [] [] [Module K V] (p : ) (hp : p < ) :
f, f 0

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.

theorem quotient_prod_linearEquiv {K : Type u_3} {V : Type u_4} [] [] [Module K V] (p : ) :
Nonempty (((V p) × { x // x p }) ≃ₗ[K] V)