mathlib documentation

linear_algebra.matrix.to_lin

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.

Tags #

linear_map, matrix, linear_equiv, diagonal, det, trace

@[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] :
fintype (matrix m n R)
Equations
def matrix.mul_vec_lin {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] (M : matrix m n R) :
(n → R) →ₗ[R] m → R

matrix.mul_vec M is a linear map.

Equations
@[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) :
@[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] :
((n → R) →ₗ[R] m → R) ≃ₗ[R] matrix m n R

Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R.

Equations
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] :
matrix m n R ≃ₗ[R] (n → R) →ₗ[R] m → R

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) :
linear_map.to_matrix' f i j = f (λ (j' : n), ite (j' = j) 1 0) i
@[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) :
@[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) :
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 l] [fintype m] [fintype n] [decidable_eq n] [decidable_eq m] (M : matrix l m R) (N : matrix m n R) (x : n → R) :

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 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) :
@[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 m] [fintype n] [decidable_eq n] [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 m] [fintype n] [decidable_eq n] [decidable_eq m] {M : matrix m n R} {M' : matrix n m R} (hMM' : M M' = 1) (hM'M : M' M = 1) :
(m → R) ≃ₗ[R] n → R

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
@[simp]
theorem matrix.to_lin'_of_inv_apply {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype m] [fintype n] [decidable_eq n] [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] :
((n → R) →ₗ[R] n → R) ≃ₐ[R] matrix n n R

Linear maps (n → R) →ₗ[R] (n → R) are algebra equivalent to matrix n n R.

Equations
def matrix.to_lin_alg_equiv' {R : Type u_1} [comm_ring R] {n : Type u_4} [fintype n] [decidable_eq n] :
matrix n n R ≃ₐ[R] (n → R) →ₗ[R] n → R

A matrix n n R is algebra equivalent to a linear map (n → R) →ₗ[R] (n → R).

Equations
@[simp]
@[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) :
linear_map.to_matrix_alg_equiv' f i j = f (λ (j' : n), ite (j' = j) 1 0) i
@[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) :
@[simp]
theorem matrix.rank_vec_mul_vec {K m n : Type u} [field K] [fintype m] [fintype n] [decidable_eq n] (w : m → K) (v : n → K) :
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₂) :
(M₁ →ₗ[R] M₂) ≃ₗ[R] matrix m n R

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
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₂) :
matrix m n R ≃ₗ[R] 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
@[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₂) :
@[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₂) :
@[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) :
(linear_map.to_matrix v₁ v₂) f i j = ((v₂.repr) (f (v₁ j))) i
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) :
((linear_map.to_matrix v₁ v₂) f) j = ((v₂.repr) (f (v₁ j)))
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) :
(linear_map.to_matrix v₁ v₂) f i j = ((v₂.repr) (f (v₁ j))) i
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) :
((linear_map.to_matrix v₁ v₂) f) j = ((v₂.repr) (f (v₁ j)))
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₁) :
((matrix.to_lin v₁ v₂) M) v = ∑ (j : m), M.mul_vec ((v₁.repr) v) j v₂ j
@[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) :
((matrix.to_lin v₁ v₂) M) (v₁ i) = ∑ (j : m), M j i v₂ j
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₁) :

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₁) :
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₂) [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₂) :
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₁) :
((linear_map.to_matrix v₁ v₂) f).mul_vec ((v₁.repr) x) = ((v₂.repr) (f x))
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)
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 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) (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 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₂) [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')
def matrix.to_lin_of_inv {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₂) [decidable_eq m] {M : matrix m n R} {M' : matrix n m R} (hMM' : M M' = 1) (hM'M : M' M = 1) :
M₁ ≃ₗ[R] M₂

If M and M are each other's inverse matrices, matrix.to_lin M and matrix.to_lin M' form a linear equivalence.

Equations
@[simp]
theorem matrix.to_lin_of_inv_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₂) [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)
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₁) :
(M₁ →ₗ[R] M₁) ≃ₐ[R] matrix n n R

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₁) :
matrix n n R ≃ₐ[R] M₁ →ₗ[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₁) :
@[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) :
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) :
(linear_map.to_matrix_alg_equiv v₁) f i j = ((v₁.repr) (f (v₁ j))) i
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) :
((linear_map.to_matrix_alg_equiv v₁) f) j = ((v₁.repr) (f (v₁ j)))
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) :
(linear_map.to_matrix_alg_equiv v₁) f i j = ((v₁.repr) (f (v₁ j))) i
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) :
((linear_map.to_matrix_alg_equiv v₁) f) j = ((v₁.repr) (f (v₁ j)))
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₁) :
((matrix.to_lin_alg_equiv v₁) M) v = ∑ (j : n), M.mul_vec ((v₁.repr) v) j v₁ j
@[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) :
((matrix.to_lin_alg_equiv v₁) M) (v₁ i) = ∑ (j : n), M j i v₁ j
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) :
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₁) :
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₁) :
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) :
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) :
S →ₐ[R] matrix m m R

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
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) :
theorem algebra.left_mul_matrix_eq_repr_mul {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) :
(algebra.left_mul_matrix b) x i j = ((b.repr) (x * b j)) i
theorem algebra.left_mul_matrix_mul_vec_repr {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 y : S) :
@[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) :
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] [fintype n] [decidable_eq n] (b : basis m R S) (c : basis n S T) (x : T) (ik jk : m × n) :
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] [fintype n] [decidable_eq n] (b : basis m R S) (c : basis n S T) (x : S) :
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] [fintype n] [decidable_eq n] (b : basis m R S) (c : basis n S T) (x : S) (i j : m) (k : n) :
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] [fintype n] [decidable_eq n] (b : basis m R S) (c : basis n S T) (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
@[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] :
@[simp]

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

A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.

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

A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.

Equations