finite subsemigroups of a group

Johan G. F. Belinfante
2012 March 5

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

summary

A nonempty finite subsemigroup of a group is a subgroup.  This fact is posed as exercise 3 on page 25 in the following reference.  The derivation presented in this notebook uses the hint given there.

"Nathan Jacobson, Lectures in Abstract Algebra. Volume 1 - Basic Concepts, D. Van Nostrand Company, Inc., Princeton, New Jersey, 1951.";

Several versions of this result are obtained, inclusing a variable-free statement.

preliminaries

Two general results about rotated functions are derived in this section.

Theorem.  If  x ⊂ y  and  rotate[y]  is a function, then so is  rotate[x].

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> P[x], v -> P[y], 
          w -> image[inverse[IMAGE[ROT]], FUNS]}] // Reverse

or[FUNCTION[rotate[x_]], not[FUNCTION[rotate[y_]]], 
        not[subclass[x_, y_]]] := True

Dual Theorem.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> P[x], v -> P[y], 
          w -> image[inverse[IMAGE[inverse[ROT]]], FUNS]}] // 
      Reverse

or[FUNCTION[rotate[composite[x_, SWAP]]], 
        not[FUNCTION[rotate[composite[y_, SWAP]]]], not[subclass[x_, y_]]] := 
      True

main theorem

Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> intersection[x, P[gp[y]]], 
          v -> P[gp[y]], w -> image[inverse[IMAGE[ROT]], FUNS]}] // 
      Reverse

subclass[image[IMAGE[ROT], intersection[x_, P[gp[y_]]]], FUNS] := 
      True

Dual Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> intersection[x, P[gp[y]]], 
          v -> P[gp[y]], 
          w -> image[inverse[IMAGE[inverse[ROT]]], FUNS]}] // 
      Reverse

subclass[image[IMAGE[inverse[ROT]], intersection[x_, P[gp[y_]]]], 
        FUNS] := True

Lemma.   (This has a reundant literal.)

SubstTest[implies, and[member[u, v], subclass[v, w]], 
          member[u, w], {u -> x, v -> P[gp[y]], 
            w -> image[inverse[IMAGE[ROT]], FUNS]}] // Reverse // 
      MapNotNot

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

Lemma.  Any subclass of a group is a set.

SubstTest[implies, and[subclass[x, t], member[t, V]], member[x, V], 
        t -> gp[y]] // Reverse

or[member[x_, V], not[subclass[x_, gp[y_]]]] := True

Theorem.  The rotation of any subset of a group is a function.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
          not[implies[p1, p3]], {p1 -> subclass[x, gp[y]], 
            p2 -> member[x, V], p3 -> FUNCTION[rotate[x]]}]] // 
      Reverse

or[FUNCTION[rotate[x_]], not[subclass[x_, gp[y_]]]] := True

Lemma.

SubstTest[implies, subclass[u, gp[v]], 
        FUNCTION[rotate[u]], {u -> flip[x], v -> flip[gp[y]]}] // 
      Reverse

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

Dual Theorem.  The reverse rotation of any subset of a group is a function.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> subclass[x, gp[y]], 
            p2 -> subclass[composite[x, id[cart[V, V]]], gp[y]], 
            p3 -> FUNCTION[rotate[composite[x, SWAP]]]}]] // 
      Reverse

or[FUNCTION[rotate[composite[x_, SWAP]]], not[subclass[x_, gp[y_]]]] := 
      True

Wrapper free versions can be derived.

Theorem.  If  x ⊂ y  and if  y  is a group, then  rotate[x]  is a function.

SubstTest[implies, equal[y, gp[t]], 
          or[FUNCTION[rotate[x]], not[subclass[x, y]]], t -> y] // 
        Reverse // MapNotNot

or[FUNCTION[rotate[x_]], not[member[y_, GROUPS]], 
        not[subclass[x_, y_]]] := True

Dual Theorem.

SubstTest[implies, equal[y, gp[t]], 
          or[FUNCTION[rotate[composite[x, SWAP]]], not[subclass[x, y]]], 
          t -> y] // Reverse // MapNotNot

or[FUNCTION[rotate[composite[x_, SWAP]]], not[member[y_, GROUPS]], 
        not[subclass[x_, y_]]] := True

The main theorem follows from the fact that any nonempty finite cancellative semigroup is a group.  This result was derived in the recently posted notebook cxlfinbo.nb.

Main Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p1, p2, p3], p4], 
          not[implies[p1, p4]], {p1 -> 
              member[x, intersection[FINITE, SEMIGPS, P[gp[y]]]], 
            p2 -> FUNCTION[rotate[x]], p3 -> FUNCTION[rotate[flip[x]]], 
            p4 -> or[empty[x], member[x, GROUPS]]}]] // 
      Reverse

or[equal[0, x_], member[x_, GROUPS], not[member[x_, FINITE]], 
        not[member[x_, SEMIGPS]], not[subclass[x_, gp[y_]]]] := 
      True

Corollary.  (Remove the  gp  wrapper.)  Any nonempty finite subsemigroup of a group is a group.

SubstTest[implies, equal[y, gp[t]], 
          or[equal[0, x], member[x, GROUPS], not[member[x, FINITE]], 
            not[member[x, SEMIGPS]], not[subclass[x, y]]], t -> y] // 
        Reverse // MapNotNot

or[equal[0, x_], member[x_, GROUPS], not[member[x_, FINITE]], 
        not[member[x_, SEMIGPS]], not[member[y_, GROUPS]], 
        not[subclass[x_, y_]]] := True

eliminating variables

In this section the variables  x  and  y  in the main theorem are eliminated.  One can eliminate both variables using reify, but it is slightly faster to eliminate one of the variables using the Normality test.

Theorem.  (Eliminate one of the two variables.)

Map[equal[V, #] &, 
      complement[
          dif[intersection[FINITE, SEMIGPS, P[gp[x]]], 
            union[GROUPS, set[0]]]] // Normality]

subclass[intersection[FINITE, SEMIGPS, P[gp[x_]]], 
        union[GROUPS, set[0]]] := True

Corollary.  (Eliminate the  gp  wrapper.)

SubstTest[implies, equal[x, gp[t]], 
          subclass[intersection[FINITE, SEMIGPS, P[x]], 
            union[GROUPS, set[0]]], t -> x] // Reverse // 
      MapNotNot

or[not[member[x_, GROUPS]], 
        subclass[intersection[FINITE, SEMIGPS, P[x_]], 
          union[GROUPS, set[0]]]] := True

Corollary.  A variable-free restatement.

Map[equal[V, domain[#]] &, 
      SubstTest[reify, x, 
        case[or[not[member[x, GROUPS]], 
            subclass[intersection[FINITE, SEMIGPS, P[x]], t]]], 
        t -> union[GROUPS, set[0]]]]

subclass[intersection[FINITE, SEMIGPS, image[inverse[S], GROUPS]], 
        union[GROUPS, set[0]]] := True