# mathlib3documentation

linear_algebra.matrix.basis

# Bases and matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main definitions #

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

## Main results #

• linear_map.to_matrix_id_eq_basis_to_matrix: linear_map.to_matrix b c id is equal to basis.to_matrix b c
• basis.to_matrix_mul_to_matrix: multiplying basis.to_matrix with another basis.to_matrix gives a basis.to_matrix

## Tags #

matrix, basis

noncomputable def basis.to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (e : R M) (v : ι' M) :
ι' 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
theorem basis.to_matrix_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (e : R M) (v : ι' M) (i : ι) (j : ι') :
e.to_matrix v i j = ((e.repr) (v j)) i
theorem basis.to_matrix_transpose_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (e : R M) (v : ι' M) (j : ι') :
(e.to_matrix v).transpose j = ((e.repr) (v j))
theorem basis.to_matrix_eq_to_matrix_constr {ι : Type u_1} {R : Type u_5} {M : Type u_6} [ M] (e : R M) [fintype ι] [decidable_eq ι] (v : ι M) :
e.to_matrix v = e) ((e.constr ) v)
@[simp]
theorem basis.to_matrix_self {ι : Type u_1} {R : Type u_5} {M : Type u_6} [ M] (e : R M) [decidable_eq ι] :
theorem basis.to_matrix_update {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (e : R M) (v : ι' M) (j : ι') [decidable_eq ι'] (x : M) :
@[simp]
theorem basis.to_matrix_units_smul {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [comm_ring R₂] [add_comm_group M₂] [module R₂ M₂] [decidable_eq ι] (e : R₂ M₂) (w : ι R₂ˣ) :

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

@[simp]
theorem basis.to_matrix_is_unit_smul {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [comm_ring R₂] [add_comm_group M₂] [module R₂ M₂] [decidable_eq ι] (e : R₂ M₂) {w : ι R₂} (hw : (i : ι), is_unit (w i)) :

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

@[simp]
theorem basis.sum_to_matrix_smul_self {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (e : R M) (v : ι' M) (j : ι') [fintype ι] :
finset.univ.sum (λ (i : ι), e.to_matrix v i j e i) = v j
theorem basis.to_matrix_map_vec_mul {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {S : Type u_3} [ring S] [ S] [fintype ι] (b : R S) (v : ι' S) :
((b.to_matrix v).map S)) = v
@[simp]
theorem basis.to_lin_to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (e : R M) [fintype ι] [fintype ι'] [decidable_eq ι'] (v : basis ι' R M) :
noncomputable def basis.to_matrix_equiv {ι : Type u_1} {R : Type u_5} {M : Type u_6} [ M] [fintype ι] (e : R M) :
M) ≃ₗ[R] ι 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
@[simp]
theorem basis_to_matrix_mul_linear_map_to_matrix {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [ M] {N : Type u_9} [ N] (b' : basis ι' R M) (c : R N) (c' : basis κ' R N) (f : M →ₗ[R] N) [fintype ι'] [fintype κ] [fintype κ'] [decidable_eq ι'] :
(c.to_matrix c').mul ( c') f) = c) f
@[simp]
theorem linear_map_to_matrix_mul_basis_to_matrix {ι : Type u_1} {ι' : Type u_2} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [ M] {N : Type u_9} [ N] (b : R M) (b' : basis ι' R M) (c' : basis κ' R N) (f : M →ₗ[R] N) [fintype ι'] [fintype κ'] [fintype ι] [decidable_eq ι] [decidable_eq ι'] :
( c') f).mul (b'.to_matrix b) = c') f
theorem basis_to_matrix_mul_linear_map_to_matrix_mul_basis_to_matrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} {R : Type u_5} {M : Type u_6} [ M] {N : Type u_9} [ N] (b : R M) (b' : basis ι' R M) (c : R N) (c' : basis κ' R N) (f : M →ₗ[R] N) [fintype ι'] [fintype κ] [fintype κ'] [fintype ι] [decidable_eq ι] [decidable_eq ι'] :
((c.to_matrix c').mul ( c') f)).mul (b'.to_matrix b) = c) f
theorem basis_to_matrix_mul {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [ M] {N : Type u_9} [ N] [fintype ι'] [fintype κ] [fintype ι] [decidable_eq κ] (b₁ : R M) (b₂ : basis ι' R M) (b₃ : R N) (A : matrix ι' κ R) :
(b₁.to_matrix b₂).mul A = b₁) ( b₂) A)
theorem mul_basis_to_matrix {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [ M] {N : Type u_9} [ N] [fintype ι'] [fintype κ] [fintype ι] [decidable_eq ι] [decidable_eq ι'] (b₁ : R M) (b₂ : basis ι' R M) (b₃ : R N) (A : ι R) :
A.mul (b₁.to_matrix b₂) = b₃) ( b₃) A)
theorem basis_to_matrix_basis_fun_mul {ι : Type u_1} {R : Type u_5} [fintype ι] (b : R R)) (A : ι R) :
(b.to_matrix ι)).mul A = matrix.of (λ (i j : ι), ((b.repr) (A.transpose j)) i)
@[simp]
theorem linear_map.to_matrix_id_eq_basis_to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (b : R M) (b' : basis ι' R M) [fintype ι'] [fintype ι] [decidable_eq ι] :

A generalization of linear_map.to_matrix_id.

theorem basis.to_matrix_reindex' {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] [fintype ι'] [fintype ι] [decidable_eq ι] [decidable_eq ι'] (b : R M) (v : ι' M) (e : ι ι') :
(b.reindex e).to_matrix v = (b.to_matrix (v e))

See also basis.to_matrix_reindex which gives the simp normal form of this result.

@[simp]
theorem basis.to_matrix_mul_to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (b : R M) (b' : basis ι' R M) {ι'' : Type u_3} [fintype ι'] (b'' : ι'' M) :
(b.to_matrix b').mul (b'.to_matrix b'') = b.to_matrix b''

A generalization of basis.to_matrix_self, in the opposite direction.

theorem basis.to_matrix_mul_to_matrix_flip {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (b : R M) (b' : basis ι' R M) [decidable_eq ι] [fintype ι'] :
(b.to_matrix b').mul (b'.to_matrix b) = 1

b.to_matrix b' and b'.to_matrix b are inverses.

noncomputable def basis.invertible_to_matrix {ι : Type u_1} {R₂ : Type u_7} {M₂ : Type u_8} [comm_ring R₂] [add_comm_group M₂] [module R₂ M₂] [decidable_eq ι] [fintype ι] (b b' : R₂ M₂) :

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

Equations
@[simp]
theorem basis.to_matrix_reindex {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [ M] (b : R M) (v : ι' M) (e : ι ι') :
@[simp]
theorem basis.to_matrix_map {ι : Type u_1} {R : Type u_5} {M : Type u_6} [ M] {N : Type u_9} [ N] (b : R M) (f : M ≃ₗ[R] N) (v : ι N) :
(b.map f).to_matrix v = b.to_matrix ((f.symm) v)