# Block Matrices from Rows and Columns #

This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as A = fromColumns A₁ A₂ the concatenation of two matrices with the same column indices can be expressed as B = fromRows B₁ B₂.

We then provide a few lemmas that deal with the products of these with each other and with block matrices

## Tags #

column matrices, row matrices, column row block matrices

def Matrix.fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
Matrix (m₁ m₂) n R

Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a bigger matrix indexed by [(m₁ ⊕ m₂) × N]

Equations
• A₁.fromRows A₂ = Matrix.of (Sum.elim A₁ A₂)
Instances For
def Matrix.fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
Matrix m (n₁ n₂) R

Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

Equations
• B₁.fromColumns B₂ = Matrix.of fun (i : m) => Sum.elim (B₁ i) (B₂ i)
Instances For
def Matrix.toColumns₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) :
Matrix m n₁ R

Given a column partitioned matrix extract the first column

Equations
• A.toColumns₁ = Matrix.of fun (i : m) (j : n₁) => A i ()
Instances For
def Matrix.toColumns₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) :
Matrix m n₂ R

Given a column partitioned matrix extract the second column

Equations
• A.toColumns₂ = Matrix.of fun (i : m) (j : n₂) => A i ()
Instances For
def Matrix.toRows₁ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) :
Matrix m₁ n R

Given a row partitioned matrix extract the first row

Equations
• A.toRows₁ = Matrix.of fun (i : m₁) (j : n) => A () j
Instances For
def Matrix.toRows₂ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) :
Matrix m₂ n R

Given a row partitioned matrix extract the second row

Equations
• A.toRows₂ = Matrix.of fun (i : m₂) (j : n) => A () j
Instances For
@[simp]
theorem Matrix.fromRows_apply_inl {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₁) (j : n) :
A₁.fromRows A₂ () j = A₁ i j
@[simp]
theorem Matrix.fromRows_apply_inr {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₂) (j : n) :
A₁.fromRows A₂ () j = A₂ i j
@[simp]
theorem Matrix.fromColumns_apply_inl {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
A₁.fromColumns A₂ i () = A₁ i j
@[simp]
theorem Matrix.fromColumns_apply_inr {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :
A₁.fromColumns A₂ i () = A₂ i j
@[simp]
theorem Matrix.toRows₁_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) (i : m₁) (j : n) :
A.toRows₁ i j = A () j
@[simp]
theorem Matrix.toRows₂_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) (i : m₂) (j : n) :
A.toRows₂ i j = A () j
@[simp]
theorem Matrix.toRows₁_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
(A₁.fromRows A₂).toRows₁ = A₁
@[simp]
theorem Matrix.toRows₂_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
(A₁.fromRows A₂).toRows₂ = A₂
@[simp]
theorem Matrix.toColumns₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) (i : m) (j : n₁) :
A.toColumns₁ i j = A i ()
@[simp]
theorem Matrix.toColumns₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) (i : m) (j : n₂) :
A.toColumns₂ i j = A i ()
@[simp]
theorem Matrix.toColumns₁_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
(A₁.fromColumns A₂).toColumns₁ = A₁
@[simp]
theorem Matrix.toColumns₂_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
(A₁.fromColumns A₂).toColumns₂ = A₂
@[simp]
theorem Matrix.fromColumns_toColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ n₂) R) :
A.toColumns₁.fromColumns A.toColumns₂ = A
@[simp]
theorem Matrix.fromRows_toRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ m₂) n R) :
A.toRows₁.fromRows A.toRows₂ = A
theorem Matrix.fromRows_inj {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} :
Function.Injective2 Matrix.fromRows
theorem Matrix.fromColumns_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} :
Function.Injective2 Matrix.fromColumns
theorem Matrix.fromColumns_ext_iff {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
A₁.fromColumns A₂ = B₁.fromColumns B₂ A₁ = B₁ A₂ = B₂
theorem Matrix.fromRows_ext_iff {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) :
A₁.fromRows A₂ = B₁.fromRows B₂ A₁ = B₁ A₂ = B₂
theorem Matrix.transpose_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
(A₁.fromColumns A₂).transpose = A₁.transpose.fromRows A₂.transpose

A column partioned matrix when transposed gives a row partioned matrix with columns of the initial matrix tranposed to become rows.

theorem Matrix.transpose_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
(A₁.fromRows A₂).transpose = A₁.transpose.fromColumns A₂.transpose

A row partioned matrix when transposed gives a column partioned matrix with rows of the initial matrix tranposed to become columns.

@[simp]
theorem Matrix.fromRows_mulVec {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [] [] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : nR) :
(A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)
@[simp]
theorem Matrix.vecMul_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [] [] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : mR) :
Matrix.vecMul v (B₁.fromColumns B₂) = Sum.elim () ()
@[simp]
theorem Matrix.sum_elim_vecMul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Fintype m₁] [Fintype m₂] [] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁R) (v₂ : m₂R) :
Matrix.vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂
@[simp]
theorem Matrix.fromColumns_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Fintype n₁] [Fintype n₂] [] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁R) (v₂ : n₂R) :
(A₁.fromColumns A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂
@[simp]
theorem Matrix.fromRows_mul {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [] [] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
@[simp]
theorem Matrix.mul_fromColumns {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [] [] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
A * B₁.fromColumns B₂ = (A * B₁).fromColumns (A * B₂)
@[simp]
theorem Matrix.fromRows_zero {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [] :
= 0
@[simp]
theorem Matrix.fromColumns_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [] :
= 0
@[simp]
theorem Matrix.fromColumns_fromRows_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
(B₁₁.fromRows B₂₁).fromColumns (B₁₂.fromRows B₂₂) = B₁₁.fromBlocks B₁₂ B₂₁ B₂₂
@[simp]
theorem Matrix.fromRows_fromColumn_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
(B₁₁.fromColumns B₁₂).fromRows (B₂₁.fromColumns B₂₂) = B₁₁.fromBlocks B₁₂ B₂₁ B₂₂
theorem Matrix.fromRows_mul_fromColumns {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [] [] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
A₁.fromRows A₂ * B₁.fromColumns B₂ = (A₁ * B₁).fromBlocks (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

A row partitioned matrix multiplied by a column partioned matrix gives a 2 by 2 block matrix

theorem Matrix.fromColumns_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Fintype n₁] [Fintype n₂] [] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
A₁.fromColumns A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

A column partitioned matrix mulitplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices

theorem Matrix.fromColumns_mul_fromBlocks {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Fintype m₁] [Fintype m₂] [] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
A₁.fromColumns A₂ * B₁₁.fromBlocks B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromColumns (A₁ * B₁₂ + A₂ * B₂₂)

A column partitioned matrix multipiled by a block matrix results in a column partioned matrix

theorem Matrix.fromBlocks_mul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Fintype n₁] [Fintype n₂] [] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
B₁₁.fromBlocks B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

A block matrix mulitplied by a row partitioned matrix gives a row partitioned matrix

theorem Matrix.fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [] [Fintype n₁] [Fintype n₂] [] [] [] [] (e : n n₁ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 B₁.fromRows B₂ * A₁.fromColumns A₂ = 1

Multiplication of a matrix by its inverse is commutative. This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.

The condition e : n ≃ n₁ ⊕ n₂ states that fromColumns A₁ A₂ and fromRows B₁ B₂ are "square".

theorem Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [] [] [] (p : nProp) [] (A₁ : Matrix n { i : n // p i } R) (A₂ : Matrix n { i : n // ¬p i } R) (B₁ : Matrix { i : n // p i } n R) (B₂ : Matrix { i : n // ¬p i } n R) :
A₁.fromColumns A₂ * B₁.fromRows B₂ = 1 B₁.fromRows B₂ * A₁.fromColumns A₂ = 1

The lemma fromColumns_mul_fromRows_eq_one_comm specialized to the case where the index sets n₁ and n₂, are the result of subtyping by a predicate and its complement.

theorem Matrix.conjTranspose_fromColumns_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
(A₁.fromColumns A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

A column partioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix with the columns of the initial matrix conjugate transposed to become rows.

theorem Matrix.conjTranspose_fromRows_eq_fromColumns_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
(A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromColumns A₂.conjTranspose

A row partioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix with the rows of the initial matrix conjugate transposed to become columns.