finsupp is direct sum

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_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]

do we have this isomorphism?

[Johan Commelin]

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

[Scott Morrison]

There is https://github.com/leanprover-community/mathlib/blob/master/src/algebra/category/Group/biproducts.lean#L153

[Scott Morrison]

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

[Scott Morrison]

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