Linear maps and matrices
This file defines the maps to send matrices to a linear map, and to send linear maps between modules with a finite bases to matrices. This defines a linear equivalence between linear maps between finite-dimensional vector spaces and matrices indexed by the respective bases.
It also defines the trace of an endomorphism, and the determinant of a family of vectors with respect to some basis.
Some results are proved about the linear map corresponding to a
diagonal matrix (range
, ker
and rank
).
Main definitions
In the list below, and in all this file, R
is a commutative ring (semiring
is sometimes enough), M
and its variations are R
-modules, ι
, κ
, n
and m
are finite
types used for indexing.
linear_map.to_matrix
: given basesv₁ : ι → M₁
andv₂ : κ → M₂
, theR
-linear equivalence fromM₁ →ₗ[R] M₂
tomatrix κ ι R
matrix.to_lin
: the inverse oflinear_map.to_matrix
linear_map.to_matrix'
: theR
-linear equivalence from(n → R) →ₗ[R] (m → R)
tomatrix n m R
(with the standard basis onn → R
andm → 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
matrix.trace
: the trace of a square matrixlinear_map.trace
: the trace of an endomorphismis_basis.to_matrix
: the matrix whose columns are a given family of vectors in a given basisis_basis.to_matrix_equiv
: given a basis, the linear equivalence between families of vectors and matrices arising fromis_basis.to_matrix
is_basis.det
: the determinant of a family of vectors with respect to a basis, as a multilinear map
Tags
linear_map, matrix, linear_equiv, diagonal, det, trace
Equations
- matrix.fintype R = _.mpr pi.fintype
Linear maps (n → R) →ₗ[R] (m → R)
are linearly equivalent to matrix m n R
.
Equations
- linear_map.to_matrix' = {to_fun := λ (f : (n → R) →ₗ[R] m → R) (i : m) (j : n), ⇑f (⇑(linear_map.std_basis R (λ (_x : n), R) j) 1) i, map_add' := _, map_smul' := _, inv_fun := matrix.mul_vec_lin _inst_4, left_inv := _, right_inv := _}
A matrix m n R
is linearly equivalent to a linear map (n → R) →ₗ[R] (m → R)
.
Equations
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 hv₁ hv₂ = (hv₁.equiv_fun.arrow_congr hv₂.equiv_fun).trans linear_map.to_matrix'
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 hv₁ hv₂ = (linear_map.to_matrix hv₁ hv₂).symm
From a basis e : ι → M
and a family of vectors v : ι' → M
, make the matrix whose columns
are the vectors v i
written in the basis e
.
From a basis e : ι → M
, build a linear equivalence between families of vectors v : ι → M
,
and matrices, making the matrix whose columns are the vectors v i
written in the basis e
.
Builds a linear equivalence from a linear map whose determinant in some bases is a unit.
The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.
The diagonal of a square matrix.
The trace of a square matrix.
Equations
- matrix.trace n R M = {to_fun := λ (A : matrix n n M), ∑ (i : n), ⇑(matrix.diag n R M) A i, map_add' := _, map_smul' := _}
An invertible matrix yields a linear equivalence from the free module to itself.
The dimension of the space of finite dimensional matrices is the product of the number of rows and columns.
The natural map that reindexes a matrix's rows and columns with equivalent types is a linear equivalence.
Equations
- matrix.reindex_linear_equiv eₘ eₙ = {to_fun := (matrix.reindex eₘ eₙ).to_fun, map_add' := _, map_smul' := _, inv_fun := (matrix.reindex eₘ eₙ).inv_fun, left_inv := _, right_inv := _}
For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence of algebras.
Equations
- matrix.reindex_alg_equiv e = {to_fun := (matrix.reindex_linear_equiv e e).to_fun, inv_fun := (matrix.reindex_linear_equiv e e).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
simp
version of det_reindex_self
det_reindex_self
is not a good simp lemma because reindex_apply
fires before.
So we have this lemma to continue from there.
Reindexing both indices along the same equivalence preserves the determinant.
For the simp
version of this lemma, see det_reindex_self'
.
Reindexing both indices along the same equivalence preserves the determinant.
For the simp
version of this lemma, see det_reindex_self'
.
Reindexing both indices along the same equivalence preserves the determinant.
For the simp
version of this lemma, see det_reindex_self'
.
The trace of an endomorphism given a basis.
Equations
- linear_map.trace_aux R hb = (matrix.trace ι R R).comp ↑(linear_map.to_matrix hb hb)
where ι
and κ
can reside in different universes
Trace of an endomorphism independent of basis.
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.