Block Matrices #
Main definitions #
Matrix.fromBlocks
: build a block matrix out of 4 blocksMatrix.toBlocks₁₁
,Matrix.toBlocks₁₂
,Matrix.toBlocks₂₁
,Matrix.toBlocks₂₂
: extract each of the four blocks fromMatrix.fromBlocks
.Matrix.blockDiagonal
: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms,Matrix.blockDiagonalRingHom
.Matrix.blockDiag
: extract the blocks from the diagonal of a block diagonal matrix.Matrix.blockDiagonal'
: block diagonal of unequally sized blocks. On square blocks, this is a ring homomorphisms,Matrix.blockDiagonal'RingHom
.Matrix.blockDiag'
: extract the blocks from the diagonal of a block diagonal matrix.
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.
Equations
- M.toBlocks₁₁ = Matrix.of fun (i : n) (j : l) => M (Sum.inl i) (Sum.inl j)
Instances For
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.
Equations
- M.toBlocks₁₂ = Matrix.of fun (i : n) (j : m) => M (Sum.inl i) (Sum.inr j)
Instances For
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.
Equations
- M.toBlocks₂₁ = Matrix.of fun (i : o) (j : l) => M (Sum.inr i) (Sum.inl j)
Instances For
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.
Equations
- M.toBlocks₂₂ = Matrix.of fun (i : o) (j : m) => M (Sum.inr i) (Sum.inr j)
Instances For
Two block matrices are equal if their blocks are equal.
A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish
Equations
- A.IsTwoBlockDiagonal = (A.toBlocks₁₂ = 0 ∧ A.toBlocks₂₁ = 0)
Instances For
Let p
pick out certain rows and q
pick out certain columns of a matrix M
. Then
toBlock M p q
is the corresponding block matrix.
Equations
- M.toBlock p q = M.submatrix Subtype.val Subtype.val
Instances For
Let p
pick out certain rows and columns of a square matrix M
. Then
toSquareBlockProp M p
is the corresponding block matrix.
Equations
- M.toSquareBlockProp p = M.toBlock p p
Instances For
Let b
map rows and columns of a square matrix M
to blocks. Then
toSquareBlock M b k
is the block k
matrix.
Equations
- M.toSquareBlock b k = M.toSquareBlockProp fun (a : m) => b a = k
Instances For
Matrix.blockDiagonal M
turns a homogeneously-indexed collection of matrices
M : o → Matrix m n α'
into an m × o
-by-n × o
block matrix which has the entries of M
along
the diagonal and zero elsewhere.
See also Matrix.blockDiagonal'
if the matrices may not have the same size everywhere.
Equations
Instances For
Matrix.blockDiagonal
as an AddMonoidHom
.
Equations
- Matrix.blockDiagonalAddMonoidHom m n o α = { toFun := Matrix.blockDiagonal, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Matrix.blockDiagonal
as a RingHom
.
Equations
- Matrix.blockDiagonalRingHom m o α = { toFun := Matrix.blockDiagonal, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Extract a block from the diagonal of a block diagonal matrix.
This is the block form of Matrix.diag
, and the left-inverse of Matrix.blockDiagonal
.
Instances For
Matrix.blockDiag
as an AddMonoidHom
.
Equations
- Matrix.blockDiagAddMonoidHom m n o α = { toFun := Matrix.blockDiag, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Matrix.blockDiagonal' M
turns M : Π i, Matrix (m i) (n i) α
into a
Σ i, m i
-by-Σ i, n i
block matrix which has the entries of M
along the diagonal
and zero elsewhere.
This is the dependently-typed version of Matrix.blockDiagonal
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Matrix.blockDiagonal'
as an AddMonoidHom
.
Equations
- Matrix.blockDiagonal'AddMonoidHom m' n' α = { toFun := Matrix.blockDiagonal', map_zero' := ⋯, map_add' := ⋯ }
Instances For
Matrix.blockDiagonal'
as a RingHom
.
Equations
- Matrix.blockDiagonal'RingHom m' α = { toFun := Matrix.blockDiagonal', map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Extract a block from the diagonal of a block diagonal matrix.
This is the block form of Matrix.diag
, and the left-inverse of Matrix.blockDiagonal'
.
Equations
- M.blockDiag' k = Matrix.of fun (i : m' k) (j : n' k) => M ⟨k, i⟩ ⟨k, j⟩
Instances For
Matrix.blockDiag'
as an AddMonoidHom
.
Equations
- Matrix.blockDiag'AddMonoidHom m' n' α = { toFun := Matrix.blockDiag', map_zero' := ⋯, map_add' := ⋯ }