## Stream: Is there code for X?

### Topic: finsupp tensor finsupp

#### Kenny Lau (Jun 22 2020 at 13:25):

import linear_algebra.finsupp linear_algebra.tensor_product

open_locale classical big_operators tensor_product

def finsupp_tensor_finsupp {R ι κ M N : Sort*} [comm_ring R]
(ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] (ι × κ) →₀ (M ⊗[R] N) :=
by library_search


#### Kenny Lau (Jun 22 2020 at 13:25):

Do we have this isomorphism?

nafaik

#### Kevin Buzzard (Jun 22 2020 at 14:10):

Don't forget to tag it with @[canonical]

#### Aaron Anderson (Jun 22 2020 at 16:27):

I don’t even think we have the corresponding thing with finite-dimensional vectors, although I’ve constructed a linear map each way that should be inverses

#### Scott Morrison (Jun 22 2020 at 23:58):

I think this could be proved for any preadditive monoidal_category with has_biproducts.

#### Scott Morrison (Jun 22 2020 at 23:59):

In one fell swoop you'd provide the same isomorphism for modules over a Lie algebra, or for chain complexes, etc.

#### Scott Morrison (Jun 22 2020 at 23:59):

(I guess you'd do the dfinsupp generalisation.)

Last updated: May 17 2021 at 15:13 UTC