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 #

Tags #

basis, bases

noncomputable def Basis.extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndependent (ι := { x : V // x s }) K Subtype.val) :
Basis ((hs.extend )) K V

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

Equations
Instances For
    theorem Basis.extend_apply_self {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndependent (ι := { x : V // x s }) K Subtype.val) (x : (hs.extend )) :
    (Basis.extend hs) x = x
    @[simp]
    theorem Basis.coe_extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndependent (ι := { x : V // x s }) K Subtype.val) :
    (Basis.extend hs) = Subtype.val
    theorem Basis.range_extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndependent (ι := { x : V // x s }) K Subtype.val) :
    Set.range (Basis.extend hs) = hs.extend
    def 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
    Instances For
      noncomputable def 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 (ι (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
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Basis.subset_extend {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Set V} (hs : LinearIndependent (ι := { x : V // x s }) K Subtype.val) :
        s hs.extend
        noncomputable def 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
        Instances For
          noncomputable def Basis.ofVectorSpace (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :

          Each vector space has a basis.

          Equations
          Instances For
            @[instance 100]
            instance Module.Free.of_divisionRing (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :
            Equations
            • =
            theorem Basis.ofVectorSpace_apply_self (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] (x : (Basis.ofVectorSpaceIndex K V)) :
            (Basis.ofVectorSpace K V) x = x
            @[simp]
            theorem Basis.coe_ofVectorSpace (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :
            (Basis.ofVectorSpace K V) = Subtype.val
            theorem Basis.ofVectorSpaceIndex.linearIndependent (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :
            LinearIndependent (ι := { x : V // x Basis.ofVectorSpaceIndex K V }) K Subtype.val
            theorem 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) :

            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] :

            The lattice of submodules of a module over a division ring is atomistic.

            Equations
            • =
            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 : LinearMap.ker f = ) :
            ∃ (g : V' →ₗ[K] V), g ∘ₗ f = LinearMap.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
            Equations
            • =
            theorem LinearMap.exists_rightInverse_of_surjective {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_surj : LinearMap.range f = ) :
            ∃ (g : V' →ₗ[K] V), f ∘ₗ g = LinearMap.id
            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 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)