Documentation

Mathlib.LinearAlgebra.Matrix.Basis

Bases and matrices #

This file defines the map Basis.toMatrix that sends a family of vectors to the matrix of their coordinates with respect to some basis.

Main definitions #

Main results #

Tags #

matrix, basis

def Basis.toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) :
Matrix ι ι' R

From a basis e : ι → M and a family of vectors v : ι' → M, make the matrix whose columns are the vectors v i written in the basis e.

Equations
  • e.toMatrix v i j = (e.repr (v j)) i
Instances For
    theorem Basis.toMatrix_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (i : ι) (j : ι') :
    e.toMatrix v i j = (e.repr (v j)) i
    theorem Basis.toMatrix_transpose_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') :
    (e.toMatrix v).transpose j = (e.repr (v j))
    theorem Basis.toMatrix_eq_toMatrix_constr {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) [Fintype ι] [DecidableEq ι] (v : ιM) :
    e.toMatrix v = (LinearMap.toMatrix e e) ((e.constr ) v)
    theorem Basis.coePiBasisFun.toMatrix_eq_transpose {ι : Type u_1} {R : Type u_5} [CommSemiring R] [Finite ι] :
    (Pi.basisFun R ι).toMatrix = Matrix.transpose
    @[simp]
    theorem Basis.toMatrix_self {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) [DecidableEq ι] :
    e.toMatrix e = 1
    theorem Basis.toMatrix_update {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') [DecidableEq ι'] (x : M) :
    e.toMatrix (Function.update v j x) = (e.toMatrix v).updateColumn j (e.repr x)
    @[simp]
    theorem Basis.toMatrix_unitsSMul {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] (e : Basis ι R₂ M₂) (w : ιR₂ˣ) :
    e.toMatrix (e.unitsSMul w) = Matrix.diagonal (Units.val w)

    The basis constructed by unitsSMul has vectors given by a diagonal matrix.

    @[simp]
    theorem Basis.toMatrix_isUnitSMul {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] (e : Basis ι R₂ M₂) {w : ιR₂} (hw : ∀ (i : ι), IsUnit (w i)) :
    e.toMatrix (e.isUnitSMul hw) = Matrix.diagonal w

    The basis constructed by isUnitSMul has vectors given by a diagonal matrix.

    @[simp]
    theorem Basis.sum_toMatrix_smul_self {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') [Fintype ι] :
    i : ι, e.toMatrix v i j e i = v j
    theorem Basis.toMatrix_smul {ι : Type u_1} {R₁ : Type u_9} {S : Type u_10} [CommRing R₁] [Ring S] [Algebra R₁ S] [Fintype ι] [DecidableEq ι] (x : S) (b : Basis ι R₁ S) (w : ιS) :
    b.toMatrix (x w) = (Algebra.leftMulMatrix b) x * b.toMatrix w
    theorem Basis.toMatrix_map_vecMul {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} [CommSemiring R] {S : Type u_9} [Ring S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (v : ι'S) :
    Matrix.vecMul (b) ((b.toMatrix v).map (algebraMap R S)) = v
    @[simp]
    theorem Basis.toLin_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (e : Basis ι R M) [Finite ι] [Fintype ι'] [DecidableEq ι'] (v : Basis ι' R M) :
    (Matrix.toLin v e) (e.toMatrix v) = LinearMap.id
    def Basis.toMatrixEquiv {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι] (e : Basis ι R M) :
    (ιM) ≃ₗ[R] Matrix ι ι R

    From a basis e : ι → M, build a linear equivalence between families of vectors v : ι → M, and matrices, making the matrix whose columns are the vectors v i written in the basis e.

    Equations
    • e.toMatrixEquiv = { toFun := e.toMatrix, map_add' := , map_smul' := , invFun := fun (m : Matrix ι ι R) (j : ι) => i : ι, m i j e i, left_inv := , right_inv := }
    Instances For
      theorem Basis.restrictScalars_toMatrix {ι : Type u_1} (R₂ : Type u_7) {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [Fintype ι] [DecidableEq ι] {S : Type u_9} [CommRing S] [Nontrivial S] [Algebra R₂ S] [Module S M₂] [IsScalarTower R₂ S M₂] [NoZeroSMulDivisors R₂ S] (b : Basis ι S M₂) (v : ι(Submodule.span R₂ (Set.range b))) :
      (algebraMap R₂ S).mapMatrix ((Basis.restrictScalars R₂ b).toMatrix v) = b.toMatrix fun (i : ι) => (v i)
      @[simp]
      theorem LinearMap.toMatrix_id_eq_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [Fintype ι] [DecidableEq ι] [Finite ι'] :
      (LinearMap.toMatrix b b') LinearMap.id = b'.toMatrix b

      A generalization of LinearMap.toMatrix_id.

      @[simp]
      theorem basis_toMatrix_mul_linearMap_toMatrix {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Finite κ] [Fintype κ'] [DecidableEq ι'] :
      c.toMatrix c' * (LinearMap.toMatrix b' c') f = (LinearMap.toMatrix b' c) f
      theorem basis_toMatrix_mul {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] [Fintype ι'] [Fintype κ] [Finite ι] [DecidableEq κ] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix ι' κ R) :
      b₁.toMatrix b₂ * A = (LinearMap.toMatrix b₃ b₁) ((Matrix.toLin b₃ b₂) A)
      @[simp]
      theorem linearMap_toMatrix_mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Fintype ι] [Finite κ'] [DecidableEq ι] [DecidableEq ι'] :
      (LinearMap.toMatrix b' c') f * b'.toMatrix b = (LinearMap.toMatrix b c') f
      theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [Finite κ] [Fintype ι] [Fintype κ'] [DecidableEq ι] [DecidableEq ι'] :
      c.toMatrix c' * (LinearMap.toMatrix b' c') f * b'.toMatrix b = (LinearMap.toMatrix b c) f
      theorem mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] [Fintype ι'] [Finite κ] [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix κ ι R) :
      A * b₁.toMatrix b₂ = (LinearMap.toMatrix b₂ b₃) ((Matrix.toLin b₁ b₃) A)
      theorem basis_toMatrix_basisFun_mul {ι : Type u_1} {R : Type u_5} [CommSemiring R] [Fintype ι] (b : Basis ι R (ιR)) (A : Matrix ι ι R) :
      b.toMatrix (Pi.basisFun R ι) * A = Matrix.of fun (i j : ι) => (b.repr (A.transpose j)) i
      theorem Basis.toMatrix_reindex' {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] [Fintype ι'] [Fintype ι] [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι'M) (e : ι ι') :
      (b.reindex e).toMatrix v = (Matrix.reindexAlgEquiv R e) (b.toMatrix (v e))

      See also Basis.toMatrix_reindex which gives the simp normal form of this result.

      @[simp]
      theorem Basis.toMatrix_mul_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) {ι'' : Type u_10} [Fintype ι'] (b'' : ι''M) :
      b.toMatrix b' * b'.toMatrix b'' = b.toMatrix b''

      A generalization of Basis.toMatrix_self, in the opposite direction.

      theorem Basis.toMatrix_mul_toMatrix_flip {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [DecidableEq ι] [Fintype ι'] :
      b.toMatrix b' * b'.toMatrix b = 1

      b.toMatrix b' and b'.toMatrix b are inverses.

      def Basis.invertibleToMatrix {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] [Fintype ι] (b : Basis ι R₂ M₂) (b' : Basis ι R₂ M₂) :
      Invertible (b.toMatrix b')

      A matrix whose columns form a basis b', expressed w.r.t. a basis b, is invertible.

      Equations
      • b.invertibleToMatrix b' = { invOf := b'.toMatrix b, invOf_mul_self := , mul_invOf_self := }
      Instances For
        @[simp]
        theorem Basis.toMatrix_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] (b : Basis ι R M) (v : ι'M) (e : ι ι') :
        (b.reindex e).toMatrix v = (b.toMatrix v).submatrix (e.symm) id
        @[simp]
        theorem Basis.toMatrix_map {ι : Type u_1} {R : Type u_5} {M : Type u_6} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ιN) :
        (b.map f).toMatrix v = b.toMatrix (f.symm v)