Best practices for block matrices

Stream: mathlib4

[Martin Dvořák]

What are the best practices for block matrices bigger than 2x2 blocks?
In particular, I will probably need 4x2 blocks.
Is any of the following definitions preferred by Mathlib?

import Mathlib.Data.Matrix.ColumnRowPartitioned


variable {R : Type*} {m₁ m₂ m₃ m₄ n₁ n₂ : Type*}
  (A₁₁ : Matrix m₁ n₁ R) (A₁₂ : Matrix m₁ n₂ R)
  (A₂₁ : Matrix m₂ n₁ R) (A₂₂ : Matrix m₂ n₂ R)
  (A₃₁ : Matrix m₃ n₁ R) (A₃₂ : Matrix m₃ n₂ R)
  (A₄₁ : Matrix m₄ n₁ R) (A₄₂ : Matrix m₄ n₂ R)


def B : Matrix (m₁ ⊕ m₂ ⊕ m₃ ⊕ m₄) (n₁ ⊕ n₂) R :=
  (Matrix.fromRows (Matrix.fromColumns A₁₁ A₁₂)
  (Matrix.fromRows (Matrix.fromColumns A₂₁ A₂₂)
  (Matrix.fromRows (Matrix.fromColumns A₃₁ A₃₂)
                   (Matrix.fromColumns A₄₁ A₄₂))))

def C : Matrix (m₁ ⊕ m₂ ⊕ m₃ ⊕ m₄) (n₁ ⊕ n₂) R :=
  Matrix.fromColumns
    (Matrix.fromRows A₁₁ (Matrix.fromRows A₂₁ (Matrix.fromRows A₃₁ A₄₁)))
    (Matrix.fromRows A₁₂ (Matrix.fromRows A₂₂ (Matrix.fromRows A₃₂ A₄₂)))

def D : Matrix (m₁ ⊕ m₂ ⊕ m₃ ⊕ m₄) (n₁ ⊕ n₂) R :=
  Matrix.fromBlocks
    A₁₁ A₁₂
    (Matrix.fromRows A₂₁ (Matrix.fromRows A₃₁ A₄₁)) (Matrix.fromRows A₂₂ (Matrix.fromRows A₃₂ A₄₂))

def E : Matrix ((m₁ ⊕ m₂) ⊕ (m₃ ⊕ m₄)) (n₁ ⊕ n₂) R :=
  Matrix.fromRows
    (Matrix.fromBlocks A₁₁ A₁₂ A₂₁ A₂₂)
    (Matrix.fromBlocks A₃₁ A₃₂ A₄₁ A₄₂)

def F : Matrix ((m₁ ⊕ m₂) ⊕ (m₃ ⊕ m₄)) (n₁ ⊕ n₂) R :=
  Matrix.fromBlocks
    (Matrix.fromRows A₁₁ A₂₁) (Matrix.fromRows A₁₂ A₂₂)
    (Matrix.fromRows A₃₁ A₄₁) (Matrix.fromRows A₃₂ A₄₂)

[Martin Dvořák]

PS: I could maybe write a general definition, but I think it is overkill:

import Mathlib.Data.Matrix.ColumnRowPartitioned


def BigBlockMatrix {R α β : Type*} [Fintype α] [Fintype β] {m : α → Type*} {n : β → Type*}
    (M : Π a : α, Π b : β, Matrix (m a) (n b) R) :
    Matrix (Σ a : α, m a) (Σ b : β, n b) R :=
  Matrix.of
    (fun (⟨_, i⟩ : (Σ a : α, m a)) (⟨_, j⟩ : (Σ b : β, n b)) => M _ _ i j)

[Eric Wieser]

I think the sigma version probably is reasonable

[Eric Wieser]

(though I would recommend not using pattern matching)

[Martin Dvořák]

import Mathlib.Data.Matrix.Basic

def BigBlockMatrix {R α β : Type*} [Fintype α] [Fintype β] {m : α → Type*} {n : β → Type*}
    (M : Π a : α, Π b : β, Matrix (m a) (n b) R) :
    Matrix (Σ a : α, m a) (Σ b : β, n b) R :=
  Matrix.of
    (fun (i : (Σ a : α, m a)) (j : (Σ b : β, n b)) => M i.fst j.fst i.snd j.snd)

[Martin Dvořák]

Eric Wieser said:

I think the sigma version probably is reasonable

Uh, a lot of API will have to be built!
Would you go directly to the big block matrix, or would you rather define generalizations of Matrix.fromRows and Matrix.fromColumns first?

[Eric Wieser]

I guess the latter allows you to use an nary sum in the columns and a binary one in the rows

[Eric Wieser]

I think the convention would be to use primed names to match docs#Matrix.blockDiagonal'