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.mulVec
ᵥ*
forMatrix.vecMul
ᵀ
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 fun i j ↦ _
or even (fun 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.
Equations
- Matrix.of = Equiv.refl (m → n → α)
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
Equations
- M.map f = Matrix.of fun (i : m) (j : n) => f (M i j)
Instances For
The transpose of a matrix.
Equations
- Matrix.«term_ᵀ» = Lean.ParserDescr.trailingNode `Matrix.term_ᵀ 1024 1024 (Lean.ParserDescr.symbol "ᵀ")
Instances For
The conjugate transpose of a matrix defined in term of star
.
Equations
- Matrix.«term_ᴴ» = Lean.ParserDescr.trailingNode `Matrix.term_ᴴ 1024 1024 (Lean.ParserDescr.symbol "ᴴ")
Instances For
Equations
- Matrix.decidableEq = Fintype.decidablePiFintype
Equations
- Matrix.instFintypeOfDecidableEq α = inferInstanceAs (Fintype (m → n → α))
Equations
- Matrix.addSemigroup = Pi.addSemigroup
Equations
- Matrix.addCommSemigroup = Pi.addCommSemigroup
Equations
- Matrix.addZeroClass = Pi.addZeroClass
Equations
- Matrix.addCommMonoid = Pi.addCommMonoid
Equations
- Matrix.addCommGroup = Pi.addCommGroup
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- Matrix.distribMulAction = Pi.distribMulAction R
simp-normal form pulls of
to the outside.
The scalar action via mul.toOppositeSMul
is transformed by the same map as the
elements of the matrix, when f
preserves multiplication.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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:
Equations
- Matrix.diagonal d = Matrix.of fun (i j : n) => if i = j then d i else 0
Instances For
Equations
- Matrix.instNatCastOfZero = { natCast := fun (m : ℕ) => Matrix.diagonal fun (x : n) => ↑m }
Equations
- Matrix.instIntCastOfZero = { intCast := fun (m : ℤ) => Matrix.diagonal fun (x : n) => ↑m }
Matrix.diagonal
as an AddMonoidHom
.
Equations
- Matrix.diagonalAddMonoidHom n α = { toFun := Matrix.diagonal, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Matrix.diagonal
as a LinearMap
.
Equations
- Matrix.diagonalLinearMap n R α = { toFun := (↑(Matrix.diagonalAddMonoidHom n α)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Equations
- Matrix.one = { one := Matrix.diagonal fun (x : n) => 1 }
Equations
- Matrix.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯
Equations
- Matrix.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Equations
- Matrix.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯
Equations
- Matrix.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯
Matrix.diag
as an AddMonoidHom
.
Equations
- Matrix.diagAddMonoidHom n α = { toFun := Matrix.diag, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Matrix.diag
as a LinearMap
.
Equations
- Matrix.diagLinearMap n R α = { toFun := (↑(Matrix.diagAddMonoidHom n α)).toFun, map_add' := ⋯, map_smul' := ⋯ }
Instances For
dotProduct v w
is the sum of the entrywise products v i * w i
Equations
- Matrix.dotProduct v w = ∑ i : m, v i * w i
Instances For
dotProduct v w
is the sum of the entrywise products v i * w i
Equations
- Matrix.«term_⬝ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.term_⬝ᵥ_ 72 72 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⬝ᵥ ") (Lean.ParserDescr.cat `term 73))
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.
Equations
- Matrix.instHMulOfFintypeOfMulOfAddCommMonoid = { hMul := fun (M : Matrix l m α) (N : Matrix m n α) (i : l) (k : n) => Matrix.dotProduct (fun (j : m) => M i j) fun (j : m) => N j k }
Equations
- Matrix.nonUnitalNonAssocSemiring = NonUnitalNonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Left multiplication by a matrix, as an AddMonoidHom
from matrices to matrices.
Equations
Instances For
Right multiplication by a matrix, as an AddMonoidHom
from matrices to matrices.
Equations
Instances For
This instance enables use with smul_mul_assoc
.
Equations
- ⋯ = ⋯
This instance enables use with mul_smul_comm
.
Equations
- ⋯ = ⋯
Equations
- Matrix.nonAssocSemiring = NonAssocSemiring.mk ⋯ ⋯ ⋯ ⋯
Matrix.diagonal
as a RingHom
.
Equations
- Matrix.diagonalRingHom n α = { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Equations
- Matrix.nonUnitalSemiring = NonUnitalSemiring.mk ⋯
Equations
- Matrix.semiring = Semiring.mk ⋯ ⋯ ⋯ ⋯ npowRec ⋯ ⋯
Equations
- Matrix.nonUnitalNonAssocRing = NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
Equations
- Matrix.instNonUnitalRing = NonUnitalRing.mk ⋯
Equations
- Matrix.instNonAssocRing = NonAssocRing.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
The ring homomorphism α →+* Matrix n n α
sending a
to the diagonal matrix with a
on the diagonal.
Equations
- Matrix.scalar n = (Matrix.diagonalRingHom n α).comp (Pi.constRingHom n α)
Instances For
Equations
- Matrix.instAlgebra = Algebra.mk ((Matrix.scalar n).comp (algebraMap R α)) ⋯ ⋯
Matrix.diagonal
as an AlgHom
.
Equations
- Matrix.diagonalAlgHom R = { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
Instances For
Bundled versions of Matrix.map
#
The Equiv
between spaces of matrices induced by an Equiv
between their
coefficients. This is Matrix.map
as an Equiv
.
Equations
Instances For
The AddMonoidHom
between spaces of matrices induced by an AddMonoidHom
between their
coefficients. This is Matrix.map
as an AddMonoidHom
.
Equations
Instances For
The LinearMap
between spaces of matrices induced by a LinearMap
between their
coefficients. This is Matrix.map
as a LinearMap
.
Equations
Instances For
The LinearEquiv
between spaces of matrices induced by a LinearEquiv
between their
coefficients. This is Matrix.map
as a LinearEquiv
.
Equations
Instances For
The RingHom
between spaces of square matrices induced by a RingHom
between their
coefficients. This is Matrix.map
as a RingHom
.
Equations
Instances For
The RingEquiv
between spaces of square matrices induced by a RingEquiv
between their
coefficients. This is Matrix.map
as a RingEquiv
.
Equations
Instances For
The AlgHom
between spaces of square matrices induced by an AlgHom
between their
coefficients. This is Matrix.map
as an AlgHom
.
Equations
Instances For
The AlgEquiv
between spaces of square matrices induced by an AlgEquiv
between their
coefficients. This is Matrix.map
as an AlgEquiv
.
Equations
Instances For
For two vectors w
and v
, vecMulVec w v i j
is defined to be w i * v j
.
Put another way, vecMulVec w v
is exactly col w * row v
.
Equations
- Matrix.vecMulVec w v = Matrix.of fun (x : m) (y : n) => w x * v y
Instances For
M *ᵥ v
(notation for mulVec M v
) is the matrix-vector product of matrix M
and vector v
,
where v
is seen as a column vector.
Put another way, M *ᵥ v
is the vector whose entries are those of M * col v
(see col_mulVec
).
The notation has precedence 73, which comes immediately before ⬝ᵥ
for Matrix.dotProduct
,
so that A *ᵥ v ⬝ᵥ B *ᵥ w
is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w)
.
Equations
- M.mulVec v x = Matrix.dotProduct (fun (j : n) => M x j) v
Instances For
M *ᵥ v
(notation for mulVec M v
) is the matrix-vector product of matrix M
and vector v
,
where v
is seen as a column vector.
Put another way, M *ᵥ v
is the vector whose entries are those of M * col v
(see col_mulVec
).
The notation has precedence 73, which comes immediately before ⬝ᵥ
for Matrix.dotProduct
,
so that A *ᵥ v ⬝ᵥ B *ᵥ w
is parsed as (A *ᵥ v) ⬝ᵥ (B *ᵥ w)
.
Equations
- Matrix.«term_*ᵥ_» = Lean.ParserDescr.trailingNode `Matrix.term_*ᵥ_ 73 74 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *ᵥ ") (Lean.ParserDescr.cat `term 73))
Instances For
v ᵥ* M
(notation for vecMul v M
) is the vector-matrix product of vector v
and matrix M
,
where v
is seen as a row vector.
Put another way, v ᵥ* M
is the vector whose entries are those of row v * M
(see row_vecMul
).
The notation has precedence 73, which comes immediately before ⬝ᵥ
for Matrix.dotProduct
,
so that v ᵥ* A ⬝ᵥ w ᵥ* B
is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B)
.
Equations
- Matrix.vecMul v M x = Matrix.dotProduct v fun (i : m) => M i x
Instances For
v ᵥ* M
(notation for vecMul v M
) is the vector-matrix product of vector v
and matrix M
,
where v
is seen as a row vector.
Put another way, v ᵥ* M
is the vector whose entries are those of row v * M
(see row_vecMul
).
The notation has precedence 73, which comes immediately before ⬝ᵥ
for Matrix.dotProduct
,
so that v ᵥ* A ⬝ᵥ w ᵥ* B
is parsed as (v ᵥ* A) ⬝ᵥ (w ᵥ* B)
.
Equations
- Matrix.«term_ᵥ*_» = Lean.ParserDescr.trailingNode `Matrix.term_ᵥ*_ 73 73 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ᵥ* ") (Lean.ParserDescr.cat `term 74))
Instances For
Left multiplication by a matrix, as an AddMonoidHom
from vectors to vectors.
Equations
- Matrix.mulVec.addMonoidHomLeft v = { toFun := fun (M : Matrix m n α) => M.mulVec v, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The i
th row of the multiplication is the same as the vecMul
with the i
th row of A
.
Associate the dot product of mulVec
to the left.
Matrix.transpose
as an AddEquiv
Equations
- Matrix.transposeAddEquiv m n α = { toFun := Matrix.transpose, invFun := Matrix.transpose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
Matrix.transpose
as a LinearMap
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matrix.transpose
as a RingEquiv
to the opposite ring
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matrix.transpose
as an AlgEquiv
to the opposite ring
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Equations
- Matrix.conjTransposeAddEquiv m n α = { toFun := Matrix.conjTranspose, invFun := Matrix.conjTranspose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
Instances For
Matrix.conjTranspose
as a LinearMap
Equations
- One or more equations did not get rendered due to their size.
Instances For
When α
has a star operation, square matrices Matrix n n α
have a star
operation equal to Matrix.conjTranspose
.
Equations
- Matrix.instStar = { star := Matrix.conjTranspose }
Equations
- Matrix.instInvolutiveStar = InvolutiveStar.mk ⋯
When α
is a *
-additive monoid, Matrix.star
is also a *
-additive monoid.
Equations
- Matrix.instStarAddMonoid = StarAddMonoid.mk ⋯
Equations
- ⋯ = ⋯
When α
is a *
-(semi)ring, Matrix.star
is also a *
-(semi)ring.
Equations
- Matrix.instStarRing = StarRing.mk ⋯
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.
Equations
- A.submatrix r_reindex c_reindex = Matrix.of fun (i : l) (j : o) => A (r_reindex i) (c_reindex j)
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.
simp
lemmas for Matrix.submatrix
s interaction with Matrix.diagonal
, 1
, and Matrix.mul
for when the mappings are bundled.
The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.
Equations
- Matrix.reindex eₘ eₙ = { toFun := fun (M : Matrix m n α) => M.submatrix ⇑eₘ.symm ⇑eₙ.symm, invFun := fun (M : Matrix l o α) => M.submatrix ⇑eₘ ⇑eₙ, left_inv := ⋯, right_inv := ⋯ }