classes of squares

Johan G. F. Belinfante
2011 May 25

SetDirectory["l:"]; << goedel.11may24a

summary

Rewrite rules are derived for classes of the form  image[CART,  id[x]].  These are classes whose members are cartesian squares.

equiv[member[s, image[CART, id[x]]], 
      and[equal[s, cart[fix[s], fix[s]]], member[fix[s], x]]]

Several rewrite rules involving  fix[image[inverse[CART], x]] remain valid when this expression is replaced with the closely related expression image[IMAGE[inverse[DUP]], x].   As an application, a rewrite rule is derived for the class of domains of sub-binary operations of a given one.

derivation

Theorem.  An inclusion.

SubstTest[implies, subclass[u, v], 
        subclass[image[u, x], 
          image[v, x]], {u -> inverse[composite[CART, DUP]], 
          v -> FIX}] // Reverse

subclass[fix[image[inverse[CART], x_]], 
        image[IMAGE[inverse[DUP]], x_]] := True

Theorem.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], image[t, v]], {t -> IMAGE[inverse[DUP]], 
          u -> x, v -> image[CART, id[y]]}] // Reverse

or[not[subclass[x_, image[CART, id[y_]]]], 
        subclass[image[IMAGE[inverse[DUP]], x_], y_]] := True

Lemma.  A temporary rewrite rule.

SubstTest[subclass, x, intersection[t, y], t -> image[CART, Id]] // 
      Reverse

subclass[x_, image[CART, id[fix[image[inverse[CART], y_]]]]] := 
      and[subclass[x, y], subclass[x, image[CART, Id]]]

Theorem.  A simplification rule.

SubstTest[equal, x, intersection[x, y], y -> image[CART, Id]] // 
      Reverse

equal[x_, image[CART, id[fix[image[inverse[CART], x_]]]]] := 
      subclass[x, image[CART, Id]]

Theorem.  An alternate formula for the class of sides of a class of squares.

SubstTest[implies, equal[x, y], 
        equal[image[t, x], image[t, y]], {t -> FIX, 
          y -> image[CART, id[fix[image[inverse[CART], x]]]]}] // 
      Reverse

or[equal[fix[image[inverse[CART], x_]], 
          image[IMAGE[inverse[DUP]], x_]], 
        not[subclass[x_, image[CART, Id]]]] := True

Lemma.  A temporary rewrite rule.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[and[p1, p2], p3], 
          not[implies[p1, p3]], {p1 -> subclass[x, image[CART, Id]], 
            p2 -> 
              equal[image[IMAGE[inverse[DUP]], x], 
                fix[image[inverse[CART], x]]], 
            p3 -> equal[x, 
                image[CART, id[image[IMAGE[inverse[DUP]], x]]]]}]] // 
      Reverse

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.  A simplification rule.

equiv[equal[x, image[CART, id[image[IMAGE[inverse[DUP]], x]]]], 
      subclass[x, image[CART, Id]]]

equal[x_, image[CART, id[image[IMAGE[inverse[DUP]], x_]]]] := 
      subclass[x, image[CART, Id]]

an application

An application to the theory of binary operations is made in this section.

Theorem.  The domain of any binary operation is a cartesian square.

SubstTest[implies, subclass[u, v], 
        subclass[image[t, u], image[t, v]], {t -> IMAGE[FIRST], 
          u -> intersection[BINOPS, x], v -> BINOPS}] // 
      Reverse

subclass[image[IMAGE[FIRST], intersection[BINOPS, x_]], 
        image[CART, Id]] := True

A more precise result is derived below for the special case that  x  is replaced with  P[binop[x]].

Lemma.  A temporary rewrite rule.

Map[equal[V, #] &, 
      union[complement[binclosed[binop[x]]], 
          image[inverse[IMAGE[id[fix[domain[binop[x]]]]]], 
            binclosed[binop[x]]]] // Normality]

(% /. x -> x_) /. Equal -> SetDelayed

Theorem.  A better rewrite rule.

equal[image[IMAGE[id[fix[domain[binop[x]]]]], binclosed[binop[x]]], 
      intersection[P[fix[domain[binop[x]]]], binclosed[binop[x]]]]

image[IMAGE[id[fix[domain[binop[x_]]]]], binclosed[binop[x_]]] := 
      intersection[binclosed[binop[x]], P[fix[domain[binop[x]]]]]

Theorem.  (A temporary rule subsumed by another rewrite rule derived below.)

Map[image[FIX, #] &, 
        ImageComp[IMAGE[FIRST], 
          IMAGE[composite[id[binop[x]], inverse[FIRST]]], 
          image[CART, id[binclosed[binop[x]]]]]] // Reverse

image[IMAGE[inverse[DUP]], 
        image[IMAGE[FIRST], intersection[BINOPS, P[binop[x_]]]]] := 
      intersection[binclosed[binop[x]], P[fix[domain[binop[x]]]]]

Lemma.  A simplification rule.

equal[
      image[CART, 
        id[image[IMAGE[inverse[DUP]], 
            image[IMAGE[FIRST], intersection[BINOPS, x]]]]], 
      image[IMAGE[FIRST], intersection[BINOPS, x]]]

image[CART, 
        id[image[IMAGE[inverse[DUP]], 
            image[IMAGE[FIRST], intersection[BINOPS, x_]]]]] := 
      image[IMAGE[FIRST], intersection[BINOPS, x]]

It is not clear how best to orient the following rewrite rule.  The present choice should be regarded as tentative.

Theorem.  The class of domains of sub-binary operations of a given binary operation is the class of cartesian squares of subsets of the fixed-point set of the domain of the given binary operation and sets that are binary closed under that binary operation.

SubstTest[image, CART, 
      id[image[IMAGE[inverse[DUP]], 
          image[IMAGE[FIRST], intersection[BINOPS, t]]]], 
      t -> P[binop[x]]]

image[IMAGE[FIRST], intersection[BINOPS, P[binop[x_]]]] := 
      image[CART, 
        id[intersection[binclosed[binop[x]], 
            P[fix[domain[binop[x]]]]]]]

The choice of orientation of the rewrite rule made above has the advantage that it avoids having to add a separate rule for the following fact.

equal[Aclosure[image[IMAGE[FIRST], intersection[BINOPS, P[binop[x]]]]], 
      image[IMAGE[FIRST], intersection[BINOPS, P[binop[x]]]]]

In addition, the above choice has the advantage that it makes it unnecessary to retain the rewrite rule derived above for the more complicated quantity image[IMAGE[inverse[DUP]],  image[IMAGE[FIRST], intersection[BINOPS, P[binop[x]]]]].   So the net effect is that one can get by with fewer rewrite rules if the chosen orientation is adopted.