English
Let A, B, C, D be matrices of sizes m×m, m×n, n×m, n×n over a commutative ring α, with D invertible. Then the block matrix fromBlocks(A,B,C,D) is invertible if and only if the Schur complement A − B D^{-1} C is invertible; moreover there is a natural equivalence between these two invertibility properties.
Русский
Пусть A, B, C, D — матрицы размерности m×m, m×n, n×m, n×n над дискретной сферой α, причём D обратима. Тогда блочная матрица fromBlocks(A,B,C,D) обратима тогда и только тогда, когдаSchur-комплемент A − B D^{-1} C обратим; существует естественное биекция между обратимостью блока и обратимостью Schur-комплементa.
LaTeX
$$$\\operatorname{Invertible}(\\mathrm{fromBlocks}(A,B,C,D)) \\simeq\\operatorname{Invertible}(A - B D^{-1} C)$$$
Lean4
/-- `Matrix.invertibleOfFromBlocks₂₂Invertible` and `Matrix.fromBlocks₂₂Invertible` as an
equivalence. -/
def invertibleEquivFromBlocks₂₂Invertible (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)
where
toFun _iABCD := invertibleOfFromBlocks₂₂Invertible _ _ _ _
invFun _i_schur := fromBlocks₂₂Invertible _ _ _ _
left_inv _iABCD := Subsingleton.elim _ _
right_inv _i_schur := Subsingleton.elim _ _
