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

source

noncomputable 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

e.to_matrix v = λ (i : ι) (j : ι'), ⇑(⇑(e.repr) (v j)) i

source

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

source

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

source

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) :

e.to_matrix v = ⇑(linear_map.to_matrix e e) (⇑(e.constr ℕ) v)

source

theorem basis.coe_pi_basis_fun.to_matrix_eq_transpose {ι : Type u_1} {R : Type u_5} [comm_ring R] [fintype ι] :

(pi.basis_fun R ι).to_matrix = matrix.transpose

source

@[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 ι] :

e.to_matrix ⇑e = 1

source

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) :

e.to_matrix (function.update v j x) = (e.to_matrix v).update_column j ⇑(⇑(e.repr) x)

source

@[simp]

theorem basis.to_matrix_units_smul {ι : 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 ι] (w : ι → Rˣ) :

e.to_matrix ⇑(e.units_smul w) = matrix.diagonal (coe ∘ w)

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

source

@[simp]

theorem basis.to_matrix_is_unit_smul {ι : 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 ι] {w : ι → R} (hw : ∀ (i : ι), is_unit (w i)) :

e.to_matrix ⇑(e.is_unit_smul hw) = matrix.diagonal w

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

source

@[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

source

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] [algebra R S] [fintype ι] (b : basis ι R S) (v : ι' → S) :

matrix.vec_mul ⇑b ((b.to_matrix v).map ⇑(algebra_map R S)) = v

source

@[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) :

⇑(matrix.to_lin v e) (e.to_matrix ⇑v) = linear_map.id

source

noncomputable 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

e.to_matrix_equiv = {to_fun := e.to_matrix, map_add' := _, map_smul' := _, inv_fun := λ (m : matrix ι ι R) (j : ι), ∑ (i : ι), m i j • ⇑e i, left_inv := _, right_inv := _}

source

@[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 ι'] :

c.to_matrix ⇑c' ⬝ ⇑(linear_map.to_matrix b' c') f = ⇑(linear_map.to_matrix b' c) f

source

@[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 ι'] :

⇑(linear_map.to_matrix b' c') f ⬝ b'.to_matrix ⇑b = ⇑(linear_map.to_matrix b c') f

source

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] [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) (c' : basis κ' R N) (f : M →ₗ[R] N) [fintype ι'] [fintype κ] [fintype κ'] [fintype ι] [decidable_eq ι] [decidable_eq ι'] :

c.to_matrix ⇑c' ⬝ ⇑(linear_map.to_matrix b' c') f ⬝ b'.to_matrix ⇑b = ⇑(linear_map.to_matrix b c) f

source

@[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 ι] :

⇑(linear_map.to_matrix b b') linear_map.id = b'.to_matrix ⇑b

A generalization of linear_map.to_matrix_id.

source

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 : ι ≃ ι') :

(b.reindex e).to_matrix v = ⇑(matrix.reindex_alg_equiv R e) (b.to_matrix (v ∘ ⇑e))

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

source

@[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) :

b.to_matrix ⇑b' ⬝ b'.to_matrix b'' = b.to_matrix b''

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

source

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' ⬝ b'.to_matrix ⇑b = 1

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

source

@[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 : ι ≃ ι') :

(b.reindex e).to_matrix v = (b.to_matrix v).minor ⇑(e.symm) id

source

@[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)