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

theorem Module.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 Module.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 Module.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 Module.Basis.coePiBasisFun.toMatrix_eq_transpose {ι : Type u_1} {R : Type u_5} [CommSemiring R] [Finite ι] : (Pi.basisFun R ι).toMatrix = Matrix.transpose

@[simp]

theorem Module.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 Module.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).updateCol j ⇑(e.repr x)

@[simp]

theorem Module.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 Module.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.

theorem Module.Basis.toMatrix_smul_left {ι : 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) {G : Type u_9} [Group G] [DistribMulAction G M] [SMulCommClass G R M] (g : G) : (g • e).toMatrix v = e.toMatrix (g⁻¹ • v)

@[simp]

theorem Module.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 Module.Basis.toMatrix_smul {ι : Type u_1} {R₁ : Type u_9} {S : Type u_10} [CommSemiring R₁] [Semiring 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 Module.Basis.toMatrix_map_vecMul {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} [CommSemiring R] {S : Type u_9} [Semiring S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (v : ι' → S) : Matrix.vecMul (⇑b) ((b.toMatrix v).map ⇑(algebraMap R S)) = v

@[simp]

theorem Module.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 Module.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.

theorem Module.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 ((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 : Module.Basis ι R M) (b' : Module.Basis ι' R M) [Fintype ι] [DecidableEq ι] [Finite ι'] : (toMatrix b b') 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' : Module.Basis ι' R M) (c : Module.Basis κ R N) (c' : Module.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₁ : Module.Basis ι R M) (b₂ : Module.Basis ι' R M) (b₃ : Module.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 : Module.Basis ι R M) (b' : Module.Basis ι' R M) (c' : Module.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 : Module.Basis ι R M) (b' : Module.Basis ι' R M) (c : Module.Basis κ R N) (c' : Module.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₁ : Module.Basis ι R M) (b₂ : Module.Basis ι' R M) (b₃ : Module.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 : Module.Basis ι R (ι → R)) (A : Matrix ι ι R) : b.toMatrix ⇑(Pi.basisFun R ι) * A = Matrix.of fun (i j : ι) => (b.repr (A.col j)) i

theorem Module.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 R e) (b.toMatrix (v ∘ ⇑e))

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

@[simp]

theorem Module.Basis.toMatrix_mulVec_repr {ι : 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 ι] [Finite ι'] (m : M) : (b'.toMatrix ⇑b).mulVec ⇑(b.repr m) = ⇑(b'.repr m)

@[simp]

theorem Module.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 Module.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 Module.Basis.invertibleToMatrix {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [CommRing R₂] [AddCommGroup M₂] [Module R₂ M₂] [DecidableEq ι] [Fintype ι] (b 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.

@[simp]

theorem Module.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 Module.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)