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 Module.Basis.extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndepOn K id s) : Basis (↑(hs.extend ⋯)) K V

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

Equations

• Module.Basis.extend hs = Module.Basis.mk ⋯ ⋯

theorem Module.Basis.extend_apply_self {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndepOn K id s) (x : ↑(hs.extend ⋯)) : (extend hs) x = ↑x

@[simp]

theorem Module.Basis.coe_extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndepOn K id s) : ⇑(extend hs) = Subtype.val

theorem Module.Basis.range_extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndepOn K id s) : Set.range ⇑(extend hs) = hs.extend ⋯

def Module.Basis.sumExtendIndex {ι : Type u_1} {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {v : ι → V} (hs : LinearIndependent K v) : 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.

Equations

• Module.Basis.sumExtendIndex hs = ⋯.extend ⋯ \ Set.range v

noncomputable def Module.Basis.sumExtend {ι : Type u_1} {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {v : ι → V} (hs : LinearIndependent K v) : Basis (ι ⊕ ↑(sumExtendIndex hs)) K V

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

Equations

• Module.Basis.sumExtend hs = (Module.Basis.extend ⋯).reindex (Trans.trans ((Equiv.ofInjective v ⋯).sumCongr (Equiv.refl ↑(⋯.extend ⋯ \ Set.range v))) (Equiv.Set.sumDiffSubset ⋯)).symm

theorem Module.Basis.subset_extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndepOn K id s) : s ⊆ hs.extend ⋯

noncomputable def Module.Basis.extendLe {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) : Basis (↑(hs.extend hst)) K V

If s is a family of linearly independent vectors contained in a set t spanning V, then one can get a basis of V containing s and contained in t.

Equations

• Module.Basis.extendLe hs hst ht = Module.Basis.mk ⋯ ⋯

theorem Module.Basis.extendLe_apply_self {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) (x : ↑(hs.extend hst)) : (extendLe hs hst ht) x = ↑x

@[simp]

theorem Module.Basis.coe_extendLe {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) : ⇑(extendLe hs hst ht) = Subtype.val

theorem Module.Basis.range_extendLe {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) : Set.range ⇑(extendLe hs hst ht) = hs.extend hst

theorem Module.Basis.subset_extendLe {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) : s ⊆ Set.range ⇑(extendLe hs hst ht)

theorem Module.Basis.extendLe_subset {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) (ht : ⊤ ≤ Submodule.span K t) : Set.range ⇑(extendLe hs hst ht) ⊆ t

noncomputable def Module.Basis.ofSpan {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : ⊤ ≤ Submodule.span K s) : Basis (↑(⋯.extend ⋯)) K V

If a set s spans the space, this is a basis contained in s.

Equations

• Module.Basis.ofSpan hs = Module.Basis.extendLe ⋯ ⋯ hs

theorem Module.Basis.ofSpan_apply_self {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : ⊤ ≤ Submodule.span K s) (x : ↑(⋯.extend ⋯)) : (ofSpan hs) x = ↑x

@[simp]

theorem Module.Basis.coe_ofSpan {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : ⊤ ≤ Submodule.span K s) : ⇑(ofSpan hs) = Subtype.val

theorem Module.Basis.range_ofSpan {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : ⊤ ≤ Submodule.span K s) : Set.range ⇑(ofSpan hs) = ⋯.extend ⋯

theorem Module.Basis.ofSpan_subset {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : ⊤ ≤ Submodule.span K s) : Set.range ⇑(ofSpan hs) ⊆ s

noncomputable def Module.Basis.ofVectorSpaceIndex (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : Set V

A set used to index Basis.ofVectorSpace.

Equations

• Module.Basis.ofVectorSpaceIndex K V = ⋯.extend ⋯

noncomputable def Module.Basis.ofVectorSpace (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : Basis (↑(ofVectorSpaceIndex K V)) K V

Each vector space has a basis.

Equations

• Module.Basis.ofVectorSpace K V = Module.Basis.extend ⋯

@[instance 100]

instance Module.Free.of_divisionRing (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : Free K V

Stacks Tag 09FN (Generalized from fields to division rings.)

theorem Module.Basis.ofVectorSpace_apply_self (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] (x : ↑(ofVectorSpaceIndex K V)) : (ofVectorSpace K V) x = ↑x

@[simp]

theorem Module.Basis.coe_ofVectorSpace (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : ⇑(ofVectorSpace K V) = Subtype.val

theorem Module.Basis.ofVectorSpaceIndex.linearIndependent (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : LinearIndependent K Subtype.val

theorem Module.Basis.range_ofVectorSpace (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : Set.range ⇑(ofVectorSpace K V) = ofVectorSpaceIndex K V

theorem Module.Basis.exists_basis (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] : ∃ (s : Set V), Nonempty (Basis (↑s) K V)

theorem VectorSpace.card_fintype (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] [Fintype K] [Fintype V] : ∃ (n : ℕ), Fintype.card V = Fintype.card K ^ n

theorem nonzero_span_atom {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) : IsAtom (Submodule.span K {v})

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} [DivisionRing K] [AddCommGroup V] [Module K V] (W : Submodule K V) : IsAtom W ↔ ∃ (v : V), v ≠ 0 ∧ 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.

instance instIsAtomisticSubmodule {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] : IsAtomistic (Submodule K V)

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} [DivisionRing K] [AddCommGroup V] [AddCommGroup V'] [Module K V] [Module K V'] (f : V →ₗ[K] V') (hf_inj : ker f = ⊥) : ∃ (g : V' →ₗ[K] V), g ∘ₗ f = id

theorem Submodule.exists_isCompl {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] (p : Submodule K V) : ∃ (q : Submodule K V), IsCompl p q

instance Submodule.complementedLattice {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] : ComplementedLattice (Submodule K V)

theorem LinearMap.exists_extend {K : Type u_3} {V : Type u_4} {V' : Type u_5} [DivisionRing K] [AddCommGroup V] [AddCommGroup V'] [Module K V] [Module K V'] {p : Submodule K V} (f : ↥p →ₗ[K] V') : ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f

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

theorem LinearMap.exists_extend_of_notMem {K : Type u_3} {V : Type u_4} {V' : Type u_5} [DivisionRing K] [AddCommGroup V] [AddCommGroup V'] [Module K V] [Module K V'] {p : Submodule K V} {v : V} (f : ↥p →ₗ[K] V') (hv : v ∉ p) (y : V') : ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ g v = y

@[deprecated LinearMap.exists_extend_of_notMem (since := "2025-05-23")]

theorem LinearMap.exists_extend_of_not_mem {K : Type u_3} {V : Type u_4} {V' : Type u_5} [DivisionRing K] [AddCommGroup V] [AddCommGroup V'] [Module K V] [Module K V'] {p : Submodule K V} {v : V} (f : ↥p →ₗ[K] V') (hv : v ∉ p) (y : V') : ∃ (g : V →ₗ[K] V'), g ∘ₗ p.subtype = f ∧ g v = y

Alias of LinearMap.exists_extend_of_notMem.

theorem Submodule.exists_le_ker_of_notMem {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} {v : V} (hv : v ∉ p) : ∃ (f : V →ₗ[K] K), f v ≠ 0 ∧ p ≤ LinearMap.ker f

instance instNontrivialLinearMapId {K : Type u_3} {V : Type u_4} {V' : Type u_5} [DivisionRing K] [AddCommGroup V] [AddCommGroup V'] [Module K V] [Module K V'] [Nontrivial V] [Nontrivial V'] : Nontrivial (V →ₗ[K] V')

If V and V' are nontrivial vector spaces over a field K, the space of K-linear maps between them is nontrivial.

@[deprecated Submodule.exists_le_ker_of_notMem (since := "2025-05-23")]

theorem Submodule.exists_le_ker_of_not_mem {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {p : Submodule K V} {v : V} (hv : v ∉ p) : ∃ (f : V →ₗ[K] K), f v ≠ 0 ∧ p ≤ LinearMap.ker f

Alias of Submodule.exists_le_ker_of_notMem.

theorem Submodule.exists_le_ker_of_lt_top {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] (p : Submodule K V) (hp : p < ⊤) : ∃ (f : V →ₗ[K] K), f ≠ 0 ∧ p ≤ LinearMap.ker f

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} [DivisionRing K] [AddCommGroup V] [Module K V] (p : Submodule K V) : Nonempty (((V ⧸ p) × ↥p) ≃ₗ[K] V)