## Stream: Is there code for X?

### Topic: finsupp is direct sum

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

import linear_algebra.finsupp linear_algebra.tensor_product

open_locale classical big_operators tensor_product

def finsupp_equiv_direct_sum {R ι M : Sort*} [comm_ring R] [add_comm_group M] [module R M] :
(ι →₀ M) ≃ₗ[R] direct_sum ι (λ i, M) :=
by library_search


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

do we have this isomorphism?

#### Johan Commelin (Jun 22 2020 at 13:40):

Nope... it seems there's a lot of glue missing here, afaik

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

Talking about more stuff that needs to be glued together...

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

We have categorical biproducts for AddCommGroup, but no connection between these and the "by hand" definition of direct sum.

Last updated: May 16 2021 at 05:21 UTC