mathlib3 documentation

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 #

Main results #

Tags #

matrix, basis

noncomputable def basis.to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [comm_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] (e : basis ι 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_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] (e : basis ι 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 : basis ι 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 : basis ι 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} [comm_semiring R] [add_comm_monoid M] [module R M] (e : basis ι 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_semiring R] {S : Type u_3} [ring S] [algebra R S] [fintype ι] (b : basis ι R S) (v : ι' S) :
@[simp]
theorem basis.to_lin_to_matrix {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] (e : basis ι 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_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] {N : Type u_9} [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] {N : Type u_9} [add_comm_monoid 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 ι'] :
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_semiring R] [add_comm_monoid M] [module R M] {N : Type u_9} [add_comm_monoid 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 ι'] :
theorem basis_to_matrix_mul {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {R : Type u_5} {M : Type u_6} [comm_semiring R] [add_comm_monoid M] [module R M] {N : Type u_9} [add_comm_monoid N] [module R N] [fintype ι'] [fintype κ] [fintype ι] [decidable_eq κ] (b₁ : basis ι R M) (b₂ : basis ι' R M) (b₃ : basis κ R N) (A : matrix ι' κ R) :
(b₁.to_matrix b₂).mul A = (linear_map.to_matrix b₃ b₁) ((matrix.to_lin 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} [comm_semiring R] [add_comm_monoid M] [module R M] {N : Type u_9} [add_comm_monoid N] [module R N] [fintype ι'] [fintype κ] [fintype ι] [decidable_eq ι] [decidable_eq ι'] (b₁ : basis ι R M) (b₂ : basis ι' R M) (b₃ : basis κ R N) (A : matrix κ ι R) :
A.mul (b₁.to_matrix b₂) = (linear_map.to_matrix b₂ b₃) ((matrix.to_lin b₁ b₃) A)
theorem basis_to_matrix_basis_fun_mul {ι : Type u_1} {R : Type u_5} [comm_semiring R] [fintype ι] (b : basis ι R R)) (A : matrix ι ι R) :
(b.to_matrix (pi.basis_fun R ι)).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} [comm_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] (b : basis ι 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_semiring R] [add_comm_monoid M] [module R M] (b : basis ι 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' : basis ι 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} [comm_semiring R] [add_comm_monoid 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_semiring R] [add_comm_monoid M] [module R M] {N : Type u_9} [add_comm_monoid 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)