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.
It also defines the trace of an endomorphism, and the determinant of a family of vectors with respect to some basis.
Some results are proved about the linear map corresponding to a
diagonal matrix (range, ker and rank).
Some results are proved for determinants of block triangular matrices.
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 κ ι R -
matrix.to_lin: the inverse oflinear_map.to_matrix -
linear_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 -
matrix.trace: the trace of a square matrix -
linear_map.trace: the trace of an endomorphism -
basis.to_matrix: the matrix whose columns are a given family of vectors in a given basis -
basis.to_matrix_equiv: given a basis, the linear equivalence between families of vectors and matrices arising frombasis.to_matrix -
basis.det: the determinant of a family of vectors with respect to a basis, as a multilinear map
Tags #
linear_map, matrix, linear_equiv, diagonal, det, trace
@[protected, instance]
def
matrix.fintype
{m : Type u_3}
{n : Type u_4}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
(R : Type u_1)
[fintype R] :
Equations
- matrix.fintype R = _.mpr pi.fintype
@[simp]
theorem
matrix.mul_vec_lin_apply
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype m]
[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 m]
[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 m]
[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_4, left_inv := _, right_inv := _}
def
matrix.to_lin'
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype m]
[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 m]
[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 m]
[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 m]
[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 m]
[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 m]
[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 m]
[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 l]
[fintype m]
[fintype n]
[decidable_eq n]
[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
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 l]
[fintype m]
[fintype n]
[decidable_eq n]
[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) :
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) :
def
linear_map.to_matrix
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype m]
[fintype n]
[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'
def
matrix.to_lin
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype m]
[fintype n]
[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
@[simp]
theorem
linear_map.to_matrix_symm
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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 m]
[fintype n]
[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₂)
[nontrivial R]
[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 l]
[fintype m]
[fintype n]
[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₃)
[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
theorem
linear_map.to_matrix_mul_vec_repr
{R : Type u_1}
[comm_ring R]
{m : Type u_3}
{n : Type u_4}
[fintype m]
[fintype n]
[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 l]
[fintype m]
[fintype n]
[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₃)
[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)
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
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₁)
[nontrivial R]
[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)
def
basis.to_matrix
{ι : Type u_1}
{ι' : Type u_2}
[fintype ι]
[fintype ι']
{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.
theorem
basis.to_matrix_eq_to_matrix_constr
{ι : Type u_1}
[fintype ι]
{R : Type u_5}
{M : Type u_6}
[comm_ring R]
[add_comm_group M]
[module R M]
(e : basis ι R M)
[decidable_eq ι]
(v : ι → M) :
@[simp]
theorem
basis.to_matrix_self
{ι : Type u_1}
[fintype ι]
{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}
[fintype ι]
[fintype ι']
{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)
@[simp]
theorem
basis.to_lin_to_matrix
{ι : Type u_1}
{ι' : Type u_2}
[fintype ι]
[fintype ι']
{R : Type u_5}
{M : Type u_6}
[comm_ring R]
[add_comm_group M]
[module R M]
(e : basis ι R M)
[decidable_eq ι']
(v : basis ι' R M) :
⇑(matrix.to_lin v e) (e.to_matrix ⇑v) = linear_map.id
def
basis.to_matrix_equiv
{ι : Type u_1}
[fintype ι]
{R : Type u_5}
{M : Type u_6}
[comm_ring R]
[add_comm_group M]
[module R M]
(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}
[fintype ι']
[fintype κ]
[fintype κ']
{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)
[decidable_eq ι'] :
c.to_matrix ⇑c' ⬝ ⇑(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}
[fintype ι]
[fintype ι']
[fintype κ']
{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)
[decidable_eq ι]
[decidable_eq ι'] :
⇑(linear_map.to_matrix b' c') f ⬝ b'.to_matrix ⇑b = ⇑(linear_map.to_matrix b c') f
@[simp]
theorem
linear_map.to_matrix_id_eq_basis_to_matrix
{ι : Type u_1}
{ι' : Type u_2}
[fintype ι]
[fintype ι']
{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 ι] :
⇑(linear_map.to_matrix b b') linear_map.id = b'.to_matrix ⇑b
A generalization of linear_map.to_matrix_id.
@[simp]
theorem
basis.to_matrix_mul_to_matrix
{ι : Type u_1}
{ι' : Type u_2}
[fintype ι]
[fintype ι']
{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'' : basis ι'' R M) :
A generalization of basis.to_matrix_self, in the opposite direction.
theorem
linear_equiv.is_unit_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(f : M ≃ₗ[R] M')
(v : basis ι R M)
(v' : basis ι R M') :
is_unit (⇑(linear_map.to_matrix v v') ↑f).det
@[simp]
theorem
linear_equiv.of_is_unit_det_apply
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det)
(ᾰ : M) :
⇑(linear_equiv.of_is_unit_det h) ᾰ = ⇑f ᾰ
@[simp]
theorem
linear_equiv.of_is_unit_det_symm_apply
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det)
(ᾰ : M') :
⇑((linear_equiv.of_is_unit_det h).symm) ᾰ = ⇑(⇑(matrix.to_lin v' v) (⇑(linear_map.to_matrix v v') f)⁻¹) ᾰ
def
linear_equiv.of_is_unit_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{M' : Type u_3}
[add_comm_group M']
[module R M']
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
{f : M →ₗ[R] M'}
{v : basis ι R M}
{v' : basis ι R M'}
(h : is_unit (⇑(linear_map.to_matrix v v') f).det) :
Builds a linear equivalence from a linear map whose determinant in some bases is a unit.
def
basis.det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M) :
alternating_map R M R ι
Te determinant of a family of vectors with respect to some basis, as an alternating multilinear map.
theorem
basis.det_apply
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
(v : ι → M) :
theorem
basis.det_self
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M) :
theorem
is_basis.iff_det
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{ι : Type u_4}
[decidable_eq ι]
[fintype ι]
(e : basis ι R M)
{v : ι → M} :
linear_independent R v ∧ submodule.span R (set.range v) = ⊤ ↔ is_unit (⇑(e.det) v)
@[simp]
theorem
linear_map.to_matrix_transpose
{K : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[field K]
[add_comm_group V₁]
[module K V₁]
[add_comm_group V₂]
[module K V₂]
[fintype ι₁]
[fintype ι₂]
[decidable_eq ι₁]
[decidable_eq ι₂]
{B₁ : basis ι₁ K V₁}
{B₂ : basis ι₂ K V₂}
(u : V₁ →ₗ[K] V₂) :
⇑(linear_map.to_matrix B₂.dual_basis B₁.dual_basis) (⇑module.dual.transpose u) = (⇑(linear_map.to_matrix B₁ B₂) u)ᵀ
@[simp]
theorem
matrix.to_lin_transpose
{K : Type u_1}
{V₁ : Type u_2}
{V₂ : Type u_3}
{ι₁ : Type u_4}
{ι₂ : Type u_5}
[field K]
[add_comm_group V₁]
[module K V₁]
[add_comm_group V₂]
[module K V₂]
[fintype ι₁]
[fintype ι₂]
[decidable_eq ι₁]
[decidable_eq ι₂]
{B₁ : basis ι₁ K V₁}
{B₂ : basis ι₂ K V₂}
(M : matrix ι₁ ι₂ K) :
⇑(matrix.to_lin B₁.dual_basis B₂.dual_basis) Mᵀ = ⇑module.dual.transpose (⇑(matrix.to_lin B₂ B₁) M)
@[simp]
theorem
matrix.diag_apply
{n : Type u_2}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[module R M]
(A : matrix n n M)
(i : n) :
⇑(matrix.diag n R M) A i = A i i
@[simp]
theorem
matrix.diag_one
{n : Type u_2}
[fintype n]
{R : Type v}
[semiring R]
[decidable_eq n] :
⇑(matrix.diag n R R) 1 = λ (i : n), 1
@[simp]
theorem
matrix.diag_transpose
{n : Type u_2}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[module R M]
(A : matrix n n M) :
⇑(matrix.diag n R M) Aᵀ = ⇑(matrix.diag n R M) A
def
matrix.trace
(n : Type u_2)
[fintype n]
(R : Type v)
(M : Type w)
[semiring R]
[add_comm_monoid M]
[module R M] :
The trace of a square matrix.
Equations
- matrix.trace n R M = {to_fun := λ (A : matrix n n M), ∑ (i : n), ⇑(matrix.diag n R M) A i, map_add' := _, map_smul' := _}
@[simp]
theorem
matrix.trace_diag
{n : Type u_2}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[module R M]
(A : matrix n n M) :
⇑(matrix.trace n R M) A = ∑ (i : n), ⇑(matrix.diag n R M) A i
theorem
matrix.trace_apply
{n : Type u_2}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[module R M]
(A : matrix n n M) :
⇑(matrix.trace n R M) A = ∑ (i : n), A i i
@[simp]
theorem
matrix.trace_one
{n : Type u_2}
[fintype n]
{R : Type v}
[semiring R]
[decidable_eq n] :
⇑(matrix.trace n R R) 1 = ↑(fintype.card n)
@[simp]
theorem
matrix.trace_transpose
{n : Type u_2}
[fintype n]
{R : Type v}
{M : Type w}
[semiring R]
[add_comm_monoid M]
[module R M]
(A : matrix n n M) :
⇑(matrix.trace n R M) Aᵀ = ⇑(matrix.trace n R M) A
theorem
matrix.trace_mul_comm
{m : Type u_1}
[fintype m]
{n : Type u_2}
[fintype n]
{S : Type v}
[comm_ring S]
(A : matrix m n S)
(B : matrix n m S) :
⇑(matrix.trace n S S) (B ⬝ A) = ⇑(matrix.trace m S S) (A ⬝ B)
theorem
matrix.proj_diagonal
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(i : n)
(w : n → R) :
(linear_map.proj i).comp (⇑matrix.to_lin' (matrix.diagonal w)) = w i • linear_map.proj i
theorem
matrix.diagonal_comp_std_basis
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(w : n → R)
(i : n) :
(⇑matrix.to_lin' (matrix.diagonal w)).comp (linear_map.std_basis R (λ (_x : n), R) i) = w i • linear_map.std_basis R (λ (_x : n), R) i
theorem
matrix.diagonal_to_lin'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(w : n → R) :
⇑matrix.to_lin' (matrix.diagonal w) = linear_map.pi (λ (i : n), w i • linear_map.proj i)
def
matrix.to_linear_equiv'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(P : matrix n n R)
(h : is_unit P) :
An invertible matrix yields a linear equivalence from the free module to itself.
See matrix.to_linear_equiv for the same map on arbitrary modules.
@[simp]
theorem
matrix.to_linear_equiv'_apply
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(P : matrix n n R)
(h : is_unit P) :
↑(P.to_linear_equiv' h) = ⇑matrix.to_lin' P
@[simp]
theorem
matrix.to_linear_equiv'_symm_apply
{n : Type u_1}
[fintype n]
[decidable_eq n]
{R : Type v}
[comm_ring R]
(P : matrix n n R)
(h : is_unit P) :
↑((P.to_linear_equiv' h).symm) = ⇑matrix.to_lin' P⁻¹
theorem
matrix.rank_vec_mul_vec
{K : Type u}
[field K]
{m n : Type u}
[fintype m]
[fintype n]
[decidable_eq n]
(w : m → K)
(v : n → K) :
rank (⇑matrix.to_lin' (matrix.vec_mul_vec w v)) ≤ 1
theorem
matrix.ker_diagonal_to_lin'
{m : Type u_1}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
(w : m → K) :
(⇑matrix.to_lin' (matrix.diagonal w)).ker = ⨆ (i : m) (H : i ∈ {i : m | w i = 0}), (linear_map.std_basis K (λ (i : m), K) i).range
theorem
matrix.range_diagonal
{m : Type u_1}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
(w : m → K) :
(⇑matrix.to_lin' (matrix.diagonal w)).range = ⨆ (i : m) (H : i ∈ {i : m | w i ≠ 0}), (linear_map.std_basis K (λ (i : m), K) i).range
theorem
matrix.rank_diagonal
{m : Type u_1}
[fintype m]
{K : Type u}
[field K]
[decidable_eq m]
[decidable_eq K]
(w : m → K) :
rank (⇑matrix.to_lin' (matrix.diagonal w)) = ↑(fintype.card {i // w i ≠ 0})
@[simp]
theorem
matrix.to_linear_equiv_apply
{n : Type u_2}
[fintype n]
{R : Type u_3}
{M : Type u_4}
[comm_ring R]
[add_comm_group M]
[module R M]
(b : basis n R M)
[decidable_eq n]
(A : matrix n n R)
(hA : is_unit A.det)
(ᾰ : M) :
⇑(matrix.to_linear_equiv b A hA) ᾰ = ⇑(⇑(matrix.to_lin b b) A) ᾰ
def
matrix.to_linear_equiv
{n : Type u_2}
[fintype n]
{R : Type u_3}
{M : Type u_4}
[comm_ring R]
[add_comm_group M]
[module R M]
(b : basis n R M)
[decidable_eq n]
(A : matrix n n R)
(hA : is_unit A.det) :
Given hA : is_unit A.det and b : basis R b, A.to_linear_equiv b hA is
the linear_equiv arising from to_lin b b A.
See matrix.to_linear_equiv' for this result on n → R.
theorem
matrix.ker_to_lin_eq_bot
{n : Type u_2}
[fintype n]
{R : Type u_3}
{M : Type u_4}
[comm_ring R]
[add_comm_group M]
[module R M]
(b : basis n R M)
[decidable_eq n]
(A : matrix n n R)
(hA : is_unit A.det) :
(⇑(matrix.to_lin b b) A).ker = ⊥
theorem
matrix.range_to_lin_eq_top
{n : Type u_2}
[fintype n]
{R : Type u_3}
{M : Type u_4}
[comm_ring R]
[add_comm_group M]
[module R M]
(b : basis n R M)
[decidable_eq n]
(A : matrix n n R)
(hA : is_unit A.det) :
(⇑(matrix.to_lin b b) A).range = ⊤
@[protected, instance]
def
matrix.finite_dimensional
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
{R : Type v}
[field R] :
finite_dimensional R (matrix m n R)
@[simp]
theorem
matrix.finrank_matrix
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
{R : Type v}
[field R] :
finite_dimensional.finrank R (matrix m n R) = (fintype.card m) * fintype.card n
The dimension of the space of finite dimensional matrices is the product of the number of rows and columns.
def
matrix.reindex_linear_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{m' : Type u_5}
{n' : Type u_6}
[fintype m']
[fintype n']
{R : Type v}
[semiring R]
(eₘ : m ≃ m')
(eₙ : n ≃ n') :
The natural map that reindexes a matrix's rows and columns with equivalent types,
matrix.reindex, is a linear equivalence.
Equations
- matrix.reindex_linear_equiv eₘ eₙ = {to_fun := (matrix.reindex eₘ eₙ).to_fun, map_add' := _, map_smul' := _, inv_fun := (matrix.reindex eₘ eₙ).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
matrix.reindex_linear_equiv_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{m' : Type u_5}
{n' : Type u_6}
[fintype m']
[fintype n']
{R : Type v}
[semiring R]
(eₘ : m ≃ m')
(eₙ : n ≃ n')
(M : matrix m n R) :
⇑(matrix.reindex_linear_equiv eₘ eₙ) M = ⇑(matrix.reindex eₘ eₙ) M
@[simp]
theorem
matrix.reindex_linear_equiv_symm
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{m' : Type u_5}
{n' : Type u_6}
[fintype m']
[fintype n']
{R : Type v}
[semiring R]
(eₘ : m ≃ m')
(eₙ : n ≃ n') :
(matrix.reindex_linear_equiv eₘ eₙ).symm = matrix.reindex_linear_equiv eₘ.symm eₙ.symm
@[simp]
theorem
matrix.reindex_linear_equiv_refl_refl
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[semiring R] :
matrix.reindex_linear_equiv (equiv.refl m) (equiv.refl n) = linear_equiv.refl R (matrix m n R)
def
matrix.reindex_alg_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_semiring R]
[decidable_eq m]
[decidable_eq n]
(e : m ≃ n) :
For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent
types, matrix.reindex, is an equivalence of algebras.
Equations
- matrix.reindex_alg_equiv e = {to_fun := ⇑(matrix.reindex e e), inv_fun := (matrix.reindex_linear_equiv e e).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
theorem
matrix.reindex_alg_equiv_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_semiring R]
[decidable_eq m]
[decidable_eq n]
(e : m ≃ n)
(M : matrix m m R) :
⇑(matrix.reindex_alg_equiv e) M = ⇑(matrix.reindex e e) M
@[simp]
theorem
matrix.reindex_alg_equiv_symm
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[comm_semiring R]
[decidable_eq m]
[decidable_eq n]
(e : m ≃ n) :
@[simp]
theorem
matrix.reindex_alg_equiv_refl
{m : Type u_2}
[fintype m]
{R : Type v}
[comm_semiring R]
[decidable_eq m] :
theorem
matrix.det_reindex_linear_equiv_self
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[decidable_eq m]
[decidable_eq n]
[comm_ring R]
(e : m ≃ n)
(A : matrix m m R) :
(⇑(matrix.reindex_linear_equiv e e) A).det = A.det
Reindexing both indices along the same equivalence preserves the determinant.
For the simp version of this lemma, see det_minor_equiv_self.
theorem
matrix.det_reindex_alg_equiv
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{R : Type v}
[decidable_eq m]
[decidable_eq n]
[comm_ring R]
(e : m ≃ n)
(A : matrix m m R) :
(⇑(matrix.reindex_alg_equiv e) A).det = A.det
Reindexing both indices along the same equivalence preserves the determinant.
For the simp version of this lemma, see det_minor_equiv_self.
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
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}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(c : basis m S T)
(x : T)
(i j k k' : m) :
⇑(algebra.left_mul_matrix (b.smul c)) x (i, k) (j, k') = ⇑(algebra.left_mul_matrix b) (⇑(algebra.left_mul_matrix c) x k k') i j
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}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(c : basis m S T)
(x : S) :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) = matrix.block_diagonal (λ (k : m), ⇑(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}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(c : basis m S T)
(x : S)
(i j k : m) :
⇑(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}
[fintype m]
[decidable_eq m]
(b : basis m R S)
(c : basis m S T)
(x : S)
(i j : m)
{k k' : m}
(h : k ≠ k') :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) (i, k) (j, k') = 0
def
linear_map.trace_aux
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M) :
The trace of an endomorphism given a basis.
Equations
- linear_map.trace_aux R b = (matrix.trace ι R R).comp ↑(linear_map.to_matrix b b)
theorem
linear_map.trace_aux_def
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(f : M →ₗ[R] M) :
⇑(linear_map.trace_aux R b) f = ⇑(matrix.trace ι R R) (⇑(linear_map.to_matrix b b) f)
theorem
linear_map.trace_aux_eq
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
{κ : Type u_1}
[decidable_eq κ]
[fintype κ]
(b : basis ι R M)
(c : basis κ R M) :
theorem
linear_map.trace_aux_reindex_range
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
[nontrivial R] :
Trace of an endomorphism independent of basis.
theorem
linear_map.trace_eq_matrix_trace_of_finite_set
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{s : set M}
(b : basis ↥s R M)
(hs : fintype ↥s)
(f : M →ₗ[R] M) :
⇑(linear_map.trace R M) f = ⇑(matrix.trace ↥s R R) (⇑(linear_map.to_matrix b b) f)
Auxiliary lemma for trace_eq_matrix_trace.
theorem
linear_map.trace_eq_matrix_trace
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
{ι : Type w}
[decidable_eq ι]
[fintype ι]
(b : basis ι R M)
(f : M →ₗ[R] M) :
⇑(linear_map.trace R M) f = ⇑(matrix.trace ι R R) (⇑(linear_map.to_matrix b b) f)
theorem
linear_map.trace_mul_comm
(R : Type u)
[comm_ring R]
{M : Type v}
[add_comm_group M]
[module R M]
(f g : M →ₗ[R] M) :
⇑(linear_map.trace R M) (f * g) = ⇑(linear_map.trace R M) (g * f)
@[protected, instance]
def
linear_map.finite_dimensional
{K : Type u_2}
[field K]
{V : Type u_3}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_4}
[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_2}
[field K]
{V : Type u_3}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_4}
[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}
[fintype n]
[decidable_eq 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_1}
{M₂ : Type (max u_2 u_3)}
[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.
def
alg_equiv_matrix
{R : Type v}
{M : Type w}
{n : Type u_1}
[fintype n]
[comm_ring R]
[add_comm_group M]
[module R M]
[decidable_eq 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.
Equations
@[simp]
theorem
matrix.dot_product_std_basis_eq_mul
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
[decidable_eq n]
(v : n → R)
(c : R)
(i : n) :
matrix.dot_product v (⇑(linear_map.std_basis R (λ (_x : n), R) i) c) = (v i) * c
@[simp]
theorem
matrix.dot_product_std_basis_one
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
[decidable_eq n]
(v : n → R)
(i : n) :
matrix.dot_product v (⇑(linear_map.std_basis R (λ (_x : n), R) i) 1) = v i
theorem
matrix.dot_product_eq
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
(v w : n → R)
(h : ∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) :
v = w
theorem
matrix.dot_product_eq_iff
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
{v w : n → R} :
(∀ (u : n → R), matrix.dot_product v u = matrix.dot_product w u) ↔ v = w
theorem
matrix.dot_product_eq_zero
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
(v : n → R)
(h : ∀ (w : n → R), matrix.dot_product v w = 0) :
v = 0
theorem
matrix.dot_product_eq_zero_iff
{R : Type v}
[semiring R]
{n : Type w}
[fintype n]
{v : n → R} :
(∀ (w : n → R), matrix.dot_product v w = 0) ↔ v = 0
theorem
matrix.det_to_block
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
(p : m → Prop)
[decidable_pred p] :
theorem
matrix.det_to_square_block
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
{n : ℕ}
(b : m → fin n)
(k : fin n) :
(M.to_square_block b k).det = (M.to_square_block_prop (λ (i : m), b i = k)).det
theorem
matrix.det_to_square_block'
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
(b : m → ℕ)
(k : ℕ) :
(M.to_square_block' b k).det = (M.to_square_block_prop (λ (i : m), b i = k)).det
theorem
matrix.two_block_triangular_det
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
(p : m → Prop)
[decidable_pred p]
(h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0) :
M.det = ((M.to_square_block_prop p).det) * (M.to_square_block_prop (λ (i : m), ¬p i)).det
theorem
matrix.equiv_block_det
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
{p q : m → Prop}
[decidable_pred p]
[decidable_pred q]
(e : ∀ (x : m), q x ↔ p x) :
(M.to_square_block_prop p).det = (M.to_square_block_prop q).det
theorem
matrix.to_square_block_det''
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
{n : ℕ}
(b : m → fin n)
(k : fin n) :
(M.to_square_block b k).det = (M.to_square_block' (λ (i : m), ↑(b i)) ↑k).det
def
matrix.block_triangular_matrix'
{R : Type v}
[comm_ring R]
{o : Type u_1}
[fintype o]
(M : matrix o o R)
{n : ℕ}
(b : o → fin n) :
Prop
Let b map rows and columns of a square matrix M to n blocks. Then
block_triangular_matrix' M n b says the matrix is block triangular.
Equations
- M.block_triangular_matrix' b = ∀ (i j : o), b j < b i → M i j = 0
theorem
matrix.upper_two_block_triangular'
{R : Type v}
[comm_ring R]
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
(A : matrix m m R)
(B : matrix m n R)
(D : matrix n n R) :
(A.from_blocks B 0 D).block_triangular_matrix' (sum.elim (λ (i : m), 0) (λ (j : n), 1))
def
matrix.block_triangular_matrix
{R : Type v}
[comm_ring R]
{o : Type u_1}
[fintype o]
(M : matrix o o R)
(b : o → ℕ) :
Prop
Let b map rows and columns of a square matrix M to blocks indexed by ℕs. Then
block_triangular_matrix M n b says the matrix is block triangular.
Equations
- M.block_triangular_matrix b = ∀ (i j : o), b j < b i → M i j = 0
theorem
matrix.upper_two_block_triangular
{R : Type v}
[comm_ring R]
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
(A : matrix m m R)
(B : matrix m n R)
(D : matrix n n R) :
(A.from_blocks B 0 D).block_triangular_matrix (sum.elim (λ (i : m), 0) (λ (j : n), 1))
theorem
matrix.det_of_block_triangular_matrix
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
(b : m → ℕ)
(h : M.block_triangular_matrix b)
(n : ℕ)
(hn : ∀ (i : m), b i < n) :
M.det = ∏ (k : ℕ) in finset.range n, (M.to_square_block' b k).det
theorem
matrix.det_of_block_triangular_matrix''
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
(b : m → ℕ)
(h : M.block_triangular_matrix b) :
M.det = ∏ (k : ℕ) in finset.image b finset.univ, (M.to_square_block' b k).det
theorem
matrix.det_of_block_triangular_matrix'
{m : Type u_1}
[decidable_eq m]
[fintype m]
{R : Type v}
[comm_ring R]
(M : matrix m m R)
{n : ℕ}
(b : m → fin n)
(h : M.block_triangular_matrix' b) :
M.det = ∏ (k : fin n), (M.to_square_block b k).det