Direct Sums

Stream: new members

[Ben McDonnell]

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]

oh apparently I can just type \oplus - is there any reason this wouldn't do what I expect?

[Johan Commelin]

I am afraid there is a lot of reason to expect that. It is most likely not defined yet.

[Patrick Massot]

Having the notation registered in the VScode extension has nothing to do with defining things in Lean

[Johan Commelin]

what exactly do you want the oplus to mean?

[Johan Commelin]

just the span of the summands, or also the claim that the summands have trivial intersection?

[Chris Hughes]

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]

There's a notion of "internal" direct sums too---do we have that?

[Chris Hughes]

Yes, but it will give a submodule of the direct sum.

[Ben McDonnell]

@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.