# mathlibdocumentation

linear_algebra.matrix.basis

# Bases and matrices #

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} [comm_ring R] [ 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} [comm_ring R] [ 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} [comm_ring R] [ 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} [comm_ring R] [ M] (e : R M) [fintype ι] [decidable_eq ι] (v : ι → M) :
e.to_matrix v = e) ((e.constr ) v)
theorem basis.coe_pi_basis_fun.to_matrix_eq_transpose {ι : Type u_1} {R : Type u_5} [comm_ring R] [fintype ι] :
@[simp]
theorem basis.to_matrix_self {ι : Type u_1} {R : Type u_5} {M : Type u_6} [comm_ring R] [ 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} [comm_ring R] [ M] (e : R M) (v : ι' → M) (j : ι') [decidable_eq ι'] (x : M) :
@[simp]
theorem basis.to_matrix_units_smul {ι : Type u_1} {R : Type u_5} {M : Type u_6} [comm_ring R] [ M] (e : R M) [decidable_eq ι] (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_5} {M : Type u_6} [comm_ring R] [ M] (e : R M) [decidable_eq ι] {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} [comm_ring R] [ 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} [comm_ring R] {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} [comm_ring R] [ 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} [comm_ring R] [ 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} [comm_ring R] [ M] {N : Type u_7} [ 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} [comm_ring R] [ M] {N : Type u_7} [ 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} [comm_ring R] [ M] {N : Type u_7} [ 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
@[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} [comm_ring R] [ 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} [comm_ring R] [ 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} [comm_ring R] [ 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} [comm_ring R] [ 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.

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