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 : 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
    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 : LinearIndepOn K id s) (x : (hs.extend )) :
      (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 : LinearIndepOn K id s) :
      theorem 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 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 (ι (sumExtendIndex hs)) K V

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

          Equations
            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 : LinearIndepOn K id s) :
              s hs.extend
              noncomputable def 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
                Instances For
                  theorem 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 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 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 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 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 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
                    Instances For
                      theorem 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 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) :
                      theorem 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 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 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] :
                          Basis (↑(ofVectorSpaceIndex K V)) 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] :
                              Free K V

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

                              theorem 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 Basis.coe_ofVectorSpace (K : Type u_3) (V : Type u_4) [DivisionRing K] [AddCommGroup V] [Module K V] :
                              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.

                              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
                              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 : vp) (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 : vp) (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 : vp) :
                              ∃ (f : V →ₗ[K] K), f v 0 p LinearMap.ker f
                              @[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 : vp) :
                              ∃ (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)