New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Appropriate name (and new symbol) for LSSum #3727
Comments
Perhaps it stands for "linear sum": https://math.stackexchange.com/questions/4665593/linear-sum-of-intersections-of-submodules |
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:
|
I found some hints in the Google group, see https://groups.google.com/g/metamath/c/tHXmipm9wxI/m/GrwBa0iSBQAJ (28-Apr-2016 by @digama0 ):
So |
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 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. |
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 beDSum
. 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:
( 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".The text was updated successfully, but these errors were encountered: