copies of matrices

Stream: maths

[Johan Commelin]

Suppose I have a f : matrix (fin m) (fin n). What is the best way to produce matrix (fin (k * m)) (fin (k * n)) that is just k copies of f along the diagonal, and 0 elsewhere.

[Kevin Buzzard]

Send $(i,j)$ to 0 if i/k != j/k and to f (i % k) (j % k) otherwise?

[Yakov Pechersky]

Abuse fin and cast it down

[Yakov Pechersky]

docs#matrix.block_diagonal

[Eric Wieser]

combined with docs#matrix.reindex and docs#fin_prod_fin_equiv

[Kevin Buzzard]

More generally there is a "tensor product" construction and Johan's question is the how to do the tensor product of f and the k by k identity matrix.

[Eric Wieser]

I guess the general form is

def matrix.prod_to_prod_prod_prod {m n m' n' R R' : Type*} [fintype n] [fintype m] [fintype n'] [fintype m'] :
  (matrix m n R × matrix m' n' R') → matrix (m × m') (n × n') (R × R')
| ⟨f, f'⟩ ⟨i, i'⟩ ⟨j, j'⟩ := (f i j, f' i' j')

[Adam Topaz]

If we only had the right monad instance :(

import data.fin

example : monad (λ α, Σ (n : ℕ), fin n → α) := sorry

[Johan Commelin]

@Eric Wieser I think the natural thing takes values in $R \otimes R'$

[Eric Wieser]

Sure, but you can build R ⊗ R' from R × R' but not vice versa

[Kevin Buzzard]

The thing I was thinking of has R = R'; it is tensor product of linear maps once you choose a basis.

[Kevin Buzzard]

$\phi:V\to W$ and $\psi:V' \to W'$ gives $\phi\otimes\psi : V\otimes_R V' \to W\otimes_R W'$. Here $V,W,V',W'$ are all modules over the same ring $R$

[Eric Wieser]

My hunch is that for linear_map we already have that

[Eric Wieser]

docs#linear_map.prod_map is the prod version, I assume there's an easy way to lift that to a tprod version

[Eric Wieser]

docs#tensor_product.map is the operation you're describing

[Julian Külshammer]

https://en.m.wikipedia.org/wiki/Kronecker_product

[Eric Wieser]

Right, the kronecker product is (matrix.prod_to_prod_prod_prod (f, g)).map (λ x, x.1 * x.2) from my definition above

[Scott Morrison]

We do have tensor products of R-algebras, so someone should give the equivalence in the tensor product version of Eric's statement above.