Finite product of modules is a coproduct

Stream: Is there code for X?

[Chris Hughes]

I'm looking for something saying that X -> M is the coproduct of copies of M when X is finite, i.e. I define maps into N by defining #X maps M -> N.

[Eric Wieser]

docs#inear_equiv.Pi_congr_right is close, right?

[Matthew Ballard]

docs#Module.category_theory.limits.has_finite_biproducts ?

[Eric Wieser]

Are you looking for the category_theory statement or the regular algebra one?

[Chris Hughes]

Eric Wieser said:

docs#inear_equiv.Pi_congr_right is close, right?

No, that's true in any category, the thing I want is particular to categories with biproducts. I'm trying not to import category theory, so I just want an algebraic thing.

[Eric Wieser]

docs#direct_sum.to_module is another contender, if you're willing to hand wave over pi types vs direct sums

[Eric Wieser]

And it's clones docs#dfinsupp.lsum and docs#finsupp.lsum

[Chris Hughes]

Eric Wieser said:

docs#direct_sum.to_module is another contender, if you're willing to hand wave over pi types vs direct sums

I'm not, I basically want the fact that pi-types are isomorphic to finite sums.

[Eric Wieser]

docs#dfinsupp.equiv_fun_on_fintype does the hand-wave, but annoyingly isn't linear

[Chris Hughes]

I'm shocked we don't have this.

[Eric Wieser]

I remember looking for this in the past and being shocked too

[Eric Wieser]

I also don't remember whether I then found it

[Eric Wieser]

https://github.com/leanprover-community/mathlib/pull/11744

[Eric Wieser]

That gives docs#add_monoid_hom.noncomm_pi_coprod

[Eric Wieser]

Aha! docs#linear_map.lsum

[Chris Hughes]

docs#finsupp.linear_equiv_fun_on_finite

[Eric Wieser]

linear_map.lsum : (Π i, φ i →ₗ[R] M) ≃ₗ[S] ((Π i, φ i) →ₗ[R] M) is what you want, right?

[Chris Hughes]

Yes

[Eric Wieser]

Eric Wieser said:

https://github.com/leanprover-community/mathlib/pull/11744

I found this by searching zulip for coprod copi, and then its docstrings had enough breadcrumbs to find what you wanted

[Chris Hughes]

LinearMap.lsum is a bit annoying because I don't care about S linearity, but it's not that bad

[Chris Hughes]

Now I need to define a linearMap out of R by defining a point.

[Eric Wieser]

Chris Hughes said:

LinearMap.lsum is a bit annoying because I don't care about S linearity, but it's not that bad

Setting S = nat is an easy way out, if your R isn't commutative