Matrices #
This file defines basic properties of matrices.
Matrices with rows indexed by m
, columns indexed by n
, and entries of type α
are represented
with Matrix m n α
. For the typical approach of counting rows and columns,
Matrix (Fin m) (Fin n) α
can be used.
Notation #
The locale Matrix
gives the following notation:
⬝ᵥ
forMatrix.dotProduct
ᵀ
forMatrix.transpose
ᴴ
forMatrix.conjTranspose
Implementation notes #
For convenience, Matrix m n α
is defined as m → n → α
, as this allows elements of the matrix
to be accessed with A i j
. However, it is not advisable to construct matrices using terms of the
form λ i j, _
or even (λ i j, _ : Matrix m n α)
, as these are not recognized by lean as having
the right type. Instead, Matrix.of
should be used.
TODO #
Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.
Cast a function into a matrix.
The two sides of the equivalence are definitionally equal types. We want to use an explicit cast
to distinguish the types because Matrix
has different instances to pi types (such as Pi.mul
,
which performs elementwise multiplication, vs Matrix.mul
).
If you are defining a matrix, in terms of its entries, use of (fun i j ↦ _)
. The
purpose of this approach is to ensure that terms of the form (fun i j ↦ _) * (fun i j ↦ _)
do not
appear, as the type of *
can be misleading.
Porting note: In Lean 3, it is also safe to use pattern matching in a definition as | i j := _
,
which can only be unfolded when fully-applied. leanprover/lean4#2042 means this does not
(currently) work in Lean 4.
Instances For
M.map f
is the matrix obtained by applying f
to each entry of the matrix M
.
This is available in bundled forms as:
AddMonoidHom.mapMatrix
LinearMap.mapMatrix
RingHom.mapMatrix
AlgHom.mapMatrix
Equiv.mapMatrix
AddEquiv.mapMatrix
LinearEquiv.mapMatrix
RingEquiv.mapMatrix
AlgEquiv.mapMatrix
Instances For
The conjugate transpose of a matrix defined in term of star
.
Instances For
Matrix.col u
is the column matrix whose entries are given by u
.
Instances For
Matrix.row u
is the row matrix whose entries are given by u
.
Instances For
simp-normal form pulls of
to the outside.
The scalar action via Mul.toSMul
is transformed by the same map as the elements
of the matrix, when f
preserves multiplication.
The scalar action via mul.toOppositeSMul
is transformed by the same map as the
elements of the matrix, when f
preserves multiplication.
diagonal d
is the square matrix such that (diagonal d) i i = d i
and (diagonal d) i j = 0
if i ≠ j
.
Note that bundled versions exist as:
Instances For
Matrix.diagonal
as an AddMonoidHom
.
Instances For
Matrix.diagonal
as a LinearMap
.
Instances For
The diagonal of a square matrix.
Instances For
Matrix.diag
as an AddMonoidHom
.
Instances For
Matrix.diag
as a LinearMap
.
Instances For
dotProduct v w
is the sum of the entrywise products v i * w i
Instances For
dotProduct v w
is the sum of the entrywise products v i * w i
Instances For
Permuting a vector on the left of a dot product can be transferred to the right.
Permuting a vector on the right of a dot product can be transferred to the left.
Permuting vectors on both sides of a dot product is a no-op.
M * N
is the usual product of matrices M
and N
, i.e. we have that
(M * N) i k
is the dot product of the i
-th row of M
by the k
-th column of N
.
This is currently only defined when m
is finite.
Left multiplication by a matrix, as an AddMonoidHom
from matrices to matrices.
Instances For
Right multiplication by a matrix, as an AddMonoidHom
from matrices to matrices.
Instances For
This instance enables use with smul_mul_assoc
.
This instance enables use with mul_smul_comm
.
Matrix.diagonal
as a RingHom
.
Instances For
The ring homomorphism α →+* Matrix n n α
sending a
to the diagonal matrix with a
on the diagonal.
Instances For
Matrix.diagonal
as an AlgHom
.
Instances For
Bundled versions of Matrix.map
#
The AddMonoidHom
between spaces of matrices induced by an AddMonoidHom
between their
coefficients. This is Matrix.map
as an AddMonoidHom
.
Instances For
The LinearMap
between spaces of matrices induced by a LinearMap
between their
coefficients. This is Matrix.map
as a LinearMap
.
Instances For
The LinearEquiv
between spaces of matrices induced by a LinearEquiv
between their
coefficients. This is Matrix.map
as a LinearEquiv
.
Instances For
The RingHom
between spaces of square matrices induced by a RingHom
between their
coefficients. This is Matrix.map
as a RingHom
.
Instances For
The RingEquiv
between spaces of square matrices induced by a RingEquiv
between their
coefficients. This is Matrix.map
as a RingEquiv
.
Instances For
The AlgHom
between spaces of square matrices induced by an AlgHom
between their
coefficients. This is Matrix.map
as an AlgHom
.
Instances For
The AlgEquiv
between spaces of square matrices induced by an AlgEquiv
between their
coefficients. This is Matrix.map
as an AlgEquiv
.
Instances For
mulVec M v
is the matrix-vector product of M
and v
, where v
is seen as a column matrix.
Put another way, mulVec M v
is the vector whose entries
are those of M * col v
(see col_mulVec
).
Instances For
vecMul v M
is the vector-matrix product of v
and M
, where v
is seen as a row matrix.
Put another way, vecMul v M
is the vector whose entries
are those of row v * M
(see row_vecMul
).
Instances For
Left multiplication by a matrix, as an AddMonoidHom
from vectors to vectors.
Instances For
Associate the dot product of mulVec
to the left.
Matrix.transpose
as a LinearMap
Instances For
Matrix.transpose
as a RingEquiv
to the opposite ring
Instances For
Matrix.transpose
as an AlgEquiv
to the opposite ring
Instances For
Tell simp
what the entries are in a conjugate transposed matrix.
Compare with mul_apply
, diagonal_apply_eq
, etc.
Note that StarModule
is quite a strong requirement; as such we also provide the following
variants which this lemma would not apply to:
When star x = x
on the coefficients (such as the real numbers) conjTranspose
and transpose
are the same operation.
Matrix.conjTranspose
as an AddEquiv
Instances For
Matrix.conjTranspose
as a LinearMap
Instances For
When α
has a star operation, square matrices Matrix n n α
have a star
operation equal to Matrix.conjTranspose
.
When α
is a *
-additive monoid, Matrix.star
is also a *
-additive monoid.
When α
is a *
-(semi)ring, Matrix.star
is also a *
-(semi)ring.
Given maps (r_reindex : l → m)
and (c_reindex : o → n)
reindexing the rows and columns of
a matrix M : Matrix m n α
, the matrix M.submatrix r_reindex c_reindex : Matrix l o α
is defined
by (M.submatrix r_reindex c_reindex) i j = M (r_reindex i) (c_reindex j)
for (i,j) : l × o
.
Note that the total number of row and columns does not have to be preserved.
Instances For
Given a (m × m)
diagonal matrix defined by a map d : m → α
, if the reindexing map e
is
injective, then the resulting matrix is again diagonal.