Block matrices and their determinant #
This file defines a predicate Matrix.BlockTriangular saying a matrix
is block triangular, and proves the value of the determinant for various
matrices built out of blocks.
Main definitions #
Matrix.BlockTriangularexpresses that anobyomatrix is block triangular, if the rows and columns are ordered according to some orderb : o → α
Main results #
Matrix.det_of_blockTriangular: the determinant of a block triangular matrix is equal to the product of the determinants of all the blocksMatrix.det_of_upperTriangularandMatrix.det_of_lowerTriangular: the determinant of a triangular matrix is the product of the entries along the diagonal
Tags #
matrix, diagonal, det, block triangular
def
Matrix.BlockTriangular
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
[LT α]
(M : Matrix m m R)
(b : m → α)
:
Let b map rows and columns of a square matrix M to blocks indexed by αs. Then
BlockTriangular M n b says the matrix is block triangular.
Equations
- Matrix.BlockTriangular M b = ∀ ⦃i j : m⦄, b j < b i → M i j = 0
Instances For
@[simp]
theorem
Matrix.BlockTriangular.submatrix
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[LT α]
{f : n → m}
(h : Matrix.BlockTriangular M b)
:
Matrix.BlockTriangular (Matrix.submatrix M f f) (b ∘ f)
theorem
Matrix.blockTriangular_reindex_iff
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
[LT α]
{b : n → α}
{e : m ≃ n}
:
Matrix.BlockTriangular (↑(Matrix.reindex e e) M) b ↔ Matrix.BlockTriangular M (b ∘ ↑e)
theorem
Matrix.BlockTriangular.transpose
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[LT α]
:
Matrix.BlockTriangular M b → Matrix.BlockTriangular (Matrix.transpose M) (↑OrderDual.toDual ∘ b)
@[simp]
theorem
Matrix.blockTriangular_transpose_iff
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
[LT α]
{b : m → αᵒᵈ}
:
Matrix.BlockTriangular (Matrix.transpose M) b ↔ Matrix.BlockTriangular M (↑OrderDual.ofDual ∘ b)
theorem
Matrix.BlockTriangular.neg
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[LT α]
(hM : Matrix.BlockTriangular M b)
:
Matrix.BlockTriangular (-M) b
theorem
Matrix.BlockTriangular.add
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{N : Matrix m m R}
{b : m → α}
[LT α]
(hM : Matrix.BlockTriangular M b)
(hN : Matrix.BlockTriangular N b)
:
Matrix.BlockTriangular (M + N) b
theorem
Matrix.BlockTriangular.sub
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{N : Matrix m m R}
{b : m → α}
[LT α]
(hM : Matrix.BlockTriangular M b)
(hN : Matrix.BlockTriangular N b)
:
Matrix.BlockTriangular (M - N) b
theorem
Matrix.blockTriangular_diagonal
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{b : m → α}
[Preorder α]
[DecidableEq m]
(d : m → R)
:
theorem
Matrix.blockTriangular_blockDiagonal'
{α : Type u_1}
{m' : α → Type u_6}
{R : Type v}
[CommRing R]
[Preorder α]
[DecidableEq α]
(d : (i : α) → Matrix (m' i) (m' i) R)
:
Matrix.BlockTriangular (Matrix.blockDiagonal' d) Sigma.fst
theorem
Matrix.blockTriangular_blockDiagonal
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
[Preorder α]
[DecidableEq α]
(d : α → Matrix m m R)
:
Matrix.BlockTriangular (Matrix.blockDiagonal d) Prod.snd
theorem
Matrix.BlockTriangular.mul
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{b : m → α}
[LinearOrder α]
[Fintype m]
{M : Matrix m m R}
{N : Matrix m m R}
(hM : Matrix.BlockTriangular M b)
(hN : Matrix.BlockTriangular N b)
:
Matrix.BlockTriangular (M * N) b
theorem
Matrix.upper_two_blockTriangular
{α : Type u_1}
{m : Type u_3}
{n : Type u_4}
{R : Type v}
[CommRing R]
[Preorder α]
(A : Matrix m m R)
(B : Matrix m n R)
(D : Matrix n n R)
{a : α}
{b : α}
(hab : a < b)
:
Matrix.BlockTriangular (Matrix.fromBlocks A B 0 D) (Sum.elim (fun x => a) fun x => b)
Determinant #
theorem
Matrix.equiv_block_det
{m : Type u_3}
{R : Type v}
[CommRing R]
[DecidableEq m]
[Fintype m]
(M : Matrix m m R)
{p : m → Prop}
{q : m → Prop}
[DecidablePred p]
[DecidablePred q]
(e : ∀ (x : m), q x ↔ p x)
:
@[simp]
theorem
Matrix.det_toSquareBlock_id
{m : Type u_3}
{R : Type v}
[CommRing R]
[DecidableEq m]
[Fintype m]
(M : Matrix m m R)
(i : m)
:
Matrix.det (Matrix.toSquareBlock M id i) = M i i
theorem
Matrix.det_toBlock
{m : Type u_3}
{R : Type v}
[CommRing R]
[DecidableEq m]
[Fintype m]
(M : Matrix m m R)
(p : m → Prop)
[DecidablePred p]
:
Matrix.det M = Matrix.det
(Matrix.fromBlocks (Matrix.toBlock M p p) (Matrix.toBlock M p fun j => ¬p j) (Matrix.toBlock M (fun j => ¬p j) p)
(Matrix.toBlock M (fun j => ¬p j) fun j => ¬p j))
theorem
Matrix.twoBlockTriangular_det
{m : Type u_3}
{R : Type v}
[CommRing R]
[DecidableEq m]
[Fintype m]
(M : Matrix m m R)
(p : m → Prop)
[DecidablePred p]
(h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0)
:
Matrix.det M = Matrix.det (Matrix.toSquareBlockProp M p) * Matrix.det (Matrix.toSquareBlockProp M fun i => ¬p i)
theorem
Matrix.twoBlockTriangular_det'
{m : Type u_3}
{R : Type v}
[CommRing R]
[DecidableEq m]
[Fintype m]
(M : Matrix m m R)
(p : m → Prop)
[DecidablePred p]
(h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0)
:
Matrix.det M = Matrix.det (Matrix.toSquareBlockProp M p) * Matrix.det (Matrix.toSquareBlockProp M fun i => ¬p i)
theorem
Matrix.BlockTriangular.det
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[DecidableEq α]
[LinearOrder α]
(hM : Matrix.BlockTriangular M b)
:
Matrix.det M = Finset.prod (Finset.image b Finset.univ) fun a => Matrix.det (Matrix.toSquareBlock M b a)
theorem
Matrix.BlockTriangular.det_fintype
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[DecidableEq α]
[Fintype α]
[LinearOrder α]
(h : Matrix.BlockTriangular M b)
:
Matrix.det M = Finset.prod Finset.univ fun k => Matrix.det (Matrix.toSquareBlock M b k)
theorem
Matrix.det_of_upperTriangular
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
[DecidableEq m]
[Fintype m]
[LinearOrder m]
(h : Matrix.BlockTriangular M id)
:
Matrix.det M = Finset.prod Finset.univ fun i => M i i
theorem
Matrix.det_of_lowerTriangular
{m : Type u_3}
{R : Type v}
[CommRing R]
[DecidableEq m]
[Fintype m]
[LinearOrder m]
(M : Matrix m m R)
(h : Matrix.BlockTriangular M ↑OrderDual.toDual)
:
Matrix.det M = Finset.prod Finset.univ fun i => M i i
Invertible #
theorem
Matrix.BlockTriangular.toBlock_inverse_mul_toBlock_eq_one
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[LinearOrder α]
[Invertible M]
(hM : Matrix.BlockTriangular M b)
(k : α)
:
((Matrix.toBlock M⁻¹ (fun i => b i < k) fun i => b i < k) * Matrix.toBlock M (fun i => b i < k) fun i => b i < k) = 1
theorem
Matrix.BlockTriangular.inv_toBlock
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[LinearOrder α]
[Invertible M]
(hM : Matrix.BlockTriangular M b)
(k : α)
:
(Matrix.toBlock M (fun i => b i < k) fun i => b i < k)⁻¹ = Matrix.toBlock M⁻¹ (fun i => b i < k) fun i => b i < k
The inverse of an upper-left subblock of a block-triangular matrix M is the upper-left
subblock of M⁻¹.
def
Matrix.BlockTriangular.invertibleToBlock
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[LinearOrder α]
[Invertible M]
(hM : Matrix.BlockTriangular M b)
(k : α)
:
Invertible (Matrix.toBlock M (fun i => b i < k) fun i => b i < k)
An upper-left subblock of an invertible block-triangular matrix is invertible.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Matrix.toBlock_inverse_eq_zero
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[LinearOrder α]
[Invertible M]
(hM : Matrix.BlockTriangular M b)
(k : α)
:
(Matrix.toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
A lower-left subblock of the inverse of a block-triangular matrix is zero. This is a first step
towards BlockTriangular.inv_toBlock below.
theorem
Matrix.blockTriangular_inv_of_blockTriangular
{α : Type u_1}
{m : Type u_3}
{R : Type v}
[CommRing R]
{M : Matrix m m R}
{b : m → α}
[DecidableEq m]
[Fintype m]
[LinearOrder α]
[Invertible M]
(hM : Matrix.BlockTriangular M b)
:
The inverse of a block-triangular matrix is block-triangular.