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 #

• Basis.toMatrix e v is the matrix whose i, jth entry is e.repr (v j) i
• basis.toMatrixEquiv is Basis.toMatrix bundled as a linear equiv

Main results #

• LinearMap.toMatrix_id_eq_basis_toMatrix: LinearMap.toMatrix b c id is equal to Basis.toMatrix b c
• Basis.toMatrix_mul_toMatrix: multiplying Basis.toMatrix with another Basis.toMatrix gives a Basis.toMatrix

Tags #

matrix, basis

def Basis.toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [] [] [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} [] [] [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} [] [] [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} [] [] [Module R M] (e : Basis ι R M) [] [] (v : ιM) :
e.toMatrix v = () ((e.constr ) v)
theorem Basis.coePiBasisFun.toMatrix_eq_transpose {ι : Type u_1} {R : Type u_5} [] [] :
().toMatrix = Matrix.transpose
@[simp]
theorem Basis.toMatrix_self {ι : Type u_1} {R : Type u_5} {M : Type u_6} [] [] [Module R M] (e : Basis ι R M) [] :
e.toMatrix e = 1
theorem Basis.toMatrix_update {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [] [] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') [] (x : M) :
e.toMatrix () = (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₂] [] [Module R₂ M₂] [] (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₂] [] [Module R₂ M₂] [] (e : Basis ι R₂ M₂) {w : ιR₂} (hw : ∀ (i : ι), IsUnit (w i)) :
e.toMatrix (e.isUnitSMul hw) =

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} [] [] [Module R M] (e : Basis ι R M) (v : ι'M) (j : ι') [] :
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] [] [] (x : S) (b : Basis ι R₁ S) (w : ιS) :
b.toMatrix (x w) = * b.toMatrix w
theorem Basis.toMatrix_map_vecMul {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} [] {S : Type u_9} [Ring S] [Algebra R S] [] (b : Basis ι R S) (v : ι'S) :
Matrix.vecMul (b) ((b.toMatrix v).map ()) = v
@[simp]
theorem Basis.toLin_toMatrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [] [] [Module R M] (e : Basis ι R M) [] [Fintype ι'] [] (v : Basis ι' R M) :
() (e.toMatrix v) = LinearMap.id
def Basis.toMatrixEquiv {ι : Type u_1} {R : Type u_5} {M : Type u_6} [] [] [Module R M] [] (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₂] [] [Module R₂ M₂] [] [] {S : Type u_9} [] [] [Algebra R₂ S] [Module S M₂] [IsScalarTower R₂ S M₂] [] (b : Basis ι S M₂) (v : ι(Submodule.span R₂ ())) :
(algebraMap R₂ S).mapMatrix (().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} [] [] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [] [] [Finite ι'] :
() 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} [] [] [Module R M] {N : Type u_9} [] [Module R N] (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [] [Fintype κ'] [] :
c.toMatrix c' * () f = () f
theorem basis_toMatrix_mul {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [] [] [Module R M] {N : Type u_9} [] [Module R N] [Fintype ι'] [] [] [] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix ι' κ R) :
b₁.toMatrix b₂ * A = () ((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} [] [] [Module R M] {N : Type u_9} [] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [] [Finite κ'] [] [] :
() f * b'.toMatrix b = () 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} [] [] [Module R M] {N : Type u_9} [] [Module R N] (b : Basis ι R M) (b' : Basis ι' R M) (c : Basis κ R N) (c' : Basis κ' R N) (f : M →ₗ[R] N) [Fintype ι'] [] [] [Fintype κ'] [] [] :
c.toMatrix c' * () f * b'.toMatrix b = () f
theorem mul_basis_toMatrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [] [] [Module R M] {N : Type u_9} [] [Module R N] [Fintype ι'] [] [] [] [] (b₁ : Basis ι R M) (b₂ : Basis ι' R M) (b₃ : Basis κ R N) (A : Matrix κ ι R) :
A * b₁.toMatrix b₂ = () ((Matrix.toLin b₁ b₃) A)
theorem basis_toMatrix_basisFun_mul {ι : Type u_1} {R : Type u_5} [] [] (b : Basis ι R (ιR)) (A : Matrix ι ι R) :
b.toMatrix () * 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} [] [] [Module R M] [Fintype ι'] [] [] [] (b : Basis ι R M) (v : ι'M) (e : ι ι') :
(b.reindex e).toMatrix v = () (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} [] [] [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} [] [] [Module R M] (b : Basis ι R M) (b' : Basis ι' R M) [] [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₂] [] [Module R₂ M₂] [] [] (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} [] [] [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} [] [] [Module R M] {N : Type u_9} [] [Module R N] (b : Basis ι R M) (f : M ≃ₗ[R] N) (v : ιN) :
(b.map f).toMatrix v = b.toMatrix (f.symm v)