Linear maps and matrices #
This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.
Main definitions #
In the list below, and in all this file, R is a commutative ring (semiring
is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite
types used for indexing.
linear_map.to_matrix: given basesv₁ : ι → M₁andv₂ : κ → M₂, theR-linear equivalence fromM₁ →ₗ[R] M₂tomatrix κ ι Rmatrix.to_lin: the inverse oflinear_map.to_matrixlinear_map.to_matrix': theR-linear equivalence from(n → R) →ₗ[R] (m → R)tomatrix n m R(with the standard basis onn → Randm → R)matrix.to_lin': the inverse oflinear_map.to_matrix'alg_equiv_matrix: given a basis indexed byn, theR-algebra equivalence betweenR-endomorphisms ofMandmatrix n n R
Tags #
linear_map, matrix, linear_equiv, diagonal, det, trace
@[protected, instance]
def
matrix.fintype
{n : Type u_1}
{m : Type u_2}
[fintype m]
[decidable_eq m]
[fintype n]
[decidable_eq n]
(R : Type u_3)
[fintype R] :
Equations
- matrix.fintype R = _.mpr pi.fintype
def
matrix.mul_vec_lin
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
(M : matrix m n R) :
matrix.mul_vec M is a linear map.
@[simp]
theorem
matrix.mul_vec_lin_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
(M : matrix m n R)
(v : n → R) :
⇑(M.mul_vec_lin) v = M.mul_vec v
@[simp]
theorem
matrix.mul_vec_std_basis
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
(M : matrix m n R)
(i : m)
(j : n) :
M.mul_vec (⇑(linear_map.std_basis R (λ (_x : n), R) j) 1) i = M i j
def
linear_map.to_matrix'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n] :
Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R.
Equations
- linear_map.to_matrix' = {to_fun := λ (f : (n → R) →ₗ[R] m → R) (i : m) (j : n), ⇑f (⇑(linear_map.std_basis R (λ (_x : n), R) j) 1) i, map_add' := _, map_smul' := _, inv_fun := matrix.mul_vec_lin _inst_2, left_inv := _, right_inv := _}
def
matrix.to_lin'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n] :
A matrix m n R is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R).
Equations
@[simp]
theorem
linear_map.to_matrix'_symm
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_lin'_symm
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
linear_map.to_matrix'_to_lin'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
(M : matrix m n R) :
@[simp]
theorem
matrix.to_lin'_to_matrix'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f : (n → R) →ₗ[R] m → R) :
@[simp]
theorem
linear_map.to_matrix'_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f : (n → R) →ₗ[R] m → R)
(i : m)
(j : n) :
@[simp]
theorem
matrix.to_lin'_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
(M : matrix m n R)
(v : n → R) :
⇑(⇑matrix.to_lin' M) v = M.mul_vec v
@[simp]
theorem
matrix.to_lin'_one
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
linear_map.to_matrix'_id
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_lin'_mul
{R : Type u_1}
[comm_ring R]
{l : Type u_2}
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
[fintype m]
[decidable_eq m]
(M : matrix l m R)
(N : matrix m n R) :
⇑matrix.to_lin' (M ⬝ N) = (⇑matrix.to_lin' M).comp (⇑matrix.to_lin' N)
theorem
matrix.to_lin'_mul_apply
{R : Type u_1}
[comm_ring R]
{l : Type u_2}
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
[fintype m]
[decidable_eq m]
(M : matrix l m R)
(N : matrix m n R)
(x : n → R) :
⇑(⇑matrix.to_lin' (M ⬝ N)) x = ⇑(⇑matrix.to_lin' M) (⇑(⇑matrix.to_lin' N) x)
Shortcut lemma for matrix.to_lin'_mul and linear_map.comp_apply
theorem
linear_map.to_matrix'_comp
{R : Type u_1}
[comm_ring R]
{l : Type u_2}
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
[fintype l]
[decidable_eq l]
(f : (n → R) →ₗ[R] m → R)
(g : (l → R) →ₗ[R] n → R) :
theorem
linear_map.to_matrix'_mul
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
[fintype m]
[decidable_eq m]
(f g : (m → R) →ₗ[R] m → R) :
@[simp]
theorem
linear_map.to_matrix'_algebra_map
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(x : R) :
⇑linear_map.to_matrix' (⇑(algebra_map R (module.End R (n → R))) x) = ⇑(matrix.scalar n) x
theorem
matrix.ker_to_lin'_eq_bot_iff
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M : matrix n n R} :
@[simp]
theorem
matrix.to_lin'_of_inv_symm_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
[fintype m]
[decidable_eq m]
{M : matrix m n R}
{M' : matrix n m R}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1)
(ᾰ : n → R)
(ᾰ_1 : m) :
⇑((matrix.to_lin'_of_inv hMM' hM'M).symm) ᾰ ᾰ_1 = ⇑(⇑matrix.to_lin' M) ᾰ ᾰ_1
def
matrix.to_lin'_of_inv
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
[fintype m]
[decidable_eq m]
{M : matrix m n R}
{M' : matrix n m R}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1) :
If M and M' are each other's inverse matrices, they provide an equivalence between m → A
and n → A corresponding to M.mul_vec and M'.mul_vec.
Equations
- matrix.to_lin'_of_inv hMM' hM'M = {to_fun := ⇑(⇑matrix.to_lin' M'), map_add' := _, map_smul' := _, inv_fun := ⇑(⇑matrix.to_lin' M), left_inv := _, right_inv := _}
@[simp]
theorem
matrix.to_lin'_of_inv_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n]
[fintype m]
[decidable_eq m]
{M : matrix m n R}
{M' : matrix n m R}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1)
(ᾰ : m → R)
(ᾰ_1 : n) :
⇑(matrix.to_lin'_of_inv hMM' hM'M) ᾰ ᾰ_1 = ⇑(⇑matrix.to_lin' M') ᾰ ᾰ_1
def
linear_map.to_matrix_alg_equiv'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
Linear maps (n → R) →ₗ[R] (n → R) are algebra equivalent to matrix n n R.
Equations
- linear_map.to_matrix_alg_equiv' = alg_equiv.of_linear_equiv linear_map.to_matrix' linear_map.to_matrix_alg_equiv'._proof_1 linear_map.to_matrix_alg_equiv'._proof_2
def
matrix.to_lin_alg_equiv'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
A matrix n n R is algebra equivalent to a linear map (n → R) →ₗ[R] (n → R).
@[simp]
theorem
linear_map.to_matrix_alg_equiv'_symm
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_lin_alg_equiv'_symm
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
linear_map.to_matrix_alg_equiv'_to_lin_alg_equiv'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(M : matrix n n R) :
@[simp]
theorem
matrix.to_lin_alg_equiv'_to_matrix_alg_equiv'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f : (n → R) →ₗ[R] n → R) :
@[simp]
theorem
linear_map.to_matrix_alg_equiv'_apply
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f : (n → R) →ₗ[R] n → R)
(i j : n) :
@[simp]
theorem
matrix.to_lin_alg_equiv'_apply
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(M : matrix n n R)
(v : n → R) :
⇑(⇑matrix.to_lin_alg_equiv' M) v = M.mul_vec v
@[simp]
theorem
matrix.to_lin_alg_equiv'_one
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
linear_map.to_matrix_alg_equiv'_id
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_lin_alg_equiv'_mul
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(M N : matrix n n R) :
theorem
linear_map.to_matrix_alg_equiv'_comp
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f g : (n → R) →ₗ[R] n → R) :
theorem
linear_map.to_matrix_alg_equiv'_mul
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f g : (n → R) →ₗ[R] n → R) :
theorem
matrix.rank_vec_mul_vec
{K m n : Type u}
[field K]
[fintype n]
[decidable_eq n]
(w : m → K)
(v : n → K) :
rank (⇑matrix.to_lin' (matrix.vec_mul_vec w v)) ≤ 1
noncomputable
def
linear_map.to_matrix
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂) :
Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear
equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.
Equations
- linear_map.to_matrix v₁ v₂ = (v₁.equiv_fun.arrow_congr v₂.equiv_fun).trans linear_map.to_matrix'
theorem
linear_map.to_matrix_eq_to_matrix'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
linear_map.to_matrix' is a particular case of linear_map.to_matrix, for the standard basis
pi.basis_fun R n.
noncomputable
def
matrix.to_lin
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂) :
Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear
equivalence between matrices over R indexed by the bases and linear maps M₁ →ₗ M₂.
Equations
- matrix.to_lin v₁ v₂ = (linear_map.to_matrix v₁ v₂).symm
theorem
matrix.to_lin_eq_to_lin'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
matrix.to_lin (pi.basis_fun R n) (pi.basis_fun R n) = matrix.to_lin'
matrix.to_lin' is a particular case of matrix.to_lin, for the standard basis
pi.basis_fun R n.
@[simp]
theorem
linear_map.to_matrix_symm
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂) :
(linear_map.to_matrix v₁ v₂).symm = matrix.to_lin v₁ v₂
@[simp]
theorem
matrix.to_lin_symm
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂) :
(matrix.to_lin v₁ v₂).symm = linear_map.to_matrix v₁ v₂
@[simp]
theorem
matrix.to_lin_to_matrix
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(f : M₁ →ₗ[R] M₂) :
⇑(matrix.to_lin v₁ v₂) (⇑(linear_map.to_matrix v₁ v₂) f) = f
@[simp]
theorem
linear_map.to_matrix_to_lin
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(M : matrix m n R) :
⇑(linear_map.to_matrix v₁ v₂) (⇑(matrix.to_lin v₁ v₂) M) = M
theorem
linear_map.to_matrix_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(f : M₁ →ₗ[R] M₂)
(i : m)
(j : n) :
theorem
linear_map.to_matrix_transpose_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(f : M₁ →ₗ[R] M₂)
(j : n) :
theorem
linear_map.to_matrix_apply'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(f : M₁ →ₗ[R] M₂)
(i : m)
(j : n) :
theorem
linear_map.to_matrix_transpose_apply'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(f : M₁ →ₗ[R] M₂)
(j : n) :
theorem
matrix.to_lin_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(M : matrix m n R)
(v : M₁) :
@[simp]
theorem
matrix.to_lin_self
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(M : matrix m n R)
(i : n) :
theorem
linear_map.to_matrix_id
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
⇑(linear_map.to_matrix v₁ v₁) linear_map.id = 1
This will be a special case of linear_map.to_matrix_id_eq_basis_to_matrix.
theorem
linear_map.to_matrix_one
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
⇑(linear_map.to_matrix v₁ v₁) 1 = 1
@[simp]
theorem
matrix.to_lin_one
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
⇑(matrix.to_lin v₁ v₁) 1 = linear_map.id
theorem
linear_map.to_matrix_reindex_range
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
[decidable_eq M₁]
[decidable_eq M₂]
(f : M₁ →ₗ[R] M₂)
(k : m)
(i : n) :
⇑(linear_map.to_matrix v₁.reindex_range v₂.reindex_range) f ⟨⇑v₂ k, _⟩ ⟨⇑v₁ i, _⟩ = ⇑(linear_map.to_matrix v₁ v₂) f k i
theorem
linear_map.to_matrix_comp
{R : Type u_1}
[comm_ring R]
{l : Type u_2}
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
{M₃ : Type u_7}
[add_comm_group M₃]
[module R M₃]
(v₃ : basis l R M₃)
[fintype l]
[decidable_eq m]
(f : M₂ →ₗ[R] M₃)
(g : M₁ →ₗ[R] M₂) :
⇑(linear_map.to_matrix v₁ v₃) (f.comp g) = ⇑(linear_map.to_matrix v₂ v₃) f ⬝ ⇑(linear_map.to_matrix v₁ v₂) g
theorem
linear_map.to_matrix_mul
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f g : M₁ →ₗ[R] M₁) :
⇑(linear_map.to_matrix v₁ v₁) (f * g) = ⇑(linear_map.to_matrix v₁ v₁) f ⬝ ⇑(linear_map.to_matrix v₁ v₁) g
@[simp]
theorem
linear_map.to_matrix_algebra_map
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(x : R) :
⇑(linear_map.to_matrix v₁ v₁) (⇑(algebra_map R (module.End R M₁)) x) = ⇑(matrix.scalar n) x
theorem
linear_map.to_matrix_mul_vec_repr
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
(f : M₁ →ₗ[R] M₂)
(x : M₁) :
theorem
matrix.to_lin_mul
{R : Type u_1}
[comm_ring R]
{l : Type u_2}
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
{M₃ : Type u_7}
[add_comm_group M₃]
[module R M₃]
(v₃ : basis l R M₃)
[fintype l]
[decidable_eq m]
(A : matrix l m R)
(B : matrix m n R) :
⇑(matrix.to_lin v₁ v₃) (A ⬝ B) = (⇑(matrix.to_lin v₂ v₃) A).comp (⇑(matrix.to_lin v₁ v₂) B)
theorem
matrix.to_lin_mul_apply
{R : Type u_1}
[comm_ring R]
{l : Type u_2}
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
{M₃ : Type u_7}
[add_comm_group M₃]
[module R M₃]
(v₃ : basis l R M₃)
[fintype l]
[decidable_eq m]
(A : matrix l m R)
(B : matrix m n R)
(x : M₁) :
⇑(⇑(matrix.to_lin v₁ v₃) (A ⬝ B)) x = ⇑(⇑(matrix.to_lin v₂ v₃) A) (⇑(⇑(matrix.to_lin v₁ v₂) B) x)
Shortcut lemma for matrix.to_lin_mul and linear_map.comp_apply.
@[simp]
theorem
matrix.to_lin_of_inv_symm_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
[decidable_eq m]
{M : matrix m n R}
{M' : matrix n m R}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1)
(ᾰ : M₂) :
⇑((matrix.to_lin_of_inv v₁ v₂ hMM' hM'M).symm) ᾰ = ⇑(⇑(matrix.to_lin v₂ v₁) M') ᾰ
noncomputable
def
matrix.to_lin_of_inv
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
[decidable_eq m]
{M : matrix m n R}
{M' : matrix n m R}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1) :
If M and M are each other's inverse matrices, matrix.to_lin M and matrix.to_lin M'
form a linear equivalence.
Equations
- matrix.to_lin_of_inv v₁ v₂ hMM' hM'M = {to_fun := ⇑(⇑(matrix.to_lin v₁ v₂) M), map_add' := _, map_smul' := _, inv_fun := ⇑(⇑(matrix.to_lin v₂ v₁) M'), left_inv := _, right_inv := _}
@[simp]
theorem
matrix.to_lin_of_inv_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n]
{M₁ : Type u_5}
{M₂ : Type u_6}
[add_comm_group M₁]
[add_comm_group M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
[decidable_eq m]
{M : matrix m n R}
{M' : matrix n m R}
(hMM' : M ⬝ M' = 1)
(hM'M : M' ⬝ M = 1)
(ᾰ : M₁) :
⇑(matrix.to_lin_of_inv v₁ v₂ hMM' hM'M) ᾰ = ⇑(⇑(matrix.to_lin v₁ v₂) M) ᾰ
noncomputable
def
linear_map.to_matrix_alg_equiv
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
Given a basis of a module M₁ over a commutative ring R, we get an algebra
equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis.
Equations
noncomputable
def
matrix.to_lin_alg_equiv
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
Given a basis of a module M₁ over a commutative ring R, we get an algebra
equivalence between square matrices over R indexed by the basis and linear maps M₁ →ₗ M₁.
Equations
@[simp]
theorem
linear_map.to_matrix_alg_equiv_symm
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
@[simp]
theorem
matrix.to_lin_alg_equiv_symm
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
@[simp]
theorem
matrix.to_lin_alg_equiv_to_matrix_alg_equiv
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f : M₁ →ₗ[R] M₁) :
⇑(matrix.to_lin_alg_equiv v₁) (⇑(linear_map.to_matrix_alg_equiv v₁) f) = f
@[simp]
theorem
linear_map.to_matrix_alg_equiv_to_lin_alg_equiv
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(M : matrix n n R) :
⇑(linear_map.to_matrix_alg_equiv v₁) (⇑(matrix.to_lin_alg_equiv v₁) M) = M
theorem
linear_map.to_matrix_alg_equiv_apply
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f : M₁ →ₗ[R] M₁)
(i j : n) :
theorem
linear_map.to_matrix_alg_equiv_transpose_apply
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f : M₁ →ₗ[R] M₁)
(j : n) :
theorem
linear_map.to_matrix_alg_equiv_apply'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f : M₁ →ₗ[R] M₁)
(i j : n) :
theorem
linear_map.to_matrix_alg_equiv_transpose_apply'
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f : M₁ →ₗ[R] M₁)
(j : n) :
theorem
matrix.to_lin_alg_equiv_apply
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(M : matrix n n R)
(v : M₁) :
@[simp]
theorem
matrix.to_lin_alg_equiv_self
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(M : matrix n n R)
(i : n) :
theorem
linear_map.to_matrix_alg_equiv_id
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
@[simp]
theorem
matrix.to_lin_alg_equiv_one
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁) :
theorem
linear_map.to_matrix_alg_equiv_reindex_range
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
[decidable_eq M₁]
(f : M₁ →ₗ[R] M₁)
(k i : n) :
⇑(linear_map.to_matrix_alg_equiv v₁.reindex_range) f ⟨⇑v₁ k, _⟩ ⟨⇑v₁ i, _⟩ = ⇑(linear_map.to_matrix_alg_equiv v₁) f k i
theorem
linear_map.to_matrix_alg_equiv_comp
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f g : M₁ →ₗ[R] M₁) :
⇑(linear_map.to_matrix_alg_equiv v₁) (f.comp g) = ⇑(linear_map.to_matrix_alg_equiv v₁) f ⬝ ⇑(linear_map.to_matrix_alg_equiv v₁) g
theorem
linear_map.to_matrix_alg_equiv_mul
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(f g : M₁ →ₗ[R] M₁) :
⇑(linear_map.to_matrix_alg_equiv v₁) (f * g) = ⇑(linear_map.to_matrix_alg_equiv v₁) f ⬝ ⇑(linear_map.to_matrix_alg_equiv v₁) g
theorem
matrix.to_lin_alg_equiv_mul
{R : Type u_1}
[comm_ring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_group M₁]
[module R M₁]
(v₁ : basis n R M₁)
(A B : matrix n n R) :
⇑(matrix.to_lin_alg_equiv v₁) (A ⬝ B) = (⇑(matrix.to_lin_alg_equiv v₁) A).comp (⇑(matrix.to_lin_alg_equiv v₁) B)
theorem
algebra.to_matrix_lmul'
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(x : S)
(i j : m) :
⇑(linear_map.to_matrix b b) (⇑(algebra.lmul R S) x) i j = ⇑(⇑(b.repr) (x * ⇑b j)) i
@[simp]
theorem
algebra.to_matrix_lsmul
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(x : R)
(i j : m) :
⇑(linear_map.to_matrix b b) (⇑(algebra.lsmul R S) x) i j = ite (i = j) x 0
noncomputable
def
algebra.left_mul_matrix
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S) :
left_mul_matrix b x is the matrix corresponding to the linear map λ y, x * y.
left_mul_matrix_eq_repr_mul gives a formula for the entries of left_mul_matrix.
This definition is useful for doing (more) explicit computations with algebra.lmul,
such as the trace form or norm map for algebras.
Equations
- algebra.left_mul_matrix b = {to_fun := λ (x : S), ⇑(linear_map.to_matrix b b) (⇑(algebra.lmul R S) x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
algebra.left_mul_matrix_apply
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(x : S) :
⇑(algebra.left_mul_matrix b) x = ⇑(linear_map.to_matrix b b) (⇑(algebra.lmul R S) x)
@[simp]
theorem
algebra.to_matrix_lmul_eq
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(x : S) :
⇑(linear_map.to_matrix b b) (⇑(algebra.lmul R S) x) = ⇑(algebra.left_mul_matrix b) x
theorem
algebra.left_mul_matrix_injective
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S) :
theorem
algebra.smul_left_mul_matrix
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : T)
(ik jk : m × n) :
⇑(algebra.left_mul_matrix (b.smul c)) x ik jk = ⇑(algebra.left_mul_matrix b) (⇑(algebra.left_mul_matrix c) x ik.snd jk.snd) ik.fst jk.fst
theorem
algebra.smul_left_mul_matrix_algebra_map
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : S) :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) = matrix.block_diagonal (λ (k : n), ⇑(algebra.left_mul_matrix b) x)
theorem
algebra.smul_left_mul_matrix_algebra_map_eq
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : S)
(i j : m)
(k : n) :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) (i, k) (j, k) = ⇑(algebra.left_mul_matrix b) x i j
theorem
algebra.smul_left_mul_matrix_algebra_map_ne
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : S)
(i j : m)
{k k' : n}
(h : k ≠ k') :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) (i, k) (j, k') = 0
@[protected, instance]
def
linear_map.finite_dimensional
{K : Type u_1}
[field K]
{V : Type u_2}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_3}
[add_comm_group W]
[module K W]
[finite_dimensional K W] :
finite_dimensional K (V →ₗ[K] W)
@[simp]
theorem
linear_map.finrank_linear_map
{K : Type u_1}
[field K]
{V : Type u_2}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_3}
[add_comm_group W]
[module K W]
[finite_dimensional K W] :
finite_dimensional.finrank K (V →ₗ[K] W) = (finite_dimensional.finrank K V) * finite_dimensional.finrank K W
The dimension of the space of linear transformations is the product of the dimensions of the domain and codomain.
def
alg_equiv_matrix'
{R : Type v}
[comm_ring R]
{n : Type u_1}
[decidable_eq n]
[fintype n] :
module.End R (n → R) ≃ₐ[R] matrix n n R
The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the algebra structures.
Equations
- alg_equiv_matrix' = {to_fun := linear_map.to_matrix'.to_fun, inv_fun := linear_map.to_matrix'.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
def
linear_equiv.alg_conj
{R : Type v}
[comm_ring R]
{M₁ : Type u_3}
{M₂ : Type u_4}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
(e : M₁ ≃ₗ[R] M₂) :
module.End R M₁ ≃ₐ[R] module.End R M₂
A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.
noncomputable
def
alg_equiv_matrix
{R : Type v}
[comm_ring R]
{n : Type u_1}
[decidable_eq n]
{M : Type u_2}
[add_comm_group M]
[module R M]
[fintype n]
(h : basis n R M) :
module.End R M ≃ₐ[R] matrix n n R
A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.