Documentation

Mathlib.LinearAlgebra.Matrix.Block

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 #

Main results #

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
  • M.BlockTriangular b = ∀ ⦃i j : m⦄, b j < b iM 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 : nm} (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 bM.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 α] :
    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 : mR) :
    (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] :
    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 : mProp} {q : mProp} [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 : mProp) [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 : mProp) [DecidablePred p] (h : ∀ (i : m), ¬p i∀ (j : m), p jM 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 : mProp) [DecidablePred p] (h : ∀ (i : m), p i∀ (j : m), ¬p jM 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 = aFinset.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 nPolynomial 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 nPolynomial 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)
    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 : 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.