# Zulip Chat Archive

## 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):

#### 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):

If we only had the right monad instance :(

```
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