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