Documentation

Mathlib.LinearAlgebra.Basis.Basic

Bases #

Further results on bases in modules and vector spaces.

theorem Basis.coe_sumCoords_eq_finsum {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
b.sumCoords = fun (m : M) => ∑ᶠ (i : ι), (b.coord i) m
theorem Basis.linearIndependent {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) :
theorem Basis.ne_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) [Nontrivial R] (i : ι) :
b i 0
def Basis.prod {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') :
Basis (ι ι') R (M × M')

Basis.prod maps an ι-indexed basis for M and an ι'-indexed basis for M' to an ι ⊕ ι'-index basis for M × M'. For the specific case of R × R, see also Basis.finTwoProd.

Equations
Instances For
    @[simp]
    theorem Basis.prod_repr_inl {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (x : M × M') (i : ι) :
    ((b.prod b').repr x) (Sum.inl i) = (b.repr x.1) i
    @[simp]
    theorem Basis.prod_repr_inr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (x : M × M') (i : ι') :
    ((b.prod b').repr x) (Sum.inr i) = (b'.repr x.2) i
    theorem Basis.prod_apply_inl_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι) :
    ((b.prod b') (Sum.inl i)).1 = b i
    theorem Basis.prod_apply_inr_fst {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι') :
    ((b.prod b') (Sum.inr i)).1 = 0
    theorem Basis.prod_apply_inl_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι) :
    ((b.prod b') (Sum.inl i)).2 = 0
    theorem Basis.prod_apply_inr_snd {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι') :
    ((b.prod b') (Sum.inr i)).2 = b' i
    @[simp]
    theorem Basis.prod_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (b : Basis ι R M) (b' : Basis ι' R M') (i : ι ι') :
    (b.prod b') i = Sum.elim ((LinearMap.inl R M M') b) ((LinearMap.inr R M M') b') i
    theorem Basis.noZeroSMulDivisors {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) :
    theorem Basis.smul_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) {c : R} {x : M} :
    c x = 0 c = 0 x = 0
    theorem Basis.eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) (N : Submodule R M) (rank_eq : ∀ {m : } (v : Fin mN), LinearIndependent R (Subtype.val v)m = 0) :
    N =
    theorem Basis.basis_singleton_iff {R : Type u_10} {M : Type u_11} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (ι : Type u_12) [Unique ι] :
    Nonempty (Basis ι R M) ∃ (x : M), x 0 ∀ (y : M), ∃ (r : R), r x = y
    theorem Basis.maximal {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] (b : Basis ι R M) :
    .Maximal

    Any basis is a maximal linear independent set.

    noncomputable def Basis.mk {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent R v) (hsp : Submodule.span R (Set.range v)) :
    Basis ι R M

    A linear independent family of vectors spanning the whole module is a basis.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Basis.mk_repr {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] {x : M} (hli : LinearIndependent R v) (hsp : Submodule.span R (Set.range v)) :
      (Basis.mk hli hsp).repr x = hli.repr x,
      theorem Basis.mk_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent R v) (hsp : Submodule.span R (Set.range v)) (i : ι) :
      (Basis.mk hli hsp) i = v i
      @[simp]
      theorem Basis.coe_mk {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent R v) (hsp : Submodule.span R (Set.range v)) :
      (Basis.mk hli hsp) = v
      theorem Basis.mk_coord_apply_eq {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] {hli : LinearIndependent R v} {hsp : Submodule.span R (Set.range v)} (i : ι) :
      ((Basis.mk hli hsp).coord i) (v i) = 1

      Given a basis, the ith element of the dual basis evaluates to 1 on the ith element of the basis.

      theorem Basis.mk_coord_apply_ne {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] {hli : LinearIndependent R v} {hsp : Submodule.span R (Set.range v)} {i : ι} {j : ι} (h : j i) :
      ((Basis.mk hli hsp).coord i) (v j) = 0

      Given a basis, the ith element of the dual basis evaluates to 0 on the jth element of the basis if j ≠ i.

      theorem Basis.mk_coord_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] {hli : LinearIndependent R v} {hsp : Submodule.span R (Set.range v)} [DecidableEq ι] {i : ι} {j : ι} :
      ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0

      Given a basis, the ith element of the dual basis evaluates to the Kronecker delta on the jth element of the basis.

      noncomputable def Basis.span {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent R v) :

      A linear independent family of vectors is a basis for their span.

      Equations
      Instances For
        theorem Basis.span_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ιM} [Ring R] [AddCommGroup M] [Module R M] (hli : LinearIndependent R v) (i : ι) :
        ((Basis.span hli) i) = v i
        theorem Basis.groupSMul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] {v : ιM} (hv : Submodule.span R (Set.range v) = ) {w : ιG} :
        def Basis.groupSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] (v : Basis ι R M) (w : ιG) :
        Basis ι R M

        Given a basis v and a map w such that for all i, w i are elements of a group, groupSMul provides the basis corresponding to w • v.

        Equations
        Instances For
          theorem Basis.groupSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {G : Type u_10} [Group G] [DistribMulAction G R] [DistribMulAction G M] [IsScalarTower G R M] [SMulCommClass G R M] {v : Basis ι R M} {w : ιG} (i : ι) :
          (v.groupSMul w) i = (w v) i
          theorem Basis.units_smul_span_eq_top {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {v : ιM} (hv : Submodule.span R (Set.range v) = ) {w : ιRˣ} :
          def Basis.unitsSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] (v : Basis ι R M) (w : ιRˣ) :
          Basis ι R M

          Given a basis v and a map w such that for all i, w i is a unit, unitsSMul provides the basis corresponding to w • v.

          Equations
          Instances For
            theorem Basis.unitsSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {v : Basis ι R M} {w : ιRˣ} (i : ι) :
            (v.unitsSMul w) i = w i v i
            @[simp]
            theorem Basis.coord_unitsSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_6} [CommRing R₂] [AddCommGroup M] [Module R₂ M] (e : Basis ι R₂ M) (w : ιR₂ˣ) (i : ι) :
            (e.unitsSMul w).coord i = (w i)⁻¹ e.coord i
            @[simp]
            theorem Basis.repr_unitsSMul {ι : Type u_1} {R₂ : Type u_4} {M : Type u_6} [CommRing R₂] [AddCommGroup M] [Module R₂ M] (e : Basis ι R₂ M) (w : ιR₂ˣ) (v : M) (i : ι) :
            ((e.unitsSMul w).repr v) i = (w i)⁻¹ (e.repr v) i
            def Basis.isUnitSMul {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] (v : Basis ι R M) {w : ιR} (hw : ∀ (i : ι), IsUnit (w i)) :
            Basis ι R M

            A version of unitsSMul that uses IsUnit.

            Equations
            • v.isUnitSMul hw = v.unitsSMul fun (i : ι) => .unit
            Instances For
              theorem Basis.isUnitSMul_apply {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {v : Basis ι R M} {w : ιR} (hw : ∀ (i : ι), IsUnit (w i)) (i : ι) :
              (v.isUnitSMul hw) i = w i v i
              noncomputable def Basis.mkFinCons {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (y : M) (b : Basis (Fin n) R N) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c y N) :
              Basis (Fin (n + 1)) R M

              Let b be a basis for a submodule N of M. If y : M is linear independent of N and y and N together span the whole of M, then there is a basis for M whose basis vectors are given by Fin.cons y b.

              Equations
              Instances For
                @[simp]
                theorem Basis.coe_mkFinCons {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} (y : M) (b : Basis (Fin n) R N) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : ∀ (z : M), ∃ (c : R), z + c y N) :
                (Basis.mkFinCons y b hli hsp) = Fin.cons y (Subtype.val b)
                noncomputable def Basis.mkFinConsOfLE {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} {O : Submodule R M} (y : M) (yO : y O) (b : Basis (Fin n) R N) (hNO : N O) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : zO, ∃ (c : R), z + c y N) :
                Basis (Fin (n + 1)) R O

                Let b be a basis for a submodule N ≤ O. If y ∈ O is linear independent of N and y and N together span the whole of O, then there is a basis for O whose basis vectors are given by Fin.cons y b.

                Equations
                Instances For
                  @[simp]
                  theorem Basis.coe_mkFinConsOfLE {R : Type u_3} {M : Type u_6} [Ring R] [AddCommGroup M] [Module R M] {n : } {N : Submodule R M} {O : Submodule R M} (y : M) (yO : y O) (b : Basis (Fin n) R N) (hNO : N O) (hli : ∀ (c : R), xN, c y + x = 0c = 0) (hsp : zO, ∃ (c : R), z + c y N) :
                  (Basis.mkFinConsOfLE y yO b hNO hli hsp) = Fin.cons y, yO ((Submodule.inclusion hNO) b)
                  def Basis.finTwoProd (R : Type u_10) [Semiring R] :
                  Basis (Fin 2) R (R × R)

                  The basis of R × R given by the two vectors (1, 0) and (0, 1).

                  Equations
                  Instances For
                    @[simp]
                    theorem Basis.finTwoProd_zero (R : Type u_10) [Semiring R] :
                    (Basis.finTwoProd R) 0 = (1, 0)
                    @[simp]
                    theorem Basis.finTwoProd_one (R : Type u_10) [Semiring R] :
                    (Basis.finTwoProd R) 1 = (0, 1)
                    @[simp]
                    theorem Basis.coe_finTwoProd_repr {R : Type u_10} [Semiring R] (x : R × R) :
                    ((Basis.finTwoProd R).repr x) = ![x.1, x.2]
                    def Submodule.inductionOnRankAux {ι : Type u_1} {R : Type u_3} {M : Type u_6} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] (b : Basis ι R M) (P : Submodule R MSort u_10) (ih : (N : Submodule R M) → ((N' : Submodule R M) → N' N(x : M) → x N(∀ (c : R), yN', c x + y = 0c = 0)P N')P N) (n : ) (N : Submodule R M) (rank_le : ∀ {m : } (v : Fin mN), LinearIndependent R (Subtype.val v)m n) :
                    P N

                    If N is a submodule with finite rank, do induction on adjoining a linear independent element to a submodule.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      theorem Basis.mem_center_iff {ι : Type u_1} {R : Type u_3} {A : Type u_10} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A] (b : Basis ι R A) {z : A} :
                      z Set.center A (∀ (i : ι), Commute (b i) z) ∀ (i j : ι), z * (b i * b j) = z * b i * b j b i * z * b j = b i * (z * b j) b i * b j * z = b i * (b j * z)

                      An element of a non-unital-non-associative algebra is in the center exactly when it commutes with the basis elements.

                      noncomputable def Basis.restrictScalars {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) :
                      Basis ι R (Submodule.span R (Set.range b))

                      Let b be an S-basis of M. Let R be a CommRing such that Algebra R S has no zero smul divisors, then the submodule of M spanned by b over R admits b as an R-basis.

                      Equations
                      Instances For
                        @[simp]
                        theorem Basis.restrictScalars_apply {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (i : ι) :
                        ((Basis.restrictScalars R b) i) = b i
                        @[simp]
                        theorem Basis.restrictScalars_repr_apply {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (m : (Submodule.span R (Set.range b))) (i : ι) :
                        (algebraMap R S) (((Basis.restrictScalars R b).repr m) i) = (b.repr m) i
                        theorem Basis.mem_span_iff_repr_mem {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (m : M) :
                        m Submodule.span R (Set.range b) ∀ (i : ι), (b.repr m) i Set.range (algebraMap R S)

                        Let b be an S-basis of M. Then m : M lies in the R-module spanned by b iff all the coordinates of m on the basis b are in R (see Basis.mem_span for the case R = S).