mathlib documentation

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 #

Main results #

Tags #

matrix, basis

def basis.to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group 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.

Equations
theorem basis.to_matrix_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] (e : basis ι 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] [add_comm_group M] [module R M] (e : basis ι R M) (v : ι' → M) (j : ι') :
(e.to_matrix v) 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] [add_comm_group M] [module R M] (e : basis ι R M) [fintype ι] [decidable_eq ι] (v : ι → M) :
@[simp]
theorem basis.to_matrix_self {ι : Type u_1} {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] (e : basis ι 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] [add_comm_group M] [module R M] (e : basis ι R M) (v : ι' → M) (j : ι') [decidable_eq ι'] (x : M) :
@[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] [add_comm_group M] [module R M] (e : basis ι R M) (v : ι' → M) (j : ι') [fintype ι] :
∑ (i : ι), e.to_matrix v i j e i = v j
@[simp]
theorem basis.to_lin_to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group M] [module R M] (e : basis ι R M) [fintype ι] [fintype ι'] [decidable_eq ι'] (v : basis ι' R M) :
def basis.to_matrix_equiv {ι : Type u_1} {R : Type u_5} {M : Type u_6} [comm_ring R] [add_comm_group 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.

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] [add_comm_group M] [module R M] {N : Type u_7} [add_comm_group N] [module R N] (b' : basis ι' R M) (c : basis κ R N) (c' : basis κ' R N) (f : M →ₗ[R] N) [fintype ι'] [fintype κ] [fintype κ'] [decidable_eq ι'] :
@[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] [add_comm_group M] [module R M] {N : Type u_7} [add_comm_group N] [module R N] (b : basis ι R M) (b' : basis ι' R M) (c' : basis κ' R N) (f : M →ₗ[R] N) [fintype ι'] [fintype κ'] [fintype ι] [decidable_eq ι] [decidable_eq ι'] :
@[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] [add_comm_group M] [module R M] (b : basis ι 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] [add_comm_group M] [module R M] [fintype ι'] [fintype ι] [decidable_eq ι] [decidable_eq ι'] (b : basis ι R M) (v : ι' → M) (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] [add_comm_group M] [module R M] (b : basis ι R M) (b' : basis ι' R M) {ι'' : Type u_3} [fintype ι'] (b'' : ι'' → M) :

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] [add_comm_group M] [module R M] (b : basis ι R M) (b' : basis ι' R M) [decidable_eq ι] [fintype ι'] :

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] [add_comm_group M] [module R M] (b : basis ι 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] [add_comm_group M] [module R M] {N : Type u_7} [add_comm_group N] [module R N] (b : basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N) :
(b.map f).to_matrix v = b.to_matrix ((f.symm) v)