Linear maps and matrices #
This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.
Main definitions #
In the list below, and in all this file, R is a commutative ring (semiring
is sometimes enough), M and its variations are R-modules, ι, κ, n and m are finite
types used for indexing.
linear_map.to_matrix: given basesv₁ : ι → M₁andv₂ : κ → M₂, theR-linear equivalence fromM₁ →ₗ[R] M₂tomatrix κ ι Rmatrix.to_lin: the inverse oflinear_map.to_matrixlinear_map.to_matrix': theR-linear equivalence from(m → R) →ₗ[R] (n → R)tomatrix m n R(with the standard basis onm → Randn → 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
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] :
Equations
- matrix.fintype R = _.mpr pi.fintype
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) :
matrix.vec_mul M is a linear map.
Equations
- M.vec_mul_linear = {to_fun := λ (x : m → R), matrix.vec_mul x M, map_add' := _, map_smul' := _}
@[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) :
⇑(M.vec_mul_linear) x ᾰ = matrix.vec_mul x M ᾰ
@[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] :
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
- linear_map.to_matrix_right' = {to_fun := λ (f : (m → R) →ₗ[R] n → R) (i : m) (j : n), ⇑f (⇑(linear_map.std_basis R (λ (_x : m), R) i) 1) j, map_add' := _, map_smul' := _, inv_fun := matrix.vec_mul_linear _inst_2, left_inv := _, right_inv := _}
@[reducible]
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] :
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) :
⇑(⇑matrix.to_linear_map_right' M) v = matrix.vec_mul v M
@[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) :
⇑(⇑matrix.to_linear_map_right' (M.mul N)) x = ⇑(⇑matrix.to_linear_map_right' N) (⇑(⇑matrix.to_linear_map_right' M) x)
@[simp]
theorem
matrix.to_linear_map_right'_one
{R : Type u_1}
[semiring R]
{m : Type u_3}
[fintype m]
[decidable_eq m] :
@[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) :
⇑(matrix.to_linear_equiv_right'_of_inv hMM' hM'M) ᾰ ᾰ_1 = ⇑(⇑matrix.to_linear_map_right' M') ᾰ ᾰ_1
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) :
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
- matrix.to_linear_equiv_right'_of_inv hMM' hM'M = {to_fun := ⇑(⇑matrix.to_linear_map_right' M'), map_add' := _, map_smul' := _, inv_fun := ⇑(⇑matrix.to_linear_map_right' M), left_inv := _, right_inv := _}
@[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) :
⇑((matrix.to_linear_equiv_right'_of_inv hMM' hM'M).symm) ᾰ ᾰ_1 = ⇑(⇑matrix.to_linear_map_right' M) ᾰ ᾰ_1
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) :
matrix.mul_vec M is a linear map.
@[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 ᾰ
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
@[simp]
theorem
matrix.mul_vec_std_basis_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)
(j : n) :
M.mul_vec (⇑(linear_map.std_basis R (λ (_x : n), R) j) 1) = M.transpose 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] :
Linear maps (n → R) →ₗ[R] (m → R) are linearly equivalent to matrix m n R.
def
matrix.to_lin'
{R : Type u_1}
[comm_semiring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[decidable_eq n] :
A matrix m n R is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R).
Equations
@[simp]
theorem
linear_map.to_matrix'_symm
{R : Type u_1}
[comm_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) :
@[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) :
⇑(⇑matrix.to_lin' M) v = M.mul_vec v
@[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) :
⇑matrix.to_lin' (M.mul N) = (⇑matrix.to_lin' M).comp (⇑matrix.to_lin' N)
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) :
⇑(⇑matrix.to_lin' (M.mul N)) x = ⇑(⇑matrix.to_lin' M) (⇑(⇑matrix.to_lin' N) x)
Shortcut lemma for matrix.to_lin'_mul and linear_map.comp_apply
theorem
linear_map.to_matrix'_comp
{R : Type u_1}
[comm_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) :
⇑linear_map.to_matrix' (f.comp g) = (⇑linear_map.to_matrix' f).mul (⇑linear_map.to_matrix' g)
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) :
⇑linear_map.to_matrix' (f * g) = (⇑linear_map.to_matrix' f).mul (⇑linear_map.to_matrix' g)
@[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) :
⇑linear_map.to_matrix' (⇑(algebra_map R (module.End R (n → R))) x) = ⇑(matrix.scalar n) x
theorem
matrix.ker_to_lin'_eq_bot_iff
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M : matrix n n R} :
linear_map.ker (⇑matrix.to_lin' M) = ⊥ ↔ ∀ (v : n → R), M.mul_vec v = 0 → v = 0
theorem
matrix.range_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'_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) :
If M and M' are each other's inverse matrices, they provide an equivalence between m → A
and n → A corresponding to M.mul_vec and M'.mul_vec.
Equations
- matrix.to_lin'_of_inv hMM' hM'M = {to_fun := ⇑(⇑matrix.to_lin' M'), map_add' := _, map_smul' := _, inv_fun := ⇑(⇑matrix.to_lin' M), left_inv := _, right_inv := _}
@[simp]
theorem
matrix.to_lin'_of_inv_apply
{R : Type u_1}
[comm_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] :
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_semiring 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_lin_alg_equiv'_symm
{R : Type u_1}
[comm_semiring 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_semiring 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_semiring 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_semiring 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_semiring 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
linear_map.to_matrix_alg_equiv'_id
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
@[simp]
theorem
matrix.to_lin_alg_equiv'_mul
{R : Type u_1}
[comm_semiring 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_semiring 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
(f g : (n → R) →ₗ[R] n → R) :
theorem
matrix.rank_vec_mul_vec
{K m n : Type u}
[field K]
[fintype n]
[decidable_eq n]
(w : m → K)
(v : n → K) :
rank (⇑matrix.to_lin' (matrix.vec_mul_vec w v)) ≤ 1
noncomputable
def
linear_map.to_matrix
{R : Type u_1}
[comm_semiring 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_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂) :
Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear
equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.
Equations
- linear_map.to_matrix v₁ v₂ = (v₁.equiv_fun.arrow_congr v₂.equiv_fun).trans linear_map.to_matrix'
theorem
linear_map.to_matrix_eq_to_matrix'
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n] :
linear_map.to_matrix' is a particular case of linear_map.to_matrix, for the standard basis
pi.basis_fun R n.
noncomputable
def
matrix.to_lin
{R : Type u_1}
[comm_semiring 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_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂) :
Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear
equivalence between matrices over R indexed by the bases and linear maps M₁ →ₗ M₂.
Equations
- matrix.to_lin v₁ v₂ = (linear_map.to_matrix v₁ v₂).symm
theorem
matrix.to_lin_eq_to_lin'
{R : Type u_1}
[comm_semiring R]
{m : Type u_3}
{n : Type u_4}
[fintype n]
[fintype m]
[decidable_eq n] :
matrix.to_lin (pi.basis_fun R n) (pi.basis_fun R m) = matrix.to_lin'
matrix.to_lin' is a particular case of matrix.to_lin, for the standard basis
pi.basis_fun R n.
@[simp]
theorem
linear_map.to_matrix_symm
{R : Type u_1}
[comm_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
{M₃ : Type u_7}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁)
(x : R) :
⇑(linear_map.to_matrix v₁ v₁) (⇑(algebra_map R (module.End R M₁)) x) = ⇑(matrix.scalar n) x
theorem
linear_map.to_matrix_mul_vec_repr
{R : Type u_1}
[comm_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
{M₃ : Type u_7}
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid M₂]
[module R M₁]
[module R M₂]
(v₁ : basis n R M₁)
(v₂ : basis m R M₂)
{M₃ : Type u_7}
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring 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_monoid M₁]
[add_comm_monoid 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) :
If M and M are each other's inverse matrices, matrix.to_lin M and matrix.to_lin M'
form a linear equivalence.
Equations
- matrix.to_lin_of_inv v₁ v₂ hMM' hM'M = {to_fun := ⇑(⇑(matrix.to_lin v₁ v₂) M), map_add' := _, map_smul' := _, inv_fun := ⇑(⇑(matrix.to_lin v₂ v₁) M'), left_inv := _, right_inv := _}
@[simp]
theorem
matrix.to_lin_of_inv_apply
{R : Type u_1}
[comm_semiring 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_monoid M₁]
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁) :
Given a basis of a module M₁ over a commutative ring R, we get an algebra
equivalence between linear maps M₁ →ₗ M₁ and square matrices over R indexed by the basis.
Equations
noncomputable
def
matrix.to_lin_alg_equiv
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁) :
@[simp]
theorem
matrix.to_lin_alg_equiv_symm
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁) :
@[simp]
theorem
matrix.to_lin_alg_equiv_one
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁) :
theorem
linear_map.to_matrix_alg_equiv_reindex_range
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁)
[decidable_eq M₁]
(f : M₁ →ₗ[R] M₁)
(k i : n) :
⇑(linear_map.to_matrix_alg_equiv v₁.reindex_range) f ⟨⇑v₁ k, _⟩ ⟨⇑v₁ i, _⟩ = ⇑(linear_map.to_matrix_alg_equiv v₁) f k i
theorem
linear_map.to_matrix_alg_equiv_comp
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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).mul (⇑(linear_map.to_matrix_alg_equiv v₁) g)
theorem
linear_map.to_matrix_alg_equiv_mul
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid 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).mul (⇑(linear_map.to_matrix_alg_equiv v₁) g)
theorem
matrix.to_lin_alg_equiv_mul
{R : Type u_1}
[comm_semiring R]
{n : Type u_4}
[fintype n]
[decidable_eq n]
{M₁ : Type u_5}
[add_comm_monoid M₁]
[module R M₁]
(v₁ : basis n R M₁)
(A B : matrix n n R) :
⇑(matrix.to_lin_alg_equiv v₁) (A.mul B) = (⇑(matrix.to_lin_alg_equiv v₁) A).comp (⇑(matrix.to_lin_alg_equiv v₁) B)
@[simp]
theorem
matrix.to_lin_fin_two_prod_apply
{R : Type u_1}
[comm_semiring R]
(a b c d : R)
(x : R × R) :
theorem
matrix.to_lin_fin_two_prod
{R : Type u_1}
[comm_semiring R]
(a b c d : R) :
⇑(matrix.to_lin (basis.fin_two_prod R) (basis.fin_two_prod R)) (⇑matrix.of ![![a, b], ![c, d]]) = (a • linear_map.fst R R R + b • linear_map.snd R R R).prod (c • linear_map.fst R R R + d • linear_map.snd R R 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) :
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 linear_map.mul_left,
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) (linear_map.mul_left R x) = ⇑(algebra.left_mul_matrix b) x
theorem
algebra.left_mul_matrix_injective
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[comm_ring S]
[algebra R S]
{m : Type u_4}
[fintype m]
[decidable_eq m]
(b : basis m R S) :
theorem
algebra.smul_left_mul_matrix
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : T)
(ik jk : m × n) :
⇑(algebra.left_mul_matrix (b.smul c)) x ik jk = ⇑(algebra.left_mul_matrix b) (⇑(algebra.left_mul_matrix c) x ik.snd jk.snd) ik.fst jk.fst
theorem
algebra.smul_left_mul_matrix_algebra_map
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : S) :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) = matrix.block_diagonal (λ (k : n), ⇑(algebra.left_mul_matrix b) x)
theorem
algebra.smul_left_mul_matrix_algebra_map_eq
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : S)
(i j : m)
(k : n) :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) (i, k) (j, k) = ⇑(algebra.left_mul_matrix b) x i j
theorem
algebra.smul_left_mul_matrix_algebra_map_ne
{R : Type u_1}
{S : Type u_2}
{T : Type u_3}
[comm_ring R]
[comm_ring S]
[comm_ring T]
[algebra R S]
[algebra S T]
[algebra R T]
[is_scalar_tower R S T]
{m : Type u_4}
{n : Type u_5}
[fintype m]
[decidable_eq m]
[decidable_eq n]
(b : basis m R S)
(c : basis n S T)
[fintype n]
(x : S)
(i j : m)
{k k' : n}
(h : k ≠ k') :
⇑(algebra.left_mul_matrix (b.smul c)) (⇑(algebra_map S T) x) (i, k) (j, k') = 0
@[protected, instance]
def
linear_map.finite_dimensional
{K : Type u_1}
[field K]
{V : Type u_2}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_3}
[add_comm_group W]
[module K W]
[finite_dimensional K W] :
finite_dimensional K (V →ₗ[K] W)
@[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] :
finite_dimensional K (V →ₗ[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]
theorem
linear_map.finrank_linear_map
{K : Type u_1}
[field K]
{V : Type u_2}
[add_comm_group V]
[module K V]
[finite_dimensional K V]
{W : Type u_3}
[add_comm_group W]
[module K W]
[finite_dimensional K W] :
finite_dimensional.finrank K (V →ₗ[K] W) = finite_dimensional.finrank K V * finite_dimensional.finrank K W
The dimension of the space of linear transformations is the product of the dimensions of the domain and codomain.
def
alg_equiv_matrix'
{R : Type v}
[comm_ring R]
{n : Type u_1}
[decidable_eq n]
[fintype n] :
module.End R (n → R) ≃ₐ[R] matrix n n R
The natural equivalence between linear endomorphisms of finite free modules and square matrices is compatible with the algebra structures.
Equations
- alg_equiv_matrix' = {to_fun := linear_map.to_matrix'.to_fun, inv_fun := linear_map.to_matrix'.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
def
linear_equiv.alg_conj
{R : Type v}
[comm_ring R]
{M₁ : Type u_3}
{M₂ : Type u_4}
[add_comm_group M₁]
[module R M₁]
[add_comm_group M₂]
[module R M₂]
(e : M₁ ≃ₗ[R] M₂) :
module.End R M₁ ≃ₐ[R] module.End R M₂
A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.
noncomputable
def
alg_equiv_matrix
{R : Type v}
[comm_ring R]
{n : Type u_1}
[decidable_eq n]
{M : Type u_2}
[add_comm_group M]
[module R M]
[fintype n]
(h : basis n R M) :
module.End R M ≃ₐ[R] matrix n n R
A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.