Invertibility and Schur complements for 2×2 block matrices over general rings

This module establishes invertibility criteria and factorizations for 2×2 block matrices over arbitrary (possibly noncommutative) rings R.

Mathlib's Mathlib.LinearAlgebra.Matrix.SchurComplement proves analogous results (fromBlocks_eq_of_invertible₁₁, isUnit_fromBlocks_iff_of_invertible₁₁, isUnit_fromBlocks_zero₂₁) for commutative rings ([CommRing α]). The lemmas here generalize those results to the $D = 0$ cases over arbitrary rings [Ring R], which is required when the matrix entries themselves are matrices (e.g. in rational circuit evaluations).

Main results

• Matrix.isUnit_fromBlocks_one_zero₂₁: an upper unitriangular block matrix is invertible.
• Matrix.isUnit_fromBlocks_one_zero₁₂: a lower unitriangular block matrix is invertible.
• Matrix.isUnit_fromBlocks_diagonal_iff: a block diagonal matrix is invertible iff both diagonal blocks are.
• Matrix.fromBlocks_zero₂₂_schur_factor: Schur factorization of a block matrix with a zero corner and an invertible corner.
• Matrix.isUnit_fromBlocks_zero₂₂_iff: invertibility of a block matrix with a zero corner via its Schur complement.
• Matrix.inv_smul_mul_smul, Matrix.inv_smul_mul_smul_of_ne_zero: rescaling two matrices by the same invertible scalar cancels in (c • A)⁻¹ * (c • B) = A⁻¹ * B.

References

• [OAI26a]

theorem Matrix.isUnit_fromBlocks_one_zero₂₁ {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (B : Matrix ι κ R) : IsUnit (fromBlocks 1 B 0 1)

An upper unitriangular block matrix is invertible.

theorem Matrix.isUnit_fromBlocks_one_zero₁₂ {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (C : Matrix κ ι R) : IsUnit (fromBlocks 1 0 C 1)

A lower unitriangular block matrix is invertible.

theorem Matrix.isUnit_fromBlocks_diagonal_iff {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A : Matrix ι ι R) (D : Matrix κ κ R) : IsUnit (fromBlocks A 0 0 D) ↔ IsUnit A ∧ IsUnit D

A block diagonal matrix is invertible exactly when both diagonal blocks are.

theorem Matrix.fromBlocks_zero₂₂_schur_factor {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) (hAA' : A * A' = 1) (hA'A : A' * A = 1) : fromBlocks A B C 0 = fromBlocks 1 0 (C * A') 1 * fromBlocks A 0 0 (-C * A' * B) * fromBlocks 1 (A' * B) 0 1

The Schur factorization of a block matrix with a zero corner and an invertible corner.

theorem Matrix.isUnit_fromBlocks_zero₂₂_iff {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (A A' : Matrix ι ι R) (B : Matrix ι κ R) (C : Matrix κ ι R) (hAA' : A * A' = 1) (hA'A : A' * A = 1) : IsUnit (fromBlocks A B C 0) ↔ IsUnit (C * A' * B)

A block matrix with a zero corner and an invertible corner is invertible exactly when its Schur complement is.

theorem Matrix.inv_smul_mul_smul {ι : Type u_2} [Fintype ι] [DecidableEq ι] {S : Type u_4} [CommRing S] {m : Type u_5} (A : Matrix ι ι S) (B : Matrix ι m S) (hA : IsUnit A.det) (c : S) [Invertible c] : (c • A)⁻¹ * c • B = A⁻¹ * B

Rescaling two matrices by the same invertible scalar cancels in (c • A)⁻¹ * (c • B) = A⁻¹ * B when A.det is a unit.

theorem Matrix.inv_smul_mul_smul_of_ne_zero {ι : Type u_2} [Fintype ι] [DecidableEq ι] {K : Type u_4} [Field K] {m : Type u_5} (A : Matrix ι ι K) (B : Matrix ι m K) (hA : A.det ≠ 0) {c : K} (hc : c ≠ 0) : (c • A)⁻¹ * c • B = A⁻¹ * B

Over a field, rescaling two matrices by the same nonzero scalar cancels in (c • A)⁻¹ * (c • B) = A⁻¹ * B when A.det ≠ 0.