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.BlockTriangular expresses that an o by o matrix is block triangular, if the rows and columns are ordered according to some order b : 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 blocks
• Matrix.det_of_upperTriangular and Matrix.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 → α) : Prop

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

• M.BlockTriangular b = ∀ ⦃i j : m⦄, b j < b i → M i j = 0

@[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 : M.BlockTriangular b) : (M.submatrix f f).BlockTriangular (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.reindex e e) M).BlockTriangular b ↔ M.BlockTriangular (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 α] : M.BlockTriangular b → M.transpose.BlockTriangular (⇑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 → αᵒᵈ} : M.transpose.BlockTriangular b ↔ M.BlockTriangular (⇑OrderDual.ofDual ∘ b)

@[simp]

theorem Matrix.blockTriangular_zero {α : Type u_1} {m : Type u_3} {R : Type v} [CommRing R] {b : m → α} [LT α] : Matrix.BlockTriangular 0 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 : M.BlockTriangular b) : (-M).BlockTriangular 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 : M.BlockTriangular b) (hN : N.BlockTriangular b) : (M + N).BlockTriangular 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 : M.BlockTriangular b) (hN : N.BlockTriangular b) : (M - N).BlockTriangular 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) : (Matrix.diagonal d).BlockTriangular b

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.blockDiagonal' d).BlockTriangular 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.blockDiagonal d).BlockTriangular Prod.snd

theorem Matrix.blockTriangular_one {α : Type u_1} {m : Type u_3} {R : Type v} [CommRing R] {b : m → α} [Preorder α] [DecidableEq m] : Matrix.BlockTriangular 1 b

theorem Matrix.blockTriangular_stdBasisMatrix {α : Type u_1} {m : Type u_3} {R : Type v} [CommRing R] {b : m → α} [Preorder α] [DecidableEq m] {i : m} {j : m} (hij : b i ≤ b j) (c : R) : (Matrix.stdBasisMatrix i j c).BlockTriangular b

theorem Matrix.blockTriangular_stdBasisMatrix' {α : Type u_1} {m : Type u_3} {R : Type v} [CommRing R] {b : m → α} [Preorder α] [DecidableEq m] {i : m} {j : m} (hij : b j ≤ b i) (c : R) : (Matrix.stdBasisMatrix i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)

theorem Matrix.blockTriangular_transvection {α : Type u_1} {m : Type u_3} {R : Type v} [CommRing R] {b : m → α} [Preorder α] [DecidableEq m] {i : m} {j : m} (hij : b i ≤ b j) (c : R) : (Matrix.transvection i j c).BlockTriangular b

theorem Matrix.blockTriangular_transvection' {α : Type u_1} {m : Type u_3} {R : Type v} [CommRing R] {b : m → α} [Preorder α] [DecidableEq m] {i : m} {j : m} (hij : b j ≤ b i) (c : R) : (Matrix.transvection i j c).BlockTriangular (⇑OrderDual.toDual ∘ b)

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 : M.BlockTriangular b) (hN : N.BlockTriangular b) : (M * N).BlockTriangular 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.fromBlocks A B 0 D).BlockTriangular (Sum.elim (fun (x : m) => a) fun (x : n) => 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) : (M.toSquareBlockProp p).det = (M.toSquareBlockProp q).det

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) : (M.toSquareBlock id i).det = 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] : M.det = (Matrix.fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) => ¬p j) (M.toBlock (fun (j : m) => ¬p j) p) (M.toBlock (fun (j : m) => ¬p j) fun (j : m) => ¬p j)).det

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) : M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun (i : m) => ¬p i).det

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) : M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun (i : m) => ¬p i).det

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 : M.BlockTriangular b) : M.det = ∏ a ∈ Finset.image b Finset.univ, (M.toSquareBlock b a).det

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 : M.BlockTriangular b) : M.det = ∏ k : α, (M.toSquareBlock b k).det

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 : M.BlockTriangular id) : M.det = ∏ i : m, 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 : M.BlockTriangular ⇑OrderDual.toDual) : M.det = ∏ i : m, M i i

theorem Matrix.matrixOfPolynomials_blockTriangular {R : Type v} [CommRing R] {n : ℕ} (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), (p i).natDegree ≤ ↑i) : (Matrix.of fun (i j : Fin n) => (p j).coeff ↑i).BlockTriangular id

theorem Matrix.det_matrixOfPolynomials {R : Type v} [CommRing R] {n : ℕ} (p : Fin n → Polynomial R) (h_deg : ∀ (i : Fin n), (p i).natDegree = ↑i) (h_monic : ∀ (i : Fin n), (p i).Monic) : (Matrix.of fun (i j : Fin n) => (p j).coeff ↑i).det = 1

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 : M.BlockTriangular b) (k : α) : ((M⁻¹.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k) * M.toBlock (fun (i : m) => b i < k) fun (i : m) => 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 : M.BlockTriangular b) (k : α) : (M.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k)⁻¹ = M⁻¹.toBlock (fun (i : m) => b i < k) fun (i : m) => 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 : M.BlockTriangular b) (k : α) : Invertible (M.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k)

An upper-left subblock of an invertible block-triangular matrix is invertible.

Equations

• hM.invertibleToBlock k = (M.toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k).invertibleOfLeftInverse ((⅟M).toBlock (fun (i : m) => b i < k) fun (i : m) => b i < k) ⋯

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 : M.BlockTriangular b) (k : α) : (M⁻¹.toBlock (fun (i : m) => k ≤ b i) fun (i : m) => 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 : M.BlockTriangular b) : M⁻¹.BlockTriangular b

The inverse of a block-triangular matrix is block-triangular.