Stream: maths

Topic: copies of matrices

Johan Commelin (Mar 23 2021 at 15:27):

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 (Mar 23 2021 at 15:29):

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

Yakov Pechersky (Mar 23 2021 at 15:29):

Abuse fin and cast it down

Yakov Pechersky (Mar 23 2021 at 15:31):

docs#matrix.block_diagonal

Eric Wieser (Mar 23 2021 at 15:32):

combined with docs#matrix.reindex and docs#fin_prod_fin_equiv

Kevin Buzzard (Mar 23 2021 at 15:33):

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 (Mar 23 2021 at 15:35):

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 (Mar 23 2021 at 15:39):

import data.fin

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


Johan Commelin (Mar 23 2021 at 15:43):

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

Eric Wieser (Mar 23 2021 at 15:44):

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

Kevin Buzzard (Mar 23 2021 at 15:44):

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

Kevin Buzzard (Mar 23 2021 at 15:45):

$\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 (Mar 23 2021 at 15:46):

My hunch is that for linear_map we already have that

Eric Wieser (Mar 23 2021 at 15:48):

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 (Mar 23 2021 at 15:49):

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

Julian Külshammer (Mar 23 2021 at 15:52):

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

Eric Wieser (Mar 23 2021 at 15:54):

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 (Mar 23 2021 at 23:00):

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

Last updated: May 10 2021 at 08:14 UTC