Zulip Chat Archive

Stream: Is there code for X?

Topic: finsupp tensor finsupp


view this post on Zulip 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]
  [add_comm_group M] [module R M] [add_comm_group N] [module R N] :
  (ι  M) [R] (κ  N) ≃ₗ[R] (ι × κ)  (M [R] N) :=
by library_search

view this post on Zulip Kenny Lau (Jun 22 2020 at 13:25):

Do we have this isomorphism?

view this post on Zulip Johan Commelin (Jun 22 2020 at 13:40):

nafaik

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 14:10):

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

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

view this post on Zulip Scott Morrison (Jun 22 2020 at 23:58):

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

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

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