Products, powers and idempotents of block matrices

The difference of the two products of block matrices can be computed block by block. Matrix.fromBlocks_mul_sub_mul records this calculation without requiring an associative or unital coefficient ring.

The block-diagonal matrix Matrix.fromBlocks e 0 0 f is the direct sum of the square matrices e and f. It is idempotent when e and f are, which is how direct sums of idempotent matrices, and hence the addition of algebraic K₀, are formed.

Idempotent matrices e and f, possibly of different sizes, are Murray–von Neumann equivalent when e = a * b and f = b * a for rectangular matrices a and b. After normalizing a and b, the block matrix !![1 - e, a; b, 1 - f] is an involution conjugating e ⊕ 0 to 0 ⊕ f. This is how equivalent idempotents, such as those presenting isomorphic projective modules, become conjugate after stabilization.

For an upper two-block matrix, the diagonal blocks of its powers are the powers of the diagonal blocks. Its off-diagonal block is the finite convolution of the powers of the two diagonal blocks with the original off-diagonal block. This holds over semirings, including zeroth powers and empty blocks.

Main results

• Matrix.fromBlocks_zero₂₁_pow: the power formula for an upper two-block matrix.
• Matrix.fromBlocks_mul_sub_mul: the four blocks of a difference of products.
• IsIdempotentElem.fromBlocks_zero₁₂_zero₂₁: the direct sum of idempotent matrices is idempotent.
• Matrix.fromBlocks_one_sub_mul_self_of_mul_eq and Matrix.fromBlocks_one_sub_mul_fromBlocks_mul_fromBlocks_one_sub_of_mul_eq: Murray–von Neumann equivalent idempotents are conjugate after stabilization.

References

• B. Blackadar, K-Theory for Operator Algebras, Chapter III, §4.
• J. Rosenberg, Algebraic K-Theory and Its Applications, Chapter 1.

theorem Matrix.fromBlocks_zero₂₁_pow {R : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m R) (B : Matrix m n R) (D : Matrix n n R) (k : ℕ) : fromBlocks A B 0 D ^ k = fromBlocks (A ^ k) (∑ i ∈ Finset.range k, A ^ i * B * D ^ (k - 1 - i)) 0 (D ^ k)

The power of an upper two-block matrix, with its off-diagonal block given by the finite convolution of the two diagonal-block powers.

theorem Matrix.fromBlocks_mul_sub_mul {m : Type u_1} {n : Type u_2} {R : Type u_3} [Fintype m] [Fintype n] [NonUnitalNonAssocRing R] (A E : Matrix m m R) (B F : Matrix m n R) (C G : Matrix n m R) (D H : Matrix n n R) : fromBlocks A B C D * fromBlocks E F G H - fromBlocks E F G H * fromBlocks A B C D = fromBlocks (A * E + B * G - (E * A + F * C)) (A * F + B * H - (E * B + F * D)) (C * E + D * G - (G * A + H * C)) (C * F + D * H - (G * B + H * D))

The difference of the two products of block matrices, computed in each block.

theorem IsIdempotentElem.fromBlocks_zero₁₂_zero₂₁ {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype m] [Fintype n] [NonUnitalNonAssocSemiring α] {e : Matrix m m α} {f : Matrix n n α} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) : IsIdempotentElem (Matrix.fromBlocks e 0 0 f)

The block-diagonal matrix Matrix.fromBlocks e 0 0 f with idempotent diagonal blocks is idempotent.

theorem Matrix.fromBlocks_one_sub_mul_self_of_mul_eq {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Ring α] {e : Matrix m m α} {f : Matrix n n α} {a : Matrix m n α} {b : Matrix n m α} (hab : a * b = e) (hba : b * a = f) (hea : e * a = a) (hbe : b * e = b) : fromBlocks (1 - e) a b (1 - f) * fromBlocks (1 - e) a b (1 - f) = 1

If a * b = e and b * a = f, with a a left e-multiple and b a right e-multiple, then the block matrix !![1 - e, a; b, 1 - f] is an involution.

theorem Matrix.fromBlocks_one_sub_mul_fromBlocks_mul_fromBlocks_one_sub_of_mul_eq {m : Type u_1} {n : Type u_2} {α : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [Ring α] {e : Matrix m m α} {f : Matrix n n α} {a : Matrix m n α} {b : Matrix n m α} (hab : a * b = e) (hba : b * a = f) (hbe : b * e = b) : fromBlocks (1 - e) a b (1 - f) * fromBlocks e 0 0 0 * fromBlocks (1 - e) a b (1 - f) = fromBlocks 0 0 0 f

Murray–von Neumann equivalent idempotents are stably conjugate. If a * b = e, b * a = f and b * e = b, then conjugating e ⊕ 0 by !![1 - e, a; b, 1 - f] gives 0 ⊕ f. When also e * a = a, this block matrix is an involution, by Matrix.fromBlocks_one_sub_mul_self_of_mul_eq.