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]

implicit n

[fredrik-bakke]

implicit n

[fredrik-bakke]

implicit n

[fredrik-bakke]

Can you add a short explanation of what "splitting products" means? I.e.

Given an `n+m`-dimensional vector `f`, the product of its coordinates computes as...

[fredrik-bakke]

Since this file is all about products of finite families of elements, rather than just tuples, I think a better name for this file is products-finite-families-of-elements-commutative-monoids

[fredrik-bakke]

Actually, a better way to organize this is to add a second file about products of finite families of elements where you consider types A with a counting, or a proof that A is finite.

[fredrik-bakke]

Don't forget to add links both ways between these files

[fredrik-bakke]

This subsection should be in the Definitions* section

[fredrik-bakke]

On second thought, this should be factored to a new file.

[fredrik-bakke]

please add an explanation for what splitting products means here as well

[fredrik-bakke]

After splitting up the file:

Suggested change

	The product operation extends the binary multiplication operation on a
	[commutative monoid](group-theory.commutative-monoids.md) `M` to any family of
	elements of `M` indexed by a
	[standard finite type](univalent-combinatorics.standard-finite-types.md), or to
	any [finite type](univalent-combinatorics.finite-types.md).
	We extend the binary multiplication operation on a
	[commutative monoid](group-theory.commutative-monoids.md) `M` to any family of
	elements of `M` indexed by a
	[standard finite type](univalent-combinatorics.standard-finite-types.md).

[fredrik-bakke]

Feel free to also try and jam in a concept macro invocation for "product" Disambiguation="of a family of elements in a commutative monoid over a standard finite type" if you want

[fredrik-bakke]

implicit n

[fredrik-bakke]

implicit n in this file as well?

[fredrik-bakke]

Again, can these n's be made implicit?

[fredrik-bakke]

implicit n?

[fredrik-bakke]

to be consistent with commutative monoids, this file can be split into two: one for tuples and one for finite families of elements

[fredrik-bakke]

Again, to be consistent with commutative monoids, this can also be split into two files.

[lowasser]

I declare this blocked on #1397, so we can get the better names for things.