Matrix.blockTriangular_inv_of_blockTriangular
theorem Matrix.blockTriangular_inv_of_blockTriangular :
∀ {α : Type u_1} {m : Type u_3} {R : Type v} [inst : CommRing R] {M : Matrix m m R} {b : m → α}
[inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : LinearOrder α] [inst_4 : Invertible M],
M.BlockTriangular b → M⁻¹.BlockTriangular b
The theorem `Matrix.blockTriangular_inv_of_blockTriangular` states that for any given type `α` (indexed by `m`), a commutative ring `R`, a matrix `M` of type `Matrix m m R` indexed by `m`, and a function `b` mapping from `m` to `α`, if `M` is block triangular (as determined by the function `b`), then the inverse of `M` is also block triangular (also determined by `b`). This is under the conditions that the equality within type `m` is decidable, `m` represents a finite type, there is a linear order on `α`, and that `M` is invertible.
More concisely: If `M` is a block triangular matrix over a commutative ring `R` with finite index type `m`, and `b` is a function mapping `m` to some linearly ordered type `α`, then `M` invertible implies `M⁻¹` is also block triangular with respect to `b`.
|
Matrix.toBlock_inverse_eq_zero
theorem Matrix.toBlock_inverse_eq_zero :
∀ {α : Type u_1} {m : Type u_3} {R : Type v} [inst : CommRing R] {M : Matrix m m R} {b : m → α}
[inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : LinearOrder α] [inst_4 : Invertible M],
M.BlockTriangular b → ∀ (k : α), (M⁻¹.toBlock (fun i => k ≤ b i) fun i => b i < k) = 0
This theorem states that for a given block-triangular matrix `M` over a commutative ring `R`, indexed by type `m`, and a map `b` from `m` to some type `α` that has a linear order defined on it, if `M` has a defined inverse, then any lower-left subblock of the inverse of `M` is a zero matrix. This subblock is defined by the condition that the block index `k` is less than or equal to the image of `i` under `b` for row indices and less than the image of `i` under `b` for column indices. This theorem is the first step towards proving that the inverse of a block-triangular matrix still maintains the block-triangular form.
More concisely: If `M` is a block-triangular matrix over a commutative ring `R` with a defined inverse, then the subblock of `M`^{-1} indexed by `i` and `j` with `i <_b j`, where `b` is a map from the index type of `M` to some type with a linear order, is the zero matrix.
|
Matrix.BlockTriangular.inv_toBlock
theorem Matrix.BlockTriangular.inv_toBlock :
∀ {α : Type u_1} {m : Type u_3} {R : Type v} [inst : CommRing R] {M : Matrix m m R} {b : m → α}
[inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : LinearOrder α] [inst_4 : Invertible M],
M.BlockTriangular b →
∀ (k : α),
(M.toBlock (fun i => b i < k) fun i => b i < k)⁻¹ = M⁻¹.toBlock (fun i => b i < k) fun i => b i < k
The theorem `Matrix.BlockTriangular.inv_toBlock` states that for any commutative ring `R`, any type `m` and type `α` with linear order, a block-triangular matrix `M` with entries from `R` and rows indexed by `m`, a function `b` from `m` to `α`, assuming that `m` has decidable equality and is finite, and given that `M` is block-triangular with respect to `b`, for any `k` in `α`, the inverse of the upper-left subblock of `M` obtained by taking rows and columns for which `b i` is less than `k`, is equal to the corresponding upper-left subblock of the inverse of `M`. The theorem assumes that `M` is invertible.
More concisely: For any commutative ring R, finite and linearly ordered type α, block-triangular matrix M over R with respect to a function b from m to α, if M is invertible, then the upper-left subblock of M^(-1) corresponding to indices i with b i < k is equal to the inverse of the upper-left subblock of M with respect to the same indices.
|