This is a continuation of the Interval arithmetics in groups: Pass 1 post.
Let be a binary operation on a set . We will write this operation additively as . Such operation defines another binary operation on on the powerset (set of subsets) of in a natural way: for . The nice thing about is that it inherits interesting properties of : if is commutative, then so is , if is a semigroup, then is also a semigroup, if is a monoid, then is also a monoid, if is a group. then … well, never mind, we don’t need that anyway.
This means that all theorems about adding finite (indexed) collections of semigroup elements (and there are quite a couple in the Semigroup_ZF theory) can be reused for the operation on subsets of at little additional cost.
The setup for adding group subsets in the Gyula Lakos’s paper is different in that it assumes the existence of neutral element and defines how to add an infinite number of subsets of .
b.) More generally, suppose is a countable indexed family of subsets of . Assume that for all except for finitely many. Only in that case we define the algebraic sum as except for finitely many .
We can do something in that spirit for as well. Namely suppose that
is a monoid and is a an indexed collection of subsets of such that all but finitely many contain the neutral element (denoted ). We can split the index set into two subsets, one called consisting of those for which contains the neutral element, and the rest. Then we can define the sum of the family of subsets of as follows:
where is the set of finite nonempty subsets of and are interpreted as the additive notation for . So what we do is we add all sets that do not contain , but for sets that do contain we sum every finite subcollection and take the union of all sums obtained this way.
This nicely generalizes the concept of adding finite collections of sets of semigroups (where the is empty and there is only the first component of the sum above) and (in contrast to the Lakos’ approach) does not require selecting monoid elements from infinite collections of subsets of , i.e. does not require the axiom of choice.
Tags: formalized mathematics