Concatenate matrices

Stream: new members

[Aron Erben]

Hello, I would like to concatenate two matrices together column wise, like in the following example:

import data.matrix.basic
import data.real.basic

variables
  {n p₁ p₂ : ℕ}
  (X₁ : matrix (fin n) (fin p₁) ℝ)
  (X₂ : matrix (fin n) (fin p₂) ℝ)
  (X : matrix (fin n) (fin (p₁ + p₂)) ℝ)
  (h : X = (X₁ <> X₂))

<> here represents concatenation, is there a function that does that? I'm aware matrices are functions, so I would have to concatenate their domains and ranges, right?

[Callum Cassidy-Nolan]

I didn't see the method for that, but if you need to implement it you can use this idea:
https://i.imgur.com/nspxD5K.jpg

[Eric Wieser]

This works:

def matrix.fin_append_cols
  {n p₁ p₂ : ℕ}
  (X₁ : matrix (fin n) (fin p₁) ℝ)
  (X₂ : matrix (fin n) (fin p₂) ℝ) : matrix (fin n) (fin (p₁ + p₂)) ℝ
| i := @fin.add_cases _ _ (λ i, ℝ) (X₁ i) (X₂ i)

[Eric Wieser]

Or a more general way:

import data.matrix.basic
import data.real.basic
import logic.equiv.fin

def matrix.append_cols
  {m n₁ n₂ α : Type}
  (X₁ : matrix m n₁ α)
  (X₂ : matrix m n₂ α) : matrix m (n₁ ⊕ n₂) α
| i := sum.elim (X₁ i) (X₂ i)

example
  {n p₁ p₂ : ℕ}
  (X₁ : matrix (fin n) (fin p₁) ℝ)
  (X₂ : matrix (fin n) (fin p₂) ℝ) : matrix (fin n) (fin (p₁ + p₂)) ℝ :=
(X₁.append_cols X₂).minor id fin_sum_fin_equiv.symm

[Eric Wieser]

You might be interested in docs#matrix.from_blocks