Zulip Chat Archive

Stream: Is there code for X?

Topic: finsupp is direct sum


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

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

do we have this isomorphism?

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

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

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

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

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

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

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