Matrices #
This file contains basic results on matrices including bundled versions of matrix operators.
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.
instance
Matrix.decidableEq
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[DecidableEq α]
[Fintype m]
[Fintype n]
:
DecidableEq (Matrix m n α)
instance
Matrix.instFintypeOfDecidableEq
{n : Type u_10}
{m : Type u_11}
[Fintype m]
[DecidableEq m]
[Fintype n]
[DecidableEq n]
(α : Type u_12)
[Fintype α]
:
Equations
- Matrix.instFintypeOfDecidableEq α = inferInstanceAs (Fintype (m → n → α))
def
Matrix.ofLinearEquiv
{m : Type u_2}
{n : Type u_3}
(R : Type u_7)
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
This is Matrix.of bundled as a linear equivalence.
Equations
- Matrix.ofLinearEquiv R = { toFun := Matrix.ofAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Matrix.ofAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
Matrix.coe_ofLinearEquiv
{m : Type u_2}
{n : Type u_3}
(R : Type u_7)
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
@[simp]
theorem
Matrix.coe_ofLinearEquiv_symm
{m : Type u_2}
{n : Type u_3}
(R : Type u_7)
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
theorem
Matrix.sum_apply
{m : Type u_2}
{n : Type u_3}
{α : Type v}
{β : Type w}
[AddCommMonoid α]
(i : m)
(j : n)
(s : Finset β)
(g : β → Matrix m n α)
:
Matrix.diagonal as an AddMonoidHom.
Equations
- Matrix.diagonalAddMonoidHom n α = { toFun := Matrix.diagonal, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
Matrix.diagonalAddMonoidHom_apply
(n : Type u_3)
(α : Type v)
[DecidableEq n]
[AddZeroClass α]
(d : n → α)
:
def
Matrix.diagonalLinearMap
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[DecidableEq n]
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
Matrix.diagonal as a LinearMap.
Equations
- Matrix.diagonalLinearMap n R α = { toFun := (↑(Matrix.diagonalAddMonoidHom n α)).toFun, map_add' := ⋯, map_smul' := ⋯ }
@[simp]
theorem
Matrix.diagonalLinearMap_apply
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[DecidableEq n]
[Semiring R]
[AddCommMonoid α]
[Module R α]
(a✝ : n → α)
:
theorem
Matrix.zero_le_one_elem
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[Zero α]
[One α]
[Preorder α]
[ZeroLEOneClass α]
(i j : n)
:
theorem
Matrix.zero_le_one_row
{n : Type u_3}
{α : Type v}
[DecidableEq n]
[Zero α]
[One α]
[Preorder α]
[ZeroLEOneClass α]
(i : n)
:
Matrix.diag as an AddMonoidHom.
Equations
- Matrix.diagAddMonoidHom n α = { toFun := Matrix.diag, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
Matrix.diagAddMonoidHom_apply
(n : Type u_3)
(α : Type v)
[AddZeroClass α]
(A : Matrix n n α)
(i : n)
:
def
Matrix.diagLinearMap
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
Matrix.diag as a LinearMap.
Equations
- Matrix.diagLinearMap n R α = { toFun := (↑(Matrix.diagAddMonoidHom n α)).toFun, map_add' := ⋯, map_smul' := ⋯ }
@[simp]
theorem
Matrix.diagLinearMap_apply
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
(a✝ : Matrix n n α)
(a✝¹ : n)
:
@[simp]
theorem
Matrix.diag_multiset_sum
{n : Type u_3}
{α : Type v}
[AddCommMonoid α]
(s : Multiset (Matrix n n α))
:
def
Matrix.diagonalRingHom
(n : Type u_3)
(α : Type v)
[NonAssocSemiring α]
[Fintype n]
[DecidableEq n]
:
Matrix.diagonal as a RingHom.
Equations
- Matrix.diagonalRingHom n α = { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
Matrix.diagonalRingHom_apply
(n : Type u_3)
(α : Type v)
[NonAssocSemiring α]
[Fintype n]
[DecidableEq n]
(d : n → α)
:
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 α)
@[simp]
theorem
Matrix.scalar_apply
{n : Type u_3}
{α : Type v}
[Semiring α]
[DecidableEq n]
[Fintype n]
(a : α)
:
theorem
Matrix.scalar_commute_iff
{n : Type u_3}
{α : Type v}
[Semiring α]
[DecidableEq n]
[Fintype n]
{r : α}
{M : Matrix n n α}
:
instance
Matrix.instAlgebra
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Algebra R α]
:
Equations
- Matrix.instAlgebra = { toSMul := Matrix.smul, algebraMap := (Matrix.scalar n).comp (algebraMap R α), commutes' := ⋯, smul_def' := ⋯ }
theorem
Matrix.algebraMap_matrix_apply
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Algebra R α]
{r : R}
{i j : n}
:
theorem
Matrix.algebraMap_eq_diagonal
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Algebra R α]
(r : R)
:
theorem
Matrix.algebraMap_eq_diagonalRingHom
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Algebra R α]
:
@[simp]
theorem
Matrix.map_algebraMap
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Semiring β]
[Algebra R α]
[Algebra R β]
(r : R)
(f : α → β)
(hf : f 0 = 0)
(hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r)
:
def
Matrix.diagonalAlgHom
{n : Type u_3}
(R : Type u_7)
{α : Type v}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Algebra R α]
:
Matrix.diagonal as an AlgHom.
Equations
- Matrix.diagonalAlgHom R = { toFun := Matrix.diagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
@[simp]
theorem
Matrix.diagonalAlgHom_apply
{n : Type u_3}
(R : Type u_7)
{α : Type v}
[Fintype n]
[DecidableEq n]
[CommSemiring R]
[Semiring α]
[Algebra R α]
(d : n → α)
:
theorem
Matrix.entryAddHom_eq_comp
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[Add α]
{i : m}
{j : n}
:
entryAddHom α i j = ((Pi.evalAddHom (fun (x : n) => α) j).comp (Pi.evalAddHom (fun (i : m) => n → α) i)).comp ↑ofAddEquiv.symm
def
Matrix.entryAddMonoidHom
{m : Type u_2}
{n : Type u_3}
(α : Type v)
[AddZeroClass α]
(i : m)
(j : n)
:
Extracting entries from a matrix as an additive monoid homomorphism. Note this cannot be upgraded to a ring homomorphism, as it does not respect multiplication.
Equations
- Matrix.entryAddMonoidHom α i j = { toFun := fun (M : Matrix m n α) => M i j, map_zero' := ⋯, map_add' := ⋯ }
@[simp]
theorem
Matrix.entryAddMonoidHom_apply
{m : Type u_2}
{n : Type u_3}
(α : Type v)
[AddZeroClass α]
(i : m)
(j : n)
(M : Matrix m n α)
:
theorem
Matrix.entryAddMonoidHom_eq_comp
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddZeroClass α]
{i : m}
{j : n}
:
entryAddMonoidHom α i j = ((Pi.evalAddMonoidHom (fun (x : n) => α) j).comp (Pi.evalAddMonoidHom (fun (i : m) => n → α) i)).comp ↑ofAddEquiv.symm
@[simp]
theorem
Matrix.evalAddMonoidHom_comp_diagAddMonoidHom
{m : Type u_2}
{α : Type v}
[AddZeroClass α]
(i : m)
:
@[simp]
theorem
Matrix.entryAddMonoidHom_toAddHom
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddZeroClass α]
{i : m}
{j : n}
:
def
Matrix.entryLinearMap
{m : Type u_2}
{n : Type u_3}
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
(i : m)
(j : n)
:
Extracting entries from a matrix as a linear map. Note this cannot be upgraded to an algebra homomorphism, as it does not respect multiplication.
Equations
- Matrix.entryLinearMap R α i j = { toFun := fun (M : Matrix m n α) => M i j, map_add' := ⋯, map_smul' := ⋯ }
@[simp]
theorem
Matrix.entryLinearMap_apply
{m : Type u_2}
{n : Type u_3}
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
(i : m)
(j : n)
(M : Matrix m n α)
:
theorem
Matrix.entryLinearMap_eq_comp
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
{i : m}
{j : n}
:
@[simp]
theorem
Matrix.proj_comp_diagLinearMap
{m : Type u_2}
{R : Type u_7}
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
(i : m)
:
@[simp]
theorem
Matrix.entryLinearMap_toAddMonoidHom
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
{i : m}
{j : n}
:
@[simp]
theorem
Matrix.entryLinearMap_toAddHom
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
[Semiring R]
[AddCommMonoid α]
[Module R α]
{i : m}
{j : n}
:
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.
@[simp]
def
AddMonoidHom.mapMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type v}
{β : Type w}
[AddZeroClass α]
[AddZeroClass β]
(f : α →+ β)
:
The AddMonoidHom between spaces of matrices induced by an AddMonoidHom between their
coefficients. This is Matrix.map as an AddMonoidHom.
@[simp]
theorem
AddMonoidHom.mapMatrix_apply
{m : Type u_2}
{n : Type u_3}
{α : Type v}
{β : Type w}
[AddZeroClass α]
[AddZeroClass β]
(f : α →+ β)
(M : Matrix m n α)
:
@[simp]
theorem
AddMonoidHom.mapMatrix_comp
{m : Type u_2}
{n : Type u_3}
{α : Type v}
{β : Type w}
{γ : Type u_9}
[AddZeroClass α]
[AddZeroClass β]
[AddZeroClass γ]
(f : β →+ γ)
(g : α →+ β)
:
@[simp]
theorem
AddMonoidHom.entryAddMonoidHom_comp_mapMatrix
{m : Type u_2}
{n : Type u_3}
{α : Type v}
{β : Type w}
[AddZeroClass α]
[AddZeroClass β]
(f : α →+ β)
(i : m)
(j : n)
:
def
LinearMap.mapMatrix
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(f : α →ₗ[R] β)
:
The LinearMap between spaces of matrices induced by a LinearMap between their
coefficients. This is Matrix.map as a LinearMap.
@[simp]
theorem
LinearMap.mapMatrix_comp
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
{γ : Type u_9}
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(f : β →ₗ[R] γ)
(g : α →ₗ[R] β)
:
@[simp]
theorem
LinearMap.entryLinearMap_comp_mapMatrix
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(f : α →ₗ[R] β)
(i : m)
(j : n)
:
def
LinearEquiv.mapMatrix
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(f : α ≃ₗ[R] β)
:
The LinearEquiv between spaces of matrices induced by a LinearEquiv between their
coefficients. This is Matrix.map as a LinearEquiv.
@[simp]
theorem
LinearEquiv.mapMatrix_trans
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
{γ : Type u_9}
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(f : α ≃ₗ[R] β)
(g : β ≃ₗ[R] γ)
:
@[simp]
theorem
LinearEquiv.entryLinearMap_comp_mapMatrix
{m : Type u_2}
{n : Type u_3}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(f : α ≃ₗ[R] β)
(i : m)
(j : n)
:
def
RingHom.mapMatrix
{m : Type u_2}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
(f : α →+* β)
:
The RingHom between spaces of square matrices induced by a RingHom between their
coefficients. This is Matrix.map as a RingHom.
@[simp]
theorem
RingHom.mapMatrix_apply
{m : Type u_2}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
(f : α →+* β)
(M : Matrix m m α)
:
@[simp]
theorem
RingHom.mapMatrix_id
{m : Type u_2}
{α : Type v}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
:
@[simp]
theorem
RingHom.mapMatrix_comp
{m : Type u_2}
{α : Type v}
{β : Type w}
{γ : Type u_9}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
[NonAssocSemiring γ]
(f : β →+* γ)
(g : α →+* β)
:
def
RingEquiv.mapMatrix
{m : Type u_2}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
(f : α ≃+* β)
:
The RingEquiv between spaces of square matrices induced by a RingEquiv between their
coefficients. This is Matrix.map as a RingEquiv.
@[simp]
theorem
RingEquiv.mapMatrix_apply
{m : Type u_2}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
(f : α ≃+* β)
(M : Matrix m m α)
:
@[simp]
theorem
RingEquiv.mapMatrix_refl
{m : Type u_2}
{α : Type v}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
:
@[simp]
theorem
RingEquiv.mapMatrix_symm
{m : Type u_2}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
(f : α ≃+* β)
:
@[simp]
theorem
RingEquiv.mapMatrix_trans
{m : Type u_2}
{α : Type v}
{β : Type w}
{γ : Type u_9}
[Fintype m]
[DecidableEq m]
[NonAssocSemiring α]
[NonAssocSemiring β]
[NonAssocSemiring γ]
(f : α ≃+* β)
(g : β ≃+* γ)
:
@[simp]
theorem
RingEquiv.mopMatrix_symm_apply
{m : Type u_2}
{α : Type v}
[Fintype m]
[NonAssocSemiring α]
(M : (Matrix m m α)ᵐᵒᵖ)
:
@[simp]
theorem
RingEquiv.mopMatrix_apply
{m : Type u_2}
{α : Type v}
[Fintype m]
[NonAssocSemiring α]
(M : Matrix m m αᵐᵒᵖ)
:
def
AlgHom.mapMatrix
{m : Type u_2}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[CommSemiring R]
[Semiring α]
[Semiring β]
[Algebra R α]
[Algebra R β]
(f : α →ₐ[R] β)
:
The AlgHom between spaces of square matrices induced by an AlgHom between their
coefficients. This is Matrix.map as an AlgHom.
@[simp]
theorem
AlgHom.mapMatrix_id
{m : Type u_2}
{R : Type u_7}
{α : Type v}
[Fintype m]
[DecidableEq m]
[CommSemiring R]
[Semiring α]
[Algebra R α]
:
def
AlgEquiv.mapMatrix
{m : Type u_2}
{R : Type u_7}
{α : Type v}
{β : Type w}
[Fintype m]
[DecidableEq m]
[CommSemiring R]
[Semiring α]
[Semiring β]
[Algebra R α]
[Algebra R β]
(f : α ≃ₐ[R] β)
:
The AlgEquiv between spaces of square matrices induced by an AlgEquiv between their
coefficients. This is Matrix.map as an AlgEquiv.
@[simp]
theorem
AlgEquiv.mapMatrix_refl
{m : Type u_2}
{R : Type u_7}
{α : Type v}
[Fintype m]
[DecidableEq m]
[CommSemiring R]
[Semiring α]
[Algebra R α]
:
Matrix.transpose as an AddEquiv
Equations
- Matrix.transposeAddEquiv m n α = { toFun := Matrix.transpose, invFun := Matrix.transpose, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
@[simp]
theorem
Matrix.transpose_multiset_sum
{m : Type u_2}
{n : Type u_3}
{α : Type v}
[AddCommMonoid α]
(s : Multiset (Matrix m n α))
:
def
Matrix.transposeLinearEquiv
(m : Type u_2)
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
Matrix.transpose as a LinearMap
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Matrix.transposeLinearEquiv_apply
(m : Type u_2)
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
(a✝ : Matrix m n α)
:
@[simp]
theorem
Matrix.transposeLinearEquiv_symm
(m : Type u_2)
(n : Type u_3)
(R : Type u_7)
(α : Type v)
[Semiring R]
[AddCommMonoid α]
[Module R α]
:
def
Matrix.transposeRingEquiv
(m : Type u_2)
(α : Type v)
[AddCommMonoid α]
[CommSemigroup α]
[Fintype m]
:
Matrix.transpose as a RingEquiv to the opposite ring
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Matrix.transposeRingEquiv_symm_apply
(m : Type u_2)
(α : Type v)
[AddCommMonoid α]
[CommSemigroup α]
[Fintype m]
(M : (Matrix m m α)ᵐᵒᵖ)
:
@[simp]
theorem
Matrix.transposeRingEquiv_apply
(m : Type u_2)
(α : Type v)
[AddCommMonoid α]
[CommSemigroup α]
[Fintype m]
(M : Matrix m m α)
:
@[simp]
theorem
Matrix.transpose_pow
{m : Type u_2}
{α : Type v}
[CommSemiring α]
[Fintype m]
[DecidableEq m]
(M : Matrix m m α)
(k : ℕ)
:
def
Matrix.transposeAlgEquiv
(m : Type u_2)
(R : Type u_7)
(α : Type v)
[CommSemiring R]
[CommSemiring α]
[Fintype m]
[DecidableEq m]
[Algebra R α]
:
Matrix.transpose as an AlgEquiv to the opposite ring
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Matrix.transposeAlgEquiv_apply
(m : Type u_2)
(R : Type u_7)
(α : Type v)
[CommSemiring R]
[CommSemiring α]
[Fintype m]
[DecidableEq m]
[Algebra R α]
(M : Matrix m m α)
:
@[simp]
theorem
Matrix.transposeAlgEquiv_symm_apply
(m : Type u_2)
(R : Type u_7)
(α : Type v)
[CommSemiring R]
[CommSemiring α]
[Fintype m]
[DecidableEq m]
[Algebra R α]
(a✝ : (Matrix m m α)ᵐᵒᵖ)
:
(transposeAlgEquiv m R α).symm a✝ = ((transposeAddEquiv m m α).trans MulOpposite.opAddEquiv).invFun a✝