finsupp tensor finsupp

Stream: Is there code for X?

[Kenny Lau]

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]
  [add_comm_group M] [module R M] [add_comm_group N] [module R N] :
  (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] (ι × κ) →₀ (M ⊗[R] N) :=
by library_search

[Kenny Lau]

Do we have this isomorphism?

[Johan Commelin]

nafaik

[Kevin Buzzard]

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

[Aaron Anderson]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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