# 2×2 block matrices and the Schur complement #

This file proves properties of 2×2 block matrices `[A B; C D]` that relate to the Schur complement `D - C*A⁻¹*B`.

Some of the results here generalize to 2×2 matrices in a category, rather than just a ring. A few results in this direction can be found in `Mathlib/CategoryTheory/Preadditive/Biproducts.lean`, especially the declarations `CategoryTheory.Biprod.gaussian` and `CategoryTheory.Biprod.isoElim`. Compare with `Matrix.invertibleOfFromBlocks₁₁Invertible`.

## Main results #

- `Matrix.det_fromBlocks₁₁`, `Matrix.det_fromBlocks₂₂`: determinant of a block matrix in terms of the Schur complement.
- `Matrix.invOf_fromBlocks_zero₂₁_eq`, `Matrix.invOf_fromBlocks_zero₁₂_eq`: the inverse of a block triangular matrix.
- `Matrix.isUnit_fromBlocks_zero₂₁`, `Matrix.isUnit_fromBlocks_zero₁₂`: invertibility of a block triangular matrix.
- `Matrix.det_one_add_mul_comm`: the Weinstein–Aronszajn identity.

source
theorem Matrix.fromBlocks_eq_of_invertible₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix l m α) (D : Matrix l n α) [Invertible A] :
fromBlocks A B C D = fromBlocks 1 0 (C * ⅟ A) 1 * fromBlocks A 0 0 (D - C * ⅟ A * B) * fromBlocks 1 (⅟ A * B) 0 1

LDU decomposition of a block matrix with an invertible top-left corner, using the Schur complement.

source
theorem Matrix.fromBlocks_eq_of_invertible₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype l] [Fintype m] [Fintype n] [DecidableEq l] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix l m α) (B : Matrix l n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :
fromBlocks A B C D = fromBlocks 1 (B * ⅟ D) 0 1 * fromBlocks (A - B * ⅟ D * C) 0 0 D * fromBlocks 1 0 (⅟ D * C) 1

LDU decomposition of a block matrix with an invertible bottom-right corner, using the Schur complement.

#### Block triangular matrices #

source
def Matrix.fromBlocksZero₂₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] :
Invertible (fromBlocks A B 0 D)

An upper-block-triangular matrix is invertible if its diagonal is.

Equations

- A.fromBlocksZero₂₁Invertible B D = (Matrix.fromBlocks A B 0 D).invertibleOfLeftInverse (Matrix.fromBlocks (⅟ A) (-(⅟ A * B * ⅟ D)) 0 ⅟ D) ⋯

Instances For

source
def Matrix.fromBlocksZero₁₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] :
Invertible (fromBlocks A 0 C D)

A lower-block-triangular matrix is invertible if its diagonal is.

Equations

- A.fromBlocksZero₁₂Invertible C D = (Matrix.fromBlocks A 0 C D).invertibleOfLeftInverse (Matrix.fromBlocks (⅟ A) 0 (-(⅟ D * C * ⅟ A)) ⅟ D) ⋯

Instances For

source
theorem Matrix.invOf_fromBlocks_zero₂₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible A] [Invertible D] [Invertible (fromBlocks A B 0 D)] :
⅟(fromBlocks A B 0 D) = fromBlocks (⅟ A) (-(⅟ A * B * ⅟ D)) 0 ⅟ D
source
theorem Matrix.invOf_fromBlocks_zero₁₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible D] [Invertible (fromBlocks A 0 C D)] :
⅟(fromBlocks A 0 C D) = fromBlocks (⅟ A) 0 (-(⅟ D * C * ⅟ A)) ⅟ D
source
def Matrix.invertibleOfFromBlocksZero₂₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) [Invertible (fromBlocks A B 0 D)] :
Invertible A × Invertible D

Both diagonal entries of an invertible upper-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).

Equations

- A.invertibleOfFromBlocksZero₂₁Invertible B D = (A.invertibleOfLeftInverse (⅟(Matrix.fromBlocks A B 0 D)).toBlocks₁₁ ⋯, D.invertibleOfRightInverse (⅟(Matrix.fromBlocks A B 0 D)).toBlocks₂₂ ⋯)

Instances For

source
def Matrix.invertibleOfFromBlocksZero₁₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) [Invertible (fromBlocks A 0 C D)] :
Invertible A × Invertible D

Both diagonal entries of an invertible lower-block-triangular matrix are invertible (by reading off the diagonal entries of the inverse).

Equations

- A.invertibleOfFromBlocksZero₁₂Invertible C D = (A.invertibleOfRightInverse (⅟(Matrix.fromBlocks A 0 C D)).toBlocks₁₁ ⋯, D.invertibleOfLeftInverse (⅟(Matrix.fromBlocks A 0 C D)).toBlocks₂₂ ⋯)

Instances For

source
def Matrix.fromBlocksZero₂₁InvertibleEquiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) :
Invertible (fromBlocks A B 0 D) ≃ Invertible A × Invertible D

`invertibleOfFromBlocksZero₂₁Invertible` and `Matrix.fromBlocksZero₂₁Invertible` form an equivalence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Matrix.fromBlocksZero₁₂InvertibleEquiv {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) :
Invertible (fromBlocks A 0 C D) ≃ Invertible A × Invertible D

`invertibleOfFromBlocksZero₁₂Invertible` and `Matrix.fromBlocksZero₁₂Invertible` form an equivalence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Matrix.isUnit_fromBlocks_zero₂₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α} :
IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D

An upper block-triangular matrix is invertible iff both elements of its diagonal are.

This is a propositional form of `Matrix.fromBlocksZero₂₁InvertibleEquiv`.

source
@[simp]
theorem Matrix.isUnit_fromBlocks_zero₁₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {C : Matrix n m α} {D : Matrix n n α} :
IsUnit (fromBlocks A 0 C D) ↔ IsUnit A ∧ IsUnit D

A lower block-triangular matrix is invertible iff both elements of its diagonal are.

This is a propositional form of `Matrix.fromBlocksZero₁₂InvertibleEquiv` forms an `iff`.

source
theorem Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α) (hAD : IsUnit A ↔ IsUnit D) :
(fromBlocks A B 0 D)⁻¹ = fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹

An expression for the inverse of an upper block-triangular matrix, when either both elements of diagonal are invertible, or both are not.

source
theorem Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α) (hAD : IsUnit A ↔ IsUnit D) :
(fromBlocks A 0 C D)⁻¹ = fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹

An expression for the inverse of a lower block-triangular matrix, when either both elements of diagonal are invertible, or both are not.

### 2×2 block matrices #

#### General 2×2 block matrices #

source
def Matrix.fromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (A - B * ⅟ D * C)] :
Invertible (fromBlocks A B C D)

A block matrix is invertible if the bottom right corner and the corresponding Schur complement is.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Matrix.fromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (D - C * ⅟ A * B)] :
Invertible (fromBlocks A B C D)

A block matrix is invertible if the top left corner and the corresponding Schur complement is.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Matrix.invOf_fromBlocks₂₂_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (A - B * ⅟ D * C)] [Invertible (fromBlocks A B C D)] :
⅟(fromBlocks A B C D) = fromBlocks (⅟(A - B * ⅟ D * C)) (-(⅟(A - B * ⅟ D * C) * B * ⅟ D)) (-(⅟ D * C * ⅟(A - B * ⅟ D * C))) (⅟ D + ⅟ D * C * ⅟(A - B * ⅟ D * C) * B * ⅟ D)
source
theorem Matrix.invOf_fromBlocks₁₁_eq {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (D - C * ⅟ A * B)] [Invertible (fromBlocks A B C D)] :
⅟(fromBlocks A B C D) = fromBlocks (⅟ A + ⅟ A * B * ⅟(D - C * ⅟ A * B) * C * ⅟ A) (-(⅟ A * B * ⅟(D - C * ⅟ A * B))) (-(⅟(D - C * ⅟ A * B) * C * ⅟ A)) ⅟(D - C * ⅟ A * B)
source
def Matrix.invertibleOfFromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] [Invertible (fromBlocks A B C D)] :
Invertible (A - B * ⅟ D * C)

If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.

Equations

- A.invertibleOfFromBlocks₂₂Invertible B C D = ((A - B * ⅟ D * C).invertibleOfFromBlocksZero₁₂Invertible 0 D).1

Instances For

source
def Matrix.invertibleOfFromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] [Invertible (fromBlocks A B C D)] :
Invertible (D - C * ⅟ A * B)

If a block matrix is invertible and so is its bottom left element, then so is the corresponding Schur complement.

Equations

- A.invertibleOfFromBlocks₁₁Invertible B C D = D.invertibleOfFromBlocks₂₂Invertible C B A

Instances For

source
def Matrix.invertibleEquivFromBlocks₂₂Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :
Invertible (fromBlocks A B C D) ≃ Invertible (A - B * ⅟ D * C)

`Matrix.invertibleOfFromBlocks₂₂Invertible` and `Matrix.fromBlocks₂₂Invertible` as an equivalence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Matrix.invertibleEquivFromBlocks₁₁Invertible {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] :
Invertible (fromBlocks A B C D) ≃ Invertible (D - C * ⅟ A * B)

`Matrix.invertibleOfFromBlocks₁₁Invertible` and `Matrix.fromBlocks₁₁Invertible` as an equivalence.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
theorem Matrix.isUnit_fromBlocks_iff_of_invertible₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} [Invertible D] :
IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟ D * C)

If the bottom-left element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding Schur complement is.

source
theorem Matrix.isUnit_fromBlocks_iff_of_invertible₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α} {D : Matrix n n α} [Invertible A] :
IsUnit (fromBlocks A B C D) ↔ IsUnit (D - C * ⅟ A * B)

If the top-right element of a block matrix is invertible, then the whole matrix is invertible iff the corresponding Schur complement is.

### Lemmas about `Matrix.det` #

source
theorem Matrix.det_fromBlocks₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible A] :
(fromBlocks A B C D).det = A.det * (D - C * ⅟ A * B).det

Determinant of a 2×2 block matrix, expanded around an invertible top left element in terms of the Schur complement.

source
@[simp]
theorem Matrix.det_fromBlocks_one₁₁ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) :
(fromBlocks 1 B C D).det = (D - C * B).det
source
theorem Matrix.det_fromBlocks₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) (D : Matrix n n α) [Invertible D] :
(fromBlocks A B C D).det = D.det * (A - B * ⅟ D * C).det

Determinant of a 2×2 block matrix, expanded around an invertible bottom right element in terms of the Schur complement.

source
@[simp]
theorem Matrix.det_fromBlocks_one₂₂ {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) :
(fromBlocks A B C 1).det = (A - B * C).det
source
theorem Matrix.det_one_add_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
(1 + A * B).det = (1 + B * A).det

The Weinstein–Aronszajn identity. Note the `1` on the LHS is of shape m×m, while the `1` on the RHS is of shape n×n.

source
theorem Matrix.det_mul_add_one_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
(A * B + 1).det = (B * A + 1).det

Alternate statement of the Weinstein–Aronszajn identity

source
theorem Matrix.det_one_sub_mul_comm {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] (A : Matrix m n α) (B : Matrix n m α) :
(1 - A * B).det = (1 - B * A).det
source
theorem Matrix.det_one_add_replicateCol_mul_replicateRow {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] (u v : m → α) :
(1 + replicateCol ι u * replicateRow ι v).det = 1 + v ⬝ᵥ u

A special case of the Matrix determinant lemma for when `A = I`.

source
theorem Matrix.det_add_replicateCol_mul_replicateRow {m : Type u_2} {α : Type u_4} [Fintype m] [DecidableEq m] [CommRing α] {ι : Type u_5} [Unique ι] {A : Matrix m m α} (hA : IsUnit A.det) (u v : m → α) :
(A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det

The Matrix determinant lemma

TODO: show the more general version without `hA : IsUnit A.det` as `(A + replicateCol u * replicateRow v).det = A.det + v ⬝ᵥ (adjugate A) *ᵥ u`.

source
theorem Matrix.det_add_mul {m : Type u_2} {n : Type u_3} {α : Type u_4} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α) (hA : IsUnit A.det) :
(A + U * V).det = A.det * (1 + V * A⁻¹ * U).det

A generalization of the Matrix determinant lemma