powers of monoid elements

Johan G. F. Belinfante
2012 February 5

SetDirectory["l:"];  <<  goedel.12feb03a

summary

If  x  is a monoid and  y ∈ range[x], then for every natural number n ∈ ω  there is an element  (y^n) ∈ range[x] called the n-th power of  y.  One can define the n-th power of  y  either by starting with the neutral element e[x]  and repeatedly multiplying on the left with  y, or by repeatedly multiplying on the right with  y.  Because monoids are associative, it makes no difference whether left or right multiplication is used.

a consequence of the associative law

The wrapper  monoid[x] is either a monoid, or the empty set.  In either case, it is an associative function.  As a consequence, left and right multiplications for monoid[x] commute.

Theorem.  Left and right multiplications for monoid[x] commute.

SubstTest[commute, composite[assoc[t], LEFT[y]], 
        composite[assoc[t], RIGHT[z]], t -> monoid[x]] // 
      Reverse

equal[composite[monoid[x_], LEFT[y_], monoid[x_], RIGHT[z_]], 
        composite[monoid[x_], RIGHT[z_], monoid[x_], LEFT[y_]]] := 
      True

the sequence of powers

If  x  is a monoid, and if  y  and  z  are members of  range[x], then the class iterate[x ∘ LEFT[y], {z}]  is the infinite sequence of elements starting with  z  obtained by repeately multiplying on the left with  y.   The n-th member of this sequence is usually denoted by   (y^n) z.  The following theorem allows one to rewrite this sequence in terms of the special case  z = e[x].

Theorem.

Map[
        implies[and[member[y, range[monoid[x]]], 
              member[z, range[monoid[x]]]], #] &, 
        SubstTest[implies, 
          and[equal[composite[w, SUCC], composite[u, w]], 
            equal[image[w, set[0]], v]], 
          equal[composite[w, id[omega]], 
            iterate[u, v]], {u -> composite[monoid[x], LEFT[y]], v -> set[z], 
            w -> composite[monoid[x], RIGHT[z], 
                iterate[composite[monoid[x], LEFT[y]], 
                  set[e[monoid[x]]]]]}]] // Reverse

or[equal[
          composite[monoid[x_], RIGHT[z_], 
            iterate[composite[monoid[x_], LEFT[y_]], set[e[monoid[x_]]]]], 
          iterate[composite[monoid[x_], LEFT[y_]], set[z_]]], 
        not[member[y_, range[monoid[x_]]]], 
        not[member[z_, range[monoid[x_]]]]] := True

Similarly, the class iterate[x ∘ RIGHT[y], {z}]  is the infinite sequence of elements starting with  z  obtained by repeately multiplying on the right with  y.  The n-th member of the latter sequence is usually denoted by   z (y^n).   When  z  is the identity element e[x]  these sequences are equal because the associative law for  x  implies that left multiplication commutes with right multiplication.  These facts have already been established earlier, but at that time the monoid wrapper monoid[x] had not yet been defined.  It is worthwhile to repeat the derivation using this wrapper to witness the advantages of automatic simplifications that take place, and also to slightly improve on the old results by eliminating a redundant literal.

Lemma 1.  An application of the uniqueness theorem for iterate.

Map[implies[member[y, range[monoid[x]]], #] &, 
        SubstTest[implies, 
          and[equal[composite[w, SUCC], composite[u, w]], 
            equal[image[w, set[0]], v]], 
          equal[composite[w, id[omega]], 
            iterate[u, v]], {u -> composite[monoid[x], RIGHT[y]], 
            v -> set[y], 
            w -> composite[monoid[x], RIGHT[y], 
                iterate[composite[monoid[x], RIGHT[y]], 
                  set[e[monoid[x]]]]]}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma 2.  A second application of the uniqueness theorem for iterate.

Map[implies[member[y, range[monoid[x]]], #] &, 
        SubstTest[implies, 
          and[equal[composite[w, SUCC], composite[u, w]], 
            equal[image[w, set[0]], v]], 
          equal[composite[w, id[omega]], 
            iterate[u, v]], {u -> composite[monoid[x], RIGHT[y]], 
            v -> set[y], 
            w -> composite[monoid[x], LEFT[y], 
                iterate[composite[monoid[x], RIGHT[y]], 
                  set[e[monoid[x]]]]]}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma 3.  A third application of the uniqueness theorem for iterate.

SubstTest[implies, 
        and[equal[composite[w, SUCC], composite[u, w]], 
          equal[image[w, set[0]], v]], 
        equal[composite[w, id[omega]], 
          iterate[u, v]], {u -> composite[monoid[x], LEFT[y]], 
          v -> set[e[monoid[x]]], 
          w -> iterate[composite[monoid[x], RIGHT[y]], set[e[monoid[x]]]]}] // 
      Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma 4.  If  y ∈ range[monoid[x]], then two expressions for the sequence of powers of  y  are equal.

Map[not, 
        SubstTest[and, implies[p1, p2], 
          implies[p1, p3],    
          implies[p4, p5], 
          not[implies[p1, p5]], {p1 -> member[y, range[monoid[x]]], 
            p2 -> 
              equal[composite[monoid[x], RIGHT[y], 
                  iterate[composite[monoid[x], RIGHT[y]], 
                    set[e[monoid[x]]]]], 
                iterate[composite[monoid[x], RIGHT[y]], set[y]]], 
            p3 -> 
              equal[composite[monoid[x], LEFT[y], 
                  iterate[composite[monoid[x], RIGHT[y]], 
                    set[e[monoid[x]]]]], 
                iterate[composite[monoid[x], RIGHT[y]], set[y]]], 
            p4 -> 
              equal[composite[monoid[x], LEFT[y], 
                  iterate[composite[monoid[x], RIGHT[y]], 
                    set[e[monoid[x]]]]], 
                composite[monoid[x], RIGHT[y], 
                  iterate[composite[monoid[x], RIGHT[y]], 
                    set[e[monoid[x]]]]]], 
            p5 -> equal[
                iterate[composite[monoid[x], LEFT[y]], set[e[monoid[x]]]], 
                iterate[composite[monoid[x], RIGHT[y]], 
                  set[e[monoid[x]]]]]}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

The literal  y ∈ range[monoid[x]]  in the preceding lemma is redundant.  It will now be removed.

Lemma 5.  The case that  y  is not a member of  range[monoid[x]].

SubstTest[implies, and[empty[u], empty[v]], 
        equal[iterate[u, set[e[monoid[x]]]], 
          iterate[v, set[e[monoid[x]]]]], {u -> 
            composite[monoid[x], LEFT[y]], 
          v -> composite[monoid[x], RIGHT[y]]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.  Two expressions for the sequence of powers are equal.

SubstTest[and, implies[p, q], 
        or[p, q], {p -> 
            and[member[y, range[monoid[x]]], not[empty[monoid[x]]]], 
          q -> equal[
              iterate[composite[monoid[x], LEFT[y]], set[e[monoid[x]]]], 
              iterate[composite[monoid[x], RIGHT[y]], set[e[monoid[x]]]]]}] // 
      MapNotNot

equal[iterate[composite[monoid[x_], LEFT[y_]], set[e[monoid[x_]]]], 
        iterate[composite[monoid[x_], RIGHT[y_]], set[e[monoid[x_]]]]] := 
      True

The monoid wrapper can be removed.

Corollary.  If  x ∈ MONOIDS, then  iterate[x ∘ LEFT[y], {e[x]}] = iterate[x ∘ RIGHT[y], {e[x]}].

SubstTest[implies, equal[x, monoid[t]], 
          equal[iterate[composite[x, LEFT[y]], set[e[x]]], 
            iterate[composite[x, RIGHT[y]], set[e[x]]]], t -> x] // 
        Reverse // MapNotNot

or[equal[iterate[composite[x_, LEFT[y_]], set[e[x_]]], 
          iterate[composite[x_, RIGHT[y_]], set[e[x_]]]], 
        not[member[x_, MONOIDS]]] := True

other basic facts

Theorem.  If  x ∈ MONOIDS, then iterate[monoid[x] ∘ LEFT[y], {z}] is a function.

SubstTest[implies, equal[x, monoid[t]], 
          FUNCTION[iterate[composite[x, LEFT[y]], set[z]]], t -> x] // 
        Reverse // MapNotNot

or[FUNCTION[iterate[composite[x_, LEFT[y_]], set[z_]]], 
        not[member[x_, MONOIDS]]] := True

Theorem.  An analogous result, but with LEFT replaced with RIGHT.

SubstTest[implies, equal[x, monoid[t]], 
          FUNCTION[iterate[composite[x, RIGHT[y]], set[z]]], t -> x] // 
        Reverse // MapNotNot

or[FUNCTION[iterate[composite[x_, RIGHT[y_]], set[z_]]], 
        not[member[x_, MONOIDS]]] := True

A better result will now be derived.

Theorem.  Left multiplication is a unary operation.

SubstTest[member, composite[binop[t], LEFT[y]], UNOPS, 
        t -> monoid[x]] // Reverse

member[composite[monoid[x_], LEFT[y_]], UNOPS] := True

Theorem.  Right multiplication is a unary operation.

SubstTest[member, composite[binop[t], RIGHT[y]], UNOPS, 
        t -> monoid[x]] // Reverse

member[composite[monoid[x_], RIGHT[y_]], UNOPS] := True

The monoid wrapper can be removed.

Corollary.   If  x  is a nonoid, then  x ∘ LEFT[y]  is a unary operation.

SubstTest[implies, equal[x, monoid[t]], 
          member[composite[x, LEFT[y]], UNOPS], t -> x] // Reverse // 
      MapNotNot

or[member[composite[x_, LEFT[y_]], UNOPS], not[member[x_, MONOIDS]]] := 
      True

Corollary.   If  x  is a nonoid, then  x ∘ RIGHT[y]  is a unary operation.

SubstTest[implies, equal[x, monoid[t]], 
          member[composite[x, RIGHT[y]], UNOPS], t -> x] // Reverse // 
      MapNotNot

or[member[composite[x_, RIGHT[y_]], UNOPS], not[member[x_, MONOIDS]]] := 
      True

domain of the power sequence

Theorem.

SubstTest[implies, 
        and[FUNCTION[t], subclass[range[t], domain[t]], 
          member[y, domain[t]]], equal[domain[iterate[t, set[y]]], omega], 
        t -> unop[x]] // Reverse

or[equal[omega, domain[iterate[unop[x_], set[y_]]]], 
        not[member[y_, domain[unop[x_]]]]] := True

Corollary.  If  x  is a unary operation, and  y ∈ domain[x], then  domain[iterate[x, {y}] = ω.

SubstTest[implies, equal[x, unop[t]], 
        or[equal[omega, domain[iterate[x, set[y]]]], 
          not[member[y, domain[x]]]], t -> x] // Reverse

or[equal[omega, domain[iterate[x_, set[y_]]]], not[member[x_, UNOPS]], 
        not[member[y_, domain[x_]]]] := True

This result will now be applied to powers of monoid elements.

Lemma.

SubstTest[member, pair[u, v], cartsq[t], t -> range[monoid[x]]] // 
      Reverse

member[pair[u_, v_], domain[monoid[x_]]] := 
      and[member[u, range[monoid[x]]], 
        member[v, range[monoid[x]]]]

Theorem.  If  y  and  z  are members of  range[monoid[x]], then domain[iterate[monoid[x] ∘ LEFT[y], {z}] = ω.  In other words, the quantity  (y^n) z is defined for every natural number  n.

SubstTest[or, equal[omega, domain[iterate[unop[t], set[z]]]], 
        not[member[z, domain[unop[t]]]], 
        t -> composite[monoid[x], LEFT[y]]] // Reverse

or[equal[omega, 
          domain[iterate[composite[monoid[x_], LEFT[y_]], set[z_]]]], 
        not[member[y_, range[monoid[x_]]]], 
        not[member[z_, range[monoid[x_]]]]] := True

Theorem.  Dual result:  z (y^n) is defined for every natural number  n.

SubstTest[or, equal[omega, domain[iterate[unop[t], set[z]]]], 
        not[member[z, domain[unop[t]]]], 
        t -> composite[monoid[x], RIGHT[y]]] // Reverse

or[equal[omega, 
          domain[iterate[composite[monoid[x_], RIGHT[y_]], set[z_]]]], 
        not[member[y_, range[monoid[x_]]]], 
        not[member[z_, range[monoid[x_]]]]] := True

The monoid wrapper can be removed from each of the above statement.

Corollary.   If  x ∈ MONOIDS  and  y, z ∈ range[x], then   domain[iterate[x ∘ LEFT[y], {z}] = ω.

SubstTest[implies, equal[x, monoid[t]], 
          or[equal[omega, domain[iterate[composite[x, LEFT[y]], set[z]]]], 
            not[member[y, range[x]]], not[member[z, range[x]]]], 
          t -> x] // Reverse // MapNotNot

or[equal[omega, domain[iterate[composite[x_, LEFT[y_]], set[z_]]]], 
        not[member[x_, MONOIDS]], not[member[y_, range[x_]]], 
        not[member[z_, range[x_]]]] := True

Corollary.  If  x ∈ MONOIDS  and  y, z ∈ range[x], then   domain[iterate[x ∘ RIGHT[y], {z}] = ω.

SubstTest[implies, equal[x, monoid[t]], 
          or[equal[omega, domain[iterate[composite[x, RIGHT[y]], set[z]]]], 
            not[member[y, range[x]]], not[member[z, range[x]]]], 
          t -> x] // Reverse // MapNotNot

or[equal[omega, domain[iterate[composite[x_, RIGHT[y_]], set[z_]]]], 
        not[member[x_, MONOIDS]], not[member[y_, range[x_]]], 
        not[member[z_, range[x_]]]] := True

The special case  z = e[x] is of greatest interest.

Corollary.  If  x ∈ MONOIDS  and  y ∈ range[x], then  domain[iterate[x ∘ LEFT[y], {e[x]}] = ω.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
          not[implies[p1, p3]], {p1 -> 
              and[member[x, MONOIDS], member[y, range[x]]], 
            p2 -> member[e[x], range[x]], 
            p3 -> equal[omega, 
                domain[iterate[composite[x, LEFT[y]], set[e[x]]]]]}]] // 
      Reverse

or[equal[omega, domain[iterate[composite[x_, LEFT[y_]], set[e[x_]]]]], 
        not[member[x_, MONOIDS]], not[member[y_, range[x_]]]] := 
      True

the 0-th and 1-st powers

Lemma.

SubstTest[implies, 
        and[FUNCTION[t], equal[image[t, set[u]], set[v]], 
          member[u, domain[t]]], 
        equal[APPLY[t, u], 
          v], {t -> 
            iterate[composite[monoid[x], LEFT[y]], set[e[monoid[x]]]], 
          u -> 0, v -> e[monoid[x]]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.  Simplification rule.

equiv[and[member[x, MONOIDS], not[equal[0, x]]], 
      member[x, MONOIDS]]

and[member[x_, MONOIDS], not[equal[0, x_]]] := 
      member[x, MONOIDS]

Theorem.  If  x ∈ MONOIDS, then  (y^0) = e[x].

SubstTest[implies, equal[x, monoid[t]], 
          or[equal[0, x], 
            equal[APPLY[iterate[composite[x, LEFT[y]], set[e[x]]], 0], 
              e[x]]], t -> x] // Reverse // MapNotNot

or[equal[APPLY[iterate[composite[x_, LEFT[y_]], set[e[x_]]], 0], 
          e[x_]], not[member[x_, MONOIDS]]] := True

Lemma.  (Specialize to the case  n = 1.)

Map[implies[member[y, range[monoid[x]]], #] &, 
        SubstTest[implies, 
          and[FUNCTION[t], equal[image[t, set[u]], set[v]], 
            member[u, domain[t]]], 
          equal[APPLY[t, u], 
            v], {t -> 
              iterate[composite[monoid[x], LEFT[y]], set[e[monoid[x]]]], 
            u -> set[0], v -> y}]] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Lemma.  (Remove the monoid wrapper.)

SubstTest[implies, equal[x, monoid[t]], 
          or[equal[y, 
              APPLY[iterate[composite[x, LEFT[y]], set[e[x]]], set[0]]], 
            not[member[y, range[x]]], 
            not[member[set[0], 
                domain[iterate[composite[x, LEFT[y]], set[e[x]]]]]]], 
          t -> x] // Reverse // MapNotNot

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.   If  x  is a monoid and  y ∈ range[x], then  (y^1) = y.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          implies[and[p1, p3], p4], 
          not[implies[p1, p4]], {p1 -> 
              and[member[x, MONOIDS], member[y, range[x]]], 
            p2 -> 
              equal[omega, 
                domain[iterate[composite[x, LEFT[y]], set[e[x]]]]], 
            p3 -> member[set[0], 
                domain[iterate[composite[x, LEFT[y]], set[e[x]]]]], 
            p4 -> equal[y, 
                APPLY[iterate[composite[x, LEFT[y]], set[e[x]]], set[0]]]}]] // 
      Reverse

or[equal[APPLY[iterate[composite[x_, LEFT[y_]], set[e[x_]]], set[0]], 
          y_], not[member[x_, MONOIDS]], not[member[y_, range[x_]]]] := 
      True

range of the power sequence

Theorem.  A hull formula for the range of the sequence  (y^n) z.

SubstTest[range, iterate[funpart[t], set[z]], 
        t -> composite[monoid[x], LEFT[y]]] // Reverse

range[iterate[composite[monoid[x_], LEFT[y_]], set[z_]]] := 
      hull[invar[composite[monoid[x], LEFT[y]]], set[z]]

Theorem.  A hull formula for the range of the sequence  z (y^n).

SubstTest[range, iterate[funpart[t], set[z]], 
        t -> composite[monoid[x], RIGHT[y]]] // Reverse

range[iterate[composite[monoid[x_], RIGHT[y_]], set[z_]]] := 
      hull[invar[composite[monoid[x], RIGHT[y]]], set[z]]

Lemma.

SubstTest[subclass, range[iterate[t, z]], 
        union[range[t], z], {t -> composite[monoid[x], LEFT[y]], 
          z -> set[e[monoid[x]]]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.  An upper bound for the range.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, 
          w], {u -> hull[invar[composite[monoid[x], LEFT[y]]], 
              set[e[monoid[x]]]], 
          v -> union[image[monoid[x], cart[set[y], V]], set[e[monoid[x]]]], 
          w -> range[monoid[x]]}] // Reverse

subclass[
        hull[invar[composite[monoid[x_], LEFT[y_]]], set[e[monoid[x_]]]], 
        range[monoid[x_]]] := True

Corollary.

SubstTest[implies, equal[x, monoid[t]], 
          subclass[hull[invar[composite[x, LEFT[y]]], set[e[x]]], range[x]], 
          t -> x] // Reverse // MapNotNot

or[not[member[x_, MONOIDS]], 
        subclass[hull[invar[composite[x_, LEFT[y_]]], set[e[x_]]], 
          range[x_]]] := True

Corollary.   If  x  is a monoid, the set of all powers of  y  is a subset of  range[x].

SubstTest[implies, equal[x, monoid[t]], 
          subclass[range[iterate[composite[x, LEFT[y]], set[e[x]]]], 
            range[x]], t -> x] // Reverse // MapNotNot

or[not[member[x_, MONOIDS]], 
        subclass[range[iterate[composite[x_, LEFT[y_]], set[e[x_]]]], 
          range[x_]]] := True

Theorem.  If  x  is a monoid and  y ∈ range[x], then  (y^n) ∈ range[x]  for any natural number  n = nat[z].

Map[not, 
        SubstTest[and,    
          implies[p2, p3],    
          implies[p1, p5],    
          implies[and[p4, p6], p7], 
          not[implies[p1, p7]], {p1 -> 
              and[member[x, MONOIDS], member[y, range[x]]], 
            p2 -> equal[omega, 
                domain[iterate[composite[x, LEFT[y]], set[e[x]]]]], 
            p3 -> 
              member[nat[z], 
                domain[iterate[composite[x, LEFT[y]], set[e[x]]]]], 
            p4 -> subclass[range[iterate[composite[x, LEFT[y]], set[e[x]]]], 
                range[x]], 
            p5 -> FUNCTION[iterate[composite[x, LEFT[y]], set[e[x]]]], 
            p6 -> 
              member[APPLY[iterate[composite[x, LEFT[y]], set[e[x]]], 
                  nat[z]], range[iterate[composite[x, LEFT[y]], set[e[x]]]]], 
            p7 -> member[
                APPLY[iterate[composite[x, LEFT[y]], set[e[x]]], nat[z]], 
                range[x]]}]] // Reverse

or[member[APPLY[iterate[composite[x_, LEFT[y_]], set[e[x_]]], nat[z_]], 
          range[x_]], not[member[x_, MONOIDS]], not[member[y_, range[x_]]]] := 
      True