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 = fromCols 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]

def Matrix.fromCols {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₂)]

def Matrix.toCols₁ {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

def Matrix.toCols₂ {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

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

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

@[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₂ (Sum.inl i) 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₂ (Sum.inr i) j = A₂ i j

@[simp]

theorem Matrix.fromCols_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₁.fromCols A₂ i (Sum.inl j) = A₁ i j

@[simp]

theorem Matrix.fromCols_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₁.fromCols A₂ i (Sum.inr j) = 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 (Sum.inl 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 (Sum.inr i) 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.toCols₁_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.toCols₁ i j = A i (Sum.inl j)

@[simp]

theorem Matrix.toCols₂_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.toCols₂ i j = A i (Sum.inr j)

@[simp]

theorem Matrix.toCols₁_fromCols {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₁.fromCols A₂).toCols₁ = A₁

@[simp]

theorem Matrix.toCols₂_fromCols {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₁.fromCols A₂).toCols₂ = A₂

@[simp]

theorem Matrix.fromCols_toCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) : A.toCols₁.fromCols A.toCols₂ = 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 fromRows

theorem Matrix.fromCols_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} : Function.Injective2 fromCols

theorem Matrix.fromCols_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₁.fromCols A₂ = B₁.fromCols 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_fromCols {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₁.fromCols A₂).transpose = A₁.transpose.fromRows A₂.transpose

A column partitioned matrix when transposed gives a row partitioned matrix with columns of the initial matrix transposed 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.fromCols A₂.transpose

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

theorem Matrix.fromRows_map {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) {R' : Type u_8} (f : R → R') : (A₁.fromRows A₂).map f = (A₁.map f).fromRows (A₂.map f)

theorem Matrix.fromCols_map {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) {R' : Type u_8} (f : R → R') : (A₁.fromCols A₂).map f = (A₁.map f).fromCols (A₂.map f)

@[simp]

theorem Matrix.fromRows_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) : -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

Negating a matrix partitioned by rows is equivalent to negating each of the rows.

@[simp]

theorem Matrix.fromCols_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) : -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

Negating a matrix partitioned by columns is equivalent to negating each of the columns.

@[simp]

theorem Matrix.fromCols_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₂₁).fromCols (B₁₂.fromRows B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

@[simp]

theorem Matrix.fromRows_fromCols_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₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

@[simp]

theorem Matrix.fromRows_mulVec {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) : (A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)

@[simp]

theorem Matrix.vecMul_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) : vecMul v (B₁.fromCols B₂) = Sum.elim (vecMul v B₁) (vecMul v B₂)

@[simp]

theorem Matrix.sumElim_vecMul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R) (v₂ : m₂ → R) : vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = vecMul v₁ B₁ + vecMul v₂ B₂

@[deprecated Matrix.sumElim_vecMul_fromRows (since := "2025-02-21")]

theorem Matrix.sum_elim_vecMul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R) (v₂ : m₂ → R) : vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = vecMul v₁ B₁ + vecMul v₂ B₂

Alias of Matrix.sumElim_vecMul_fromRows.

@[simp]

theorem Matrix.fromCols_mulVec_sumElim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) : (A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂

@[deprecated Matrix.fromCols_mulVec_sumElim (since := "2025-02-21")]

theorem Matrix.fromCols_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) : (A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂

Alias of Matrix.fromCols_mulVec_sumElim.

@[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} [Semiring R] [Fintype n] (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_fromCols {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) : A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

@[simp]

theorem Matrix.fromRows_zero {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] : fromRows 0 0 = 0

@[simp]

theorem Matrix.fromCols_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] : fromCols 0 0 = 0

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

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

theorem Matrix.fromCols_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [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₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

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

theorem Matrix.fromCols_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} [Semiring R] [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₁.fromCols A₂ * fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

A column partitioned matrix multipiled by a block matrix results in a column partitioned 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} [Semiring R] [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) : fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix.

theorem Matrix.fromCols_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [CommRing R] [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq 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₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols 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 fromCols A₁ A₂ and fromRows B₁ B₂ are "square".

theorem Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [CommRing R] [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p] (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₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

The lemma fromCols_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_fromCols_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₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

A column partitioned 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_fromCols_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.fromCols A₂.conjTranspose

A row partitioned 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.