# 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 #

• 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.

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 : ι') :
Basis.toMatrix e 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.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) :
= ↑() (↑() v)
theorem Basis.coePiBasisFun.toMatrix_eq_transpose {ι : Type u_1} {R : Type u_5} [] [] :
= 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) [] :
= 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) :
Basis.toMatrix e () = Matrix.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₂ˣ) :
Basis.toMatrix e ↑() = 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)) :
Basis.toMatrix e ↑() =

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 : ι') [] :
(Finset.sum Finset.univ fun i => Basis.toMatrix e v i j e i) = v j
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) (Matrix.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) :
↑() () = 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.

Instances For
@[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 κ'] [] :
Basis.toMatrix c c' * ↑() f = ↑() f
@[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 ι'] [Fintype κ'] [] [] [] :
↑() f * Basis.toMatrix b' 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 κ'] [] [] [] :
Basis.toMatrix c c' * ↑() f * Basis.toMatrix b' b = ↑() 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) :
Basis.toMatrix b₁ b₂ * A = ↑() (↑(Matrix.toLin b₃ b₂) A)
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 * Basis.toMatrix b₁ 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) :
Basis.toMatrix b ↑() * A = Matrix.of fun i j => ↑(b.repr ()) 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) [Fintype ι'] [] [] :
↑() LinearMap.id = Basis.toMatrix b' b

A generalization of LinearMap.toMatrix_id.

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 : ι ι') :
Basis.toMatrix () v = ↑() (Basis.toMatrix b (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) :

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 ι'] :
Basis.toMatrix b b' * Basis.toMatrix b' 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₂) :

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

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 : ι ι') :
Basis.toMatrix () v = Matrix.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) :