law of exponents for integer powers of a group element

Johan G. F. Belinfante
2013 July 20

SetDirectory["l:"]; << goedel.13jul19a

summary

A general law of exponents is derived in this second of a series of notebooks about integer powers of group elements.  It is shown that if  y ∈ range[gp[x]], then the integer power function  w = intpow[gp[x], y]  satisfies the equation  w ∘ INTADD = gp[x] ∘ (w ⊗ w).  Since this is an equation involving functions, it suffices to show that the right side of the equation is a subset of the left side of the equation.  As a matter of fact, this inclusion also holds when  y  is not an element of  range[gp[x]].

domain of intpow[gp[x], y]

The following equation holds for the domain of the list of natural powers of a group element.

equal[omega, 
      domain[iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]]]]

A similar result will be derived for the integer power function.

Lemma.  An implication in one direction.

SubstTest[implies, member[t, map[u, v]], 
        equal[domain[t], u], {t -> intpow[gp[x], y], u -> Z, 
          v -> range[gp[x]]}] // Reverse

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

Lemma.

Map[not, 
        SubstTest[implies, member[v, image[u, x]], 
          member[v, range[u]], {u -> PLUS, 
            v -> inverse[plus[set[0]]]}]] // Reverse

member[composite[inverse[SUCC], id[omega]], image[PLUS, x_]] := 
      False

Lemma.  The converse implication.

Map[implies[equal[Z, domain[intpow[gp[x], y]]], equal[omega, #]] &, 
      IminComp[intpow[gp[x], y], PLUS, V]]

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

Theorem.  The domain of the integer power function is the set  Z  of all integers if and only if  y ∈ range[gp[x]].

equiv[equal[Z, domain[intpow[gp[x], y]]], 
      member[y, range[gp[x]]]]

equal[Z, domain[intpow[gp[x_], y_]]] := 
      member[y, range[gp[x]]]

degenerate integer powers

In this section an inclusion is derived for the integer power function  intpow[gp[x], y]  for the less interesting case that  y  is not a member of range[gp[x]].  Only the zero-th power of  y  is defined in this case and the integer power function consists of the single point  PAIR[id[ω], e[gp[x]]].

Theorem.

SubstTest[implies, equal[z, composite[gp[x], LEFT[y]]], 
        equal[intpow[gp[x], y], 
          union[composite[iterate[z, set[e[gp[x]]]], inverse[PLUS]], 
            composite[inv[gp[x]], iterate[z, set[e[gp[x]]]], inverse[PLUS], 
              INVERSE]]], z -> 0] // Reverse

or[equal[cart[set[id[omega]], set[e[gp[x_]]]], intpow[gp[x_], y_]], 
        member[y_, range[gp[x_]]]] := True

Theorem.  An inclusion for the law of exponents when  y  is not an element of the group  gp[x].

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> not[member[y, range[gp[x]]]], 
            p2 -> equal[cart[set[id[omega]], set[e[gp[x]]]], 
                intpow[gp[x], y]], 
            p3 -> 
              subclass[
                composite[gp[x], cross[intpow[gp[x], y], intpow[gp[x], y]]], 
                composite[intpow[gp[x], y], INTADD]]}]] // Reverse

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

additive laws of exponents

When  y ∈ range[gp[x]], the law of exponents for integer powers must be derived from the additive and subtractive laws of exponents for the list of natural powers.  In this section the additive laws are considered.

Lemma.

Map[
        subclass[composite[#, inverse[cross[PLUS, PLUS]]], 
            composite[intpow[gp[x], y], INTADD]] &, 
        Assoc[intpow[gp[x], y], PLUS, NATADD]] // Reverse

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

Lemma.  An inclusion for the case of integer powers involving positive exponents.

Map[
      subclass[composite[gp[x], cross[#, #]], 
          composite[intpow[gp[x], y], INTADD]] &, 
      Assoc[intpow[gp[x], y], PLUS, inverse[PLUS]]]

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

The case that both factors involve negative exponents is completely analogous.

Lemma.

Map[
        subclass[
            composite[#, inverse[cross[PLUS, PLUS]], 
              cross[INVERSE, INVERSE]], 
            composite[intpow[gp[x], y], INTADD]] &, 
        Map[flip, 
          Assoc[intpow[gp[x], y], composite[INVERSE, PLUS], NATADD]]] // 
      Reverse

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

Theorem.  An inclusion for the case of integer powers involving negative exponents.

Map[
      subclass[composite[gp[x], cross[#, #]], 
          composite[intpow[gp[x], y], INTADD]] &, 
      Assoc[intpow[gp[x], y], composite[INVERSE, PLUS], 
        inverse[composite[INVERSE, PLUS]]]]

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

subtractive laws of exponents

For the case that one of the factors has a positive exponent, and the other has a negative exponent, the subtractive laws of exponents for natural powers must be used.  The following lemma helps to make the transition from natural powers to integer powers.

Lemma.  A temporary rewrite rule.

Assoc[composite[gp[x], cross[intpow[gp[x], y], intpow[gp[x], y]]], 
        cross[composite[INVERSE, PLUS], PLUS], 
        inverse[cross[composite[INVERSE, PLUS], PLUS]]] // Reverse

composite[gp[x_], 
        cross[composite[inv[gp[x_]], 
            iterate[composite[gp[x_], LEFT[y_]], set[e[gp[x_]]]], 
            inverse[PLUS], INVERSE], 
          composite[iterate[composite[gp[x_], LEFT[y_]], set[e[gp[x_]]]], 
            inverse[PLUS]]]] := 
      composite[gp[x], 
        cross[composite[intpow[gp[x], y], id[image[INVERSE, range[PLUS]]]], 
          composite[intpow[gp[x], y], id[range[PLUS]]]]]

Lemma.

Map[
        subclass[
            composite[inv[gp[x]], #, 
              inverse[cross[composite[INVERSE, PLUS], PLUS]]], 
            composite[intpow[gp[x], y], INTADD]] &, 
        Assoc[intpow[gp[x], y], PLUS, rotate[NATADD]]] // Reverse

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

Lemma.  Temporary rewrite rule.

Assoc[intpow[gp[x], y], INVERSE, INTADD]

composite[intpow[gp[x_], y_], INTADD, cross[INVERSE, INVERSE]] := 
      composite[inv[gp[x]], intpow[gp[x], y], INTADD]

Corollary.

SubstTest[implies, subclass[u, v], 
        subclass[composite[t, u, w], 
          composite[t, v, w]], {t -> inv[gp[x]], 
          u -> composite[inv[gp[x]], 
              iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]], 
              rotate[NATADD], 
              cross[composite[inverse[PLUS], INVERSE], inverse[PLUS]]], 
          v -> composite[intpow[gp[x], y], INTADD], 
          w -> composite[SWAP, cross[INVERSE, INVERSE]]}] // 
      Reverse

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

Lemma.  An inclusion.

SubstTest[implies, and[equal[u, v], subclass[composite[v, w], z]], 
        subclass[composite[u, w], 
          z], {u -> composite[gp[x], 
              cross[composite[inv[gp[x]], 
                  iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]]], 
                iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]]]], 
          v -> union[
              composite[inv[gp[x]], 
                iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]], 
                rotate[NATADD]], 
              composite[iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]], 
                rotate[NATADD], SWAP]], 
          w -> cross[composite[inverse[PLUS], INVERSE], inverse[PLUS]], 
          z -> composite[intpow[gp[x], y], INTADD]}] // Reverse

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

Theorem.  An inclusion for the case that the exponents have opposite signs.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> member[y, range[gp[x]]], 
            p2 -> equal[
                composite[gp[x], 
                  cross[composite[inv[gp[x]], 
                      iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]]], 
                    iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]]]], 
                union[composite[inv[gp[x]], 
                    iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]], 
                    rotate[NATADD]], 
                  composite[
                    iterate[composite[gp[x], LEFT[y]], set[e[gp[x]]]], 
                    rotate[NATADD], SWAP]]], 
            p3 -> subclass[
                composite[gp[x], 
                  cross[composite[intpow[gp[x], y], 
                      id[image[INVERSE, range[PLUS]]]], 
                    composite[intpow[gp[x], y], id[range[PLUS]]]]], 
                composite[intpow[gp[x], y], INTADD]]}]] // Reverse

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

A similar result will now be derived for the case that the signs are switched.

Lemma.

SubstTest[implies, subclass[u, v], 
        subclass[composite[t, u, w], 
          composite[t, v, w]], {t -> inv[gp[x]], 
          u -> composite[gp[x], 
              cross[composite[intpow[gp[x], y], 
                  id[image[INVERSE, range[PLUS]]]], 
                composite[intpow[gp[x], y], id[range[PLUS]]]]], 
          v -> composite[intpow[gp[x], y], INTADD], w -> SWAP}] // 
      Reverse

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

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> member[y, range[gp[x]]], 
            p2 -> 
              subclass[
                composite[gp[x], 
                  cross[composite[intpow[gp[x], y], 
                      id[image[INVERSE, range[PLUS]]]], 
                    composite[intpow[gp[x], y], id[range[PLUS]]]]], 
                composite[intpow[gp[x], y], INTADD]], 
            p3 -> subclass[
                composite[gp[x], 
                  cross[composite[inv[gp[x]], intpow[gp[x], y], 
                      id[range[PLUS]]], 
                    composite[inv[gp[x]], intpow[gp[x], y], 
                      id[image[INVERSE, range[PLUS]]]]]], 
                composite[inv[gp[x]], intpow[gp[x], y], INTADD]]}]] // 
      Reverse

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

Theorem.  (Replace  y  with its inverse.)

SubstTest[implies, member[t, range[gp[x]]], 
        subclass[
          composite[gp[x], 
            cross[composite[inv[gp[x]], intpow[gp[x], t], id[range[PLUS]]], 
              composite[inv[gp[x]], intpow[gp[x], t], 
                id[image[INVERSE, range[PLUS]]]]]], 
          composite[inv[gp[x]], intpow[gp[x], t], INTADD]], 
        t -> APPLY[inv[gp[x]], y]] // Reverse

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

general law of exponents for integer powers

The general law of exponents for integer powers is obtained by combining the four separate cases considered above.

Lemma.  An inclusion for the case  y ∈ range[gp[x]].

Map[
          implies[member[y, range[gp[x]]], 
              subclass[#, composite[intpow[gp[x], y], INTADD]]] &, 
          SubstTest[composite, gp[x], 
            union[p, q, r, 
              s], {p -> cross[composite[intpow[gp[x], y], id[range[PLUS]]], 
                  composite[intpow[gp[x], y], id[range[PLUS]]]], 
              q -> cross[
                  composite[intpow[gp[x], y], 
                    id[image[INVERSE, range[PLUS]]]], 
                  composite[intpow[gp[x], y], id[range[PLUS]]]], 
              r -> cross[composite[intpow[gp[x], y], id[range[PLUS]]], 
                  composite[intpow[gp[x], y], 
                    id[image[INVERSE, range[PLUS]]]]], 
              s -> cross[
                  composite[intpow[gp[x], y], 
                    id[image[INVERSE, range[PLUS]]]], 
                  composite[intpow[gp[x], y], 
                    id[image[INVERSE, range[PLUS]]]]]}]] // MapNotNot // 
      Reverse

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

This result can now be combined with the inclusion for the case that  y  is not an element of the group  gp[x].

Theorem.  General inclusion for the law of exponents.

SubstTest[and, implies[p, q], 
      or[p, q], {p -> member[y, range[gp[x]]], 
        q -> subclass[
            composite[gp[x], cross[intpow[gp[x], y], intpow[gp[x], y]]], 
            composite[intpow[gp[x], y], INTADD]]}]

subclass[
        composite[gp[x_], cross[intpow[gp[x_], y_], intpow[gp[x_], y_]]], 
        composite[intpow[gp[x_], y_], INTADD]] := True

Inclusions for functions can always be replaced with equations.  In the present case, one obtains the following.

Lemma.

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
        equal[u, 
          composite[v, id[domain[u]]]], {u -> 
            composite[gp[x], cross[intpow[gp[x], y], intpow[gp[x], y]]], 
          v -> composite[intpow[gp[x], y], INTADD]}] // Reverse

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

Theorem.  General law of exponents for integer powers of a group element.

SubstTest[implies, equal[z, domain[intpow[gp[x], y]]], 
        equal[composite[gp[x], cross[intpow[gp[x], y], intpow[gp[x], y]]], 
          composite[intpow[gp[x], y], INTADD, id[cart[z, z]]]], z -> Z] // 
      Reverse

or[equal[
          composite[gp[x_], cross[intpow[gp[x_], y_], intpow[gp[x_], y_]]], 
          composite[intpow[gp[x_], y_], INTADD]], 
        not[member[y_, range[gp[x_]]]]] := True