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.

Issues #

This file was originally written without attention to non-commutative rings, and so mostly only works in the commutative setting. This should be fixed.

In particular, matrix.mul_vec gives us a linear equivalence matrix m n R ≃ₗ[R] (n → R) →ₗ[Rᵐᵒᵖ] (m → R) while matrix.vec_mul gives us a linear equivalence matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] (n → R). At present, the first equivalence is developed in detail but only for commutative rings (and we omit the distinction between Rᵐᵒᵖ and R), while the second equivalence is developed only in brief, but for not-necessarily-commutative rings.

Naming is slightly inconsistent between the two developments. In the original (commutative) development linear is abbreviated to lin, although this is not consistent with the rest of mathlib. In the new (non-commutative) development linear is not abbreviated, and declarations use _right to indicate they use the right action of matrices on vectors (via matrix.vec_mul). When the two developments are made uniform, the names should be made uniform, too, by choosing between linear and lin consistently, and (presumably) adding _left where necessary.

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

matrix.vec_mul M is a linear map.

Equations
@[simp]
theorem matrix.vec_mul_linear_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] (M : matrix m n R) (x : m → R) (ᾰ : n) :
@[simp]
theorem matrix.vec_mul_std_basis {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] (M : matrix m n R) (i : m) (j : n) :
matrix.vec_mul ((linear_map.std_basis R (λ (_x : m), R) i) 1) M j = M i j
def linear_map.to_matrix_right' {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] :
((m → R) →ₗ[R] n → R) ≃ₗ[Rᵐᵒᵖ] matrix m n R

Linear maps (m → R) →ₗ[R] (n → R) are linearly equivalent over Rᵐᵒᵖ to matrix m n R, by having matrices act by right multiplication.

Equations
def matrix.to_linear_map_right' {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] :
matrix m n R ≃ₗ[Rᵐᵒᵖ] (m → R) →ₗ[R] n → R

A matrix m n R is linearly equivalent over Rᵐᵒᵖ to a linear map (m → R) →ₗ[R] (n → R), by having matrices act by right multiplication.

@[simp]
theorem matrix.to_linear_map_right'_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] (M : matrix m n R) (v : m → R) :
@[simp]
theorem matrix.to_linear_map_right'_mul {R : Type u_1} [semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype l] [decidable_eq l] (M : matrix l m R) (N : matrix m n R) :
theorem matrix.to_linear_map_right'_mul_apply {R : Type u_1} [semiring R] {l : Type u_2} {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype l] [decidable_eq l] (M : matrix l m R) (N : matrix m n R) (x : l → R) :
@[simp]
@[simp]
theorem matrix.to_linear_equiv_right'_of_inv_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {M : matrix m n R} {M' : matrix n m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : n → R) (ᾰ_1 : m) :
def matrix.to_linear_equiv_right'_of_inv {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {M : matrix m n R} {M' : matrix n m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) :
(n → R) ≃ₗ[R] m → R

If M and M' are each other's inverse matrices, they provide an equivalence between n → A and m → A corresponding to M.vec_mul and M'.vec_mul.

Equations
@[simp]
theorem matrix.to_linear_equiv_right'_of_inv_symm_apply {R : Type u_1} [semiring R] {m : Type u_3} {n : Type u_4} [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] {M : matrix m n R} {M' : matrix n m R} (hMM' : M.mul M' = 1) (hM'M : M'.mul M = 1) (ᾰ : m → R) (ᾰ_1 : n) :

From this point on, we only work with commutative rings, and fail to distinguish between Rᵐᵒᵖ and R. This should eventually be remedied.

def matrix.mul_vec_lin {R : Type u_1} [comm_semiring R] {m : Type u_3} {n : Type u_4} [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_semiring R] {m : Type u_3} {n : Type u_4} [fintype n] (M : matrix m n R) (v : n → R) (ᾰ : m) :
(M.mul_vec_lin) v = M.mul_vec v
@[simp]
theorem matrix.mul_vec_std_basis {R : Type u_1} [comm_semiring 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_semiring R] {m : Type u_3} {n : Type u_4} [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_semiring R] {m : Type u_3} {n : Type u_4} [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_semiring 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_semiring 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_semiring 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_semiring 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_semiring R] {m : Type u_3} {n : Type u_4} [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_semiring R] {m : Type u_3} {n : Type u_4} [fintype n] [decidable_eq n] (M : matrix m n R) (v : n → R) :
@[simp]
theorem matrix.to_lin'_one {R : Type u_1} [comm_semiring R] {n : Type u_4} [fintype n] [decidable_eq n] :
@[simp]
theorem linear_map.to_matrix'_id {R : Type u_1} [comm_semiring R] {n : Type u_4} [fintype n] [decidable_eq n] :
@[simp]
theorem matrix.to_lin'_mul {R : Type u_1} [comm_semiring 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) :
theorem matrix.to_lin'_mul_apply {R : Type u_1} [comm_semiring 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) :

Shortcut lemma for matrix.to_lin'_mul and linear_map.comp_apply

theorem linear_map.to_matrix'_comp {R : Type u_1} [comm_semiring 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_semiring 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_semiring R] {n : Type u_4} [fintype n] [decidable_eq n] (x : R) :
theorem matrix.ker_to_lin'_eq_bot_iff {R : Type u_1} [comm_semiring R] {n : Type u_4} [fintype n] [decidable_eq n] {M : matrix n n R} :
(matrix.to_lin' M).ker = ∀ (v : n → R), M.mul_vec v = 0v = 0
@[simp]
theorem matrix.to_lin'_of_inv_symm_apply {R : Type u_1} [comm_semiring 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.mul M' = 1) (hM'M : M'.mul 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_semiring 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.mul M' = 1) (hM'M : M'.mul 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_semiring 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.mul M' = 1) (hM'M : M'.mul 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_semiring 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_semiring 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_semiring 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_semiring 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 n] [decidable_eq n] (w : m → K) (v : n → K) :
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₂) :
(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

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₂) :
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
theorem matrix.to_lin_eq_to_lin' {R : Type u_1} [comm_ring R] {m : Type u_3} {n : Type u_4} [fintype n] [fintype m] [decidable_eq n] :

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₂) :
@[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₂) :
@[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) :
(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 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) :
((linear_map.to_matrix v₁ v₂) f).transpose 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 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) :
(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 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) :
((linear_map.to_matrix v₁ v₂) f).transpose 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 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₁) :
((matrix.to_lin v₁ v₂) M) v = finset.univ.sum (λ (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 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) :
((matrix.to_lin v₁ v₂) M) (v₁ i) = finset.univ.sum (λ (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 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).mul ((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).mul ((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) :
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₁) :
((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 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.mul 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.mul 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.mul M' = 1) (hM'M : M'.mul 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.mul M' = 1) (hM'M : M'.mul 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 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.mul M' = 1) (hM'M : M'.mul 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₁) :
(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
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₁) :
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) :
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) :
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 = finset.univ.sum (λ (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) = finset.univ.sum (λ (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
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) :
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] [decidable_eq n] (b : basis m R S) (c : basis n S T) [fintype n] (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] [decidable_eq n] (b : basis m R S) (c : basis n S T) [fintype n] (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] [decidable_eq n] (b : basis m R S) (c : basis n S T) [fintype n] (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] [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] :
@[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] {A : Type u_4} [ring A] [algebra K A] [module A V] [is_scalar_tower K A V] [module A W] [is_scalar_tower K A W] :

Linear maps over a k-algebra are finite dimensional (over k) if both the source and target are, since they form a subspace of all k-linear maps.

@[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} [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
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₂) :

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

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

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

Equations