Block Matrices #
Main definitions #
matrix.from_blocks
: build a block matrix out of 4 blocksmatrix.to_blocks₁₁
,matrix.to_blocks₁₂
,matrix.to_blocks₂₁
,matrix.to_blocks₂₂
: extract each of the four blocks frommatrix.from_blocks
.matrix.block_diagonal
: block diagonal of equally sized blocks. On square blocks, this is a ring homomorphisms,matrix.block_diagonal_ring_hom
.matrix.block_diag
: extract the blocks from the diagonal of a block diagonal matrix.matrix.block_diagonal'
: block diagonal of unequally sized blocks. On square blocks, this is a ring homomorphisms,matrix.block_diagonal'_ring_hom
.matrix.block_diag'
: extract the blocks from the diagonal of a block diagonal matrix.
We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.
A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish
Equations
- A.is_two_block_diagonal = (A.to_blocks₁₂ = 0 ∧ A.to_blocks₂₁ = 0)
Let p
pick out certain rows and q
pick out certain columns of a matrix M
. Then
to_block M p q
is the corresponding block matrix.
Let b
map rows and columns of a square matrix M
to blocks. Then
to_square_block M b k
is the block k
matrix.
Equations
- M.to_square_block b k = M.submatrix coe coe
Alternate version with b : m → nat
. Let b
map rows and columns of a square matrix M
to
blocks. Then to_square_block' M b k
is the block k
matrix.
Equations
- M.to_square_block' b k = M.submatrix coe coe
Let p
pick out certain rows and columns of a square matrix M
. Then
to_square_block_prop M p
is the corresponding block matrix.
Equations
- M.to_square_block_prop p = M.submatrix coe coe
matrix.block_diagonal M
turns a homogenously-indexed collection of matrices
M : o → matrix m n α'
into a m × o
-by-n × o
block matrix which has the entries of M
along
the diagonal and zero elsewhere.
See also matrix.block_diagonal'
if the matrices may not have the same size everywhere.
Equations
- matrix.block_diagonal M (i, k) (j, k') = ite (k = k') (M k i j) 0
matrix.block_diagonal
as an add_monoid_hom
.
Equations
- matrix.block_diagonal_add_monoid_hom m n o α = {to_fun := matrix.block_diagonal (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
matrix.block_diagonal
as a ring_hom
.
Equations
- matrix.block_diagonal_ring_hom m o α = {to_fun := matrix.block_diagonal (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
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.block_diagonal
.
Equations
- M.block_diag k i j = M (i, k) (j, k)
matrix.block_diag
as an add_monoid_hom
.
Equations
- matrix.block_diag_add_monoid_hom m n o α = {to_fun := matrix.block_diag α, map_zero' := _, map_add' := _}
matrix.block_diagonal' 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.block_diagonal
.
matrix.block_diagonal'
as an add_monoid_hom
.
Equations
- matrix.block_diagonal'_add_monoid_hom m' n' α = {to_fun := matrix.block_diagonal' (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
matrix.block_diagonal'
as a ring_hom
.
Equations
- matrix.block_diagonal'_ring_hom m' α = {to_fun := matrix.block_diagonal' (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
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.block_diagonal'
.
Equations
- M.block_diag' k i j = M ⟨k, i⟩ ⟨k, j⟩
matrix.block_diag'
as an add_monoid_hom
.
Equations
- matrix.block_diag'_add_monoid_hom m' n' α = {to_fun := matrix.block_diag' α, map_zero' := _, map_add' := _}