mathlib documentation

linear_algebra.matrix.block

Block matrices and their determinant #

This file defines a predicate matrix.block_triangular saying a matrix is block triangular, and proves the value of the determinant for various matrices built out of blocks.

Main definitions #

Main results #

Tags #

matrix, diagonal, det, block triangular

def matrix.block_triangular {α : Type u_1} {m : Type u_2} {R : Type v} [comm_ring R] [has_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 block_triangular M n b says the matrix is block triangular.

Equations
@[protected, simp]
theorem matrix.block_triangular.submatrix {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} [comm_ring R] {M : matrix m m R} {b : m → α} [has_lt α] {f : n → m} (h : M.block_triangular b) :
theorem matrix.block_triangular_reindex_iff {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} [comm_ring R] {M : matrix m m R} [has_lt α] {b : n → α} {e : m n} :
@[protected]
theorem matrix.block_triangular.transpose {α : Type u_1} {m : Type u_2} {R : Type v} [comm_ring R] {M : matrix m m R} {b : m → α} [has_lt α] :
@[protected, simp]
theorem matrix.block_triangular_transpose_iff {α : Type u_1} {m : Type u_2} {R : Type v} [comm_ring R] {M : matrix m m R} [has_lt α] {b : m → αᵒᵈ} :
theorem matrix.upper_two_block_triangular {α : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type v} [comm_ring R] [preorder α] (A : matrix m m R) (B : matrix m n R) (D : matrix n n R) {a b : α} (hab : a < b) :
(matrix.from_blocks A B 0 D).block_triangular (sum.elim (λ (i : m), a) (λ (j : n), b))

Determinant #

theorem matrix.equiv_block_det {m : Type u_2} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : matrix m m R) {p q : m → Prop} [decidable_pred p] [decidable_pred q] (e : ∀ (x : m), q x p x) :
@[simp]
theorem matrix.det_to_square_block_id {m : Type u_2} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : matrix m m R) (i : m) :
(M.to_square_block id i).det = M i i
theorem matrix.det_to_block {m : Type u_2} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : matrix m m R) (p : m → Prop) [decidable_pred p] :
M.det = (matrix.from_blocks (M.to_block p p) (M.to_block p (λ (j : m), ¬p j)) (M.to_block (λ (j : m), ¬p j) p) (M.to_block (λ (j : m), ¬p j) (λ (j : m), ¬p j))).det
theorem matrix.two_block_triangular_det {m : Type u_2} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : matrix m m R) (p : m → Prop) [decidable_pred p] (h : ∀ (i : m), ¬p i∀ (j : m), p jM i j = 0) :
M.det = (M.to_square_block_prop p).det * (M.to_square_block_prop (λ (i : m), ¬p i)).det
theorem matrix.two_block_triangular_det' {m : Type u_2} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] (M : matrix m m R) (p : m → Prop) [decidable_pred p] (h : ∀ (i : m), p i∀ (j : m), ¬p jM i j = 0) :
M.det = (M.to_square_block_prop p).det * (M.to_square_block_prop (λ (i : m), ¬p i)).det
@[protected]
theorem matrix.block_triangular.det {α : Type u_1} {m : Type u_2} {R : Type v} [comm_ring R] {M : matrix m m R} {b : m → α} [decidable_eq m] [fintype m] [decidable_eq α] [linear_order α] (hM : M.block_triangular b) :
M.det = (finset.image b finset.univ).prod (λ (a : α), (M.to_square_block b a).det)
theorem matrix.block_triangular.det_fintype {α : Type u_1} {m : Type u_2} {R : Type v} [comm_ring R] {M : matrix m m R} {b : m → α} [decidable_eq m] [fintype m] [decidable_eq α] [fintype α] [linear_order α] (h : M.block_triangular b) :
M.det = finset.univ.prod (λ (k : α), (M.to_square_block b k).det)
theorem matrix.det_of_upper_triangular {m : Type u_2} {R : Type v} [comm_ring R] {M : matrix m m R} [decidable_eq m] [fintype m] [linear_order m] (h : M.block_triangular id) :
M.det = finset.univ.prod (λ (i : m), M i i)
theorem matrix.det_of_lower_triangular {m : Type u_2} {R : Type v} [comm_ring R] [decidable_eq m] [fintype m] [linear_order m] (M : matrix m m R) (h : M.block_triangular order_dual.to_dual) :
M.det = finset.univ.prod (λ (i : m), M i i)