Appropriate name (and new symbol) for LSSum

[avekens]

Currently, the "inner (or better: internal?) direct product" (see comment of ~df-lsm) operator is called LSSum (what does this acronym it mean? What does the label fragment "lsm" mean?) and is often called "subgroup sum", which can easily be confused with "group sum". Maybe it should be called "internal direct sum" (see https://en.wikipedia.org/wiki/Direct_sum#Internal_and_external_direct_sums), and the symbol for the operator could be DSum. It should not be called "product", because we have already a definition for internal direct products (DProd, see ~df-dprd). Under certain conditions the direct sum and the direct product are equivalent (are there corresponding gtheorems in set.mm?), but in general they are different (see Wikipedia Direct_sum and Direct_product, or https://mathworld.wolfram.com/DirectProduct.html).

In PR #3724, the following remarks were made:

• @benjub: ( LSSum G ) is simply the group sum (or magma law) considered on subsets (in other words, it is the associated "direct image" operation). So I would simply say "the group sum (magma law) as an operation on subsets".
• @savask: I think the comment could indeed be something like "Define a product of subsets in a group". Calling it an inner direct product (or sum) is misleading, since df-lsm doesn't even seem to assume its operands to be subgroups. In group theory one often uses the term "direct product" for all groups and "direct sum" specifically for abelian groups (although even in that case the "product" term can be used). I think set.mm should try to adhere to that convention.

[icecream17]

Perhaps it stands for "linear sum": https://math.stackexchange.com/questions/4665593/linear-sum-of-intersections-of-submodules

[benjub]

I had a look at https://us.metamath.org/mpeuni/df-lsm.html, which brought the question of clearly naming https://us.metamath.org/mpeuni/df-plusg.html. I propose:

  $( Definition of the group-like operation of an extensible structure (see
     ~ df-struct ).  It is called "group-like" since when the structure is 
     group-like, like a magma, semigroup, monoid or group, this is the
     composition law of that structure.  It is written additively since when
     the structure is ring-like, it is the addition of that structure.
  df-plusg $a |- +g = Slot 2 $.
...
  $( Definition of the group-like operation on subsets of an extensible
     structure.  This is the version on subsets of the group-like operation 
     defined in ~ df-plusg .
  df-lsm $a |- LSSum = ( w e. _V |->

[avekens]

I found some hints in the Google group, see https://groups.google.com/g/metamath/c/tHXmipm9wxI/m/GrwBa0iSBQAJ (28-Apr-2016 by @digama0 ):

The internal direct product (or direct sum) of two subgroups already exists: it was called "subspace sum", LSSum, which was originally intended for use in left modules, but also applies to general groups with no modification.

So LSSumseems to mean "left subspace sum".

[tirix]

I'd like to propose "sumset" as this is what I came up with rather independently with #3787 .

For me the direct product or direct sums are operations on structures, while the operation in question here is an operation on sets. I don't like the "direct product" naming (and "inner product" is again something else), because for me this results in pairs of elements, with the pairwise operation.

Maybe the term sumset (as-is or with proper capitals) could be used in naming the function/operator instead of LSSum.

Wikipedia also mentions "Minkowski addition", which is the same operation on Euclidean spaces, this could be mentioned in the comment, but I would not use it for naming.