Stream: new members
Topic: Direct Sums
Ben McDonnell (Jun 01 2019 at 10:22):
Hi, I've been typing away at some representation theory, but I'm stuck with direct sums. I have a module M and submodules L and N.
I would like to say that M = L \oplus N. How do I do this?
Ben McDonnell (Jun 01 2019 at 10:41):
oh apparently I can just type \oplus - is there any reason this wouldn't do what I expect?
Johan Commelin (Jun 01 2019 at 10:42):
I am afraid there is a lot of reason to expect that. It is most likely not defined yet.
Patrick Massot (Jun 01 2019 at 10:42):
Having the notation registered in the VScode extension has nothing to do with defining things in Lean
Johan Commelin (Jun 01 2019 at 10:45):
what exactly do you want the
oplus to mean?
Johan Commelin (Jun 01 2019 at 10:46):
just the span of the summands, or also the claim that the summands have trivial intersection?
Chris Hughes (Jun 01 2019 at 10:46):
I think you have to just say they're isomorphic.
L \times N \~-\l M
oplus will give you the sum of types, you want the cartesian product of types.
Keeley Hoek (Jun 01 2019 at 10:56):
There's a notion of "internal" direct sums too---do we have that?
Chris Hughes (Jun 01 2019 at 11:05):
Yes, but it will give a submodule of the direct sum.
Ben McDonnell (Jun 01 2019 at 13:30):
@Chris Hughes ok, I see now. The direct sum of modules is the product, which is then given a module structure. And
oplus is basically just the disjoint union.
Last updated: May 16 2021 at 20:13 UTC