Zulip Chat Archive

Stream: maths

Topic: copies of matrices


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 15:29):

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

view this post on Zulip Yakov Pechersky (Mar 23 2021 at 15:29):

Abuse fin and cast it down

view this post on Zulip Yakov Pechersky (Mar 23 2021 at 15:31):

docs#matrix.block_diagonal

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:32):

combined with docs#matrix.reindex and docs#fin_prod_fin_equiv

view this post on Zulip 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.

view this post on Zulip 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')

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 23 2021 at 15:43):

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

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:44):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 15:45):

ϕ:VW\phi:V\to W and ψ:VW\psi:V' \to W' gives ϕψ:VRVWRW\phi\otimes\psi : V\otimes_R V' \to W\otimes_R W'. Here V,W,V,WV,W,V',W' are all modules over the same ring RR

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:46):

My hunch is that for linear_map we already have that

view this post on Zulip 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

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:49):

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

view this post on Zulip Julian Külshammer (Mar 23 2021 at 15:52):

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

view this post on Zulip 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

view this post on Zulip 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