Sums and products over arbitrary finite types

[lowasser]

In preparation for polynomials and formal power series, most notably multiplication of formal power series (#1357), this starts digging into sums over arbitrary finite types, and generalizes from sums on e.g. semirings to products on monoids -- mostly commutative monoids, since they're the ones where arbitrary finite sums make sense.

There is some tension with naming over whether group-theory.products-monoids should indicate the monoid on the Cartesian product of two other monoids, or products of elements in a monoid. Since monoids (and groups in general) use multiplicative terminology, we can't get away with what rings have done by differentiating sums and products. (And we don't have any support for products of elements of rings, either, though the generalization to commutative monoids is intended to make that possible down the road.)

This is marked a draft because there's one last thing I want to prove, which is that you can split sums over coproducts of arbitrary finite types.

[fredrik-bakke]

There is some tension with naming over whether group-theory.products-monoids should indicate the monoid on the Cartesian product of two other monoids, or products of elements in a monoid. Since monoids (and groups in general) use multiplicative terminology, we can't get away with what rings have done by differentiating sums and products. (And we don't have any support for products of elements of rings, either, though the generalization to commutative monoids is intended to make that possible down the road.)

Some patterns we've used elsewhere to differentiate are the following:

1. In foundation we use "cartesian product" for the construction taking the cartesian product of two (underlying carrier) types.
2. In category-theory we write "products of categories" and "products in categories" to distinguish between two notions of product (*although both are about products of objects in some category, not about multiplication operations in your sense).
3. For Minkowski products we used "Minkowski multiplication" to disambiguate from products of carrier types.

Depending on the generality of the relevant binary operation (i.e., is it associative, does it distribute over the underlying binary operation?), you might want to go with simply "binary operations on monoids", or something other than "product".

[fredrik-bakke]

I think "cartesian product" may be appropriate in this setting, to disambiguate from the "free product of monoids" which, perhaps counterintuitively, is the coproduct in the category of monoids.

[lowasser]

FWIW, I discovered that a very early attempt at the precise operation we want already existed in group-theory.products-of-tuples-of-elements-commutative-monoids.lagda.md. I have moved all the logic there and adopted the existing naming conventions there.

[fredrik-bakke]

Hmm, I suppose actually our linear-algebra namespace is better described as finite-dimensional-linear-algebra, since that is all it supports! The more general concept of a module over a ring, which allows for vectors in arbitrary dimensions, can be found in ring-theory for instance.

[fredrik-bakke]

I suppose, in computer science, the term "vector" is used for a list of a specified finite length, but this conflicts with the mathematical concept of a vector as an element of a vector space. Anyways, these are just random thoughts.

[fredrik-bakke]

Neither terminology "zero" nor "unit" vector works here, since you've adopted the multiplicative terminology for this file.

[lowasser]

Actually -- perhaps we should name this the one vector? That isn't nearly so overloaded.

[fredrik-bakke]

That's also a possibility