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 κ ι R
matrix.to_lin
: the inverse oflinear_map.to_matrix
linear_map.to_matrix'
: theR
-linear equivalence from(m → R) →ₗ[R] (n → R)
tomatrix m n R
(with the standard basis onm → R
andn → R
)matrix.to_lin'
: the inverse oflinear_map.to_matrix'
alg_equiv_matrix
: given a basis indexed byn
, theR
-algebra equivalence betweenR
-endomorphisms ofM
andmatrix 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
Equations
- matrix.fintype R = _.mpr pi.fintype
Linear maps (m → R) →ₗ[R] (n → R)
are linearly equivalent over Rᵐᵒᵖ
to matrix m n R
,
by having matrices act by right multiplication.
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.
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 := _}
From this point on, we only work with commutative rings,
and fail to distinguish between Rᵐᵒᵖ
and R
.
This should eventually be remedied.
matrix.mul_vec M
is a linear map.
Linear maps (n → R) →ₗ[R] (m → R)
are linearly equivalent to matrix m n R
.
A matrix m n R
is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R)
.
Equations
Shortcut lemma for matrix.to_lin'_mul
and linear_map.comp_apply
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 := _}
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
A matrix n n R
is algebra equivalent to a linear map (n → R) →ₗ[R] (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 v₁ v₂ = (v₁.equiv_fun.arrow_congr v₂.equiv_fun).trans linear_map.to_matrix'
linear_map.to_matrix'
is a particular case of linear_map.to_matrix
, for the standard basis
pi.basis_fun R n
.
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
matrix.to_lin'
is a particular case of matrix.to_lin
, for the standard basis
pi.basis_fun R n
.
This will be a special case of linear_map.to_matrix_id_eq_basis_to_matrix
.
Shortcut lemma for matrix.to_lin_mul
and linear_map.comp_apply
.
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 := _}
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
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
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' := _}
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.
The dimension of the space of linear transformations is the product of the dimensions of the domain and codomain.
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' := _}
A linear equivalence of two modules induces an equivalence of algebras of their endomorphisms.
A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.