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 vis the matrix whosei, jth entry ise.repr (v j) ibasis.to_matrix_equivisbasis.to_matrixbundled as a linear equiv
Main results #
linear_map.to_matrix_id_eq_basis_to_matrix:linear_map.to_matrix b c idis equal tobasis.to_matrix b cbasis.to_matrix_mul_to_matrix: multiplyingbasis.to_matrixwith anotherbasis.to_matrixgives abasis.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_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.
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) :
theorem
basis.coe_pi_basis_fun.to_matrix_eq_transpose
{ι : Type u_1}
{R : Type u_5}
[comm_semiring R]
[fintype ι] :
@[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) :
e.to_matrix (function.update v j x) = (e.to_matrix v).update_column j ⇑(⇑(e.repr) x)
@[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₂ˣ) :
e.to_matrix ⇑(e.units_smul w) = matrix.diagonal (coe ∘ w)
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)) :
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.
@[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 ι] :
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) :
matrix.vec_mul ⇑b ((b.to_matrix v).map ⇑(algebra_map R S)) = v
@[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) :
⇑(matrix.to_lin v e) (e.to_matrix ⇑v) = linear_map.id
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) :
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.
@[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 ι'] :
(c.to_matrix ⇑c').mul (⇑(linear_map.to_matrix b' c') f) = ⇑(linear_map.to_matrix b' 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_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 ι'] :
(⇑(linear_map.to_matrix b' c') f).mul (b'.to_matrix ⇑b) = ⇑(linear_map.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_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)
@[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 ι] :
⇑(linear_map.to_matrix b b') linear_map.id = b'.to_matrix ⇑b
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) :
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' 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₂) :
invertible (b.to_matrix ⇑b')
A matrix whose columns form a basis b', expressed w.r.t. a basis b, is invertible.
Equations
- b.invertible_to_matrix b' = {inv_of := b'.to_matrix ⇑b, inv_of_mul_self := _, mul_inv_of_self := _}