multiples of a rational number

Johan G. F. Belinfante
2012 December 1

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

summary

Every binary homomorphism  x  from  NATADD  to  RATADD  is of the form  rattimes[APPLY[x, {0}]] ∘ INTTIMES ∘ PLUS.

derivation

Temporary definition.

funadd[x_, y_] := 
      composite[INTADD, 
        intersection[composite[inverse[FIRST], x], 
          composite[inverse[SECOND], y]]]

Lemma.  Temporary rewrite rule.

(SubstTest[hull, RATS, 
            funadd[rat[u], rat[v]], {u -> inttimes[plus[nat[t]]], 
              v -> inttimes[plus[nat[x]]]}] /. t -> set[0]) // 
      Reverse

inttimes[composite[SUCC, plus[nat[x_]]]] := 
      ratadd[id[Z], inttimes[plus[nat[x]]]]

Lemma.  Temporary rewrite rule.

Map[composite[VERTSECT[#], id[omega]] &, 
        SubstTest[reify, t, APPLY[w, nat[t]], 
          w -> composite[rattimes[rat[x]], INTTIMES, PLUS, SUCC]]] // 
      Reverse

composite[ratplus[rat[x_]], rattimes[rat[x_]], INTTIMES, PLUS] := 
      composite[rattimes[rat[x]], INTTIMES, PLUS, SUCC]

Theorem.  (An application of the uniqueness theorem for iterate.)

SubstTest[implies, 
        and[equal[composite[u, w], composite[w, SUCC]], 
          equal[image[w, set[0]], v]], 
        equal[composite[w, id[omega]], 
          iterate[u, v]], {u -> ratplus[rat[x]], 
          v -> set[e[RATADD]], 
          w -> composite[rattimes[rat[x]], INTTIMES, PLUS]}] // 
      Reverse

iterate[ratplus[rat[x_]], set[cart[Z, set[id[omega]]]]] := 
      composite[rattimes[rat[x]], INTTIMES, PLUS]

Corollary.  (Eliminate the rat wrapper.)

SubstTest[implies, equal[x, rat[t]], 
        equal[composite[rattimes[x], INTTIMES, PLUS], 
          iterate[ratplus[x], set[cart[Z, set[id[omega]]]]]], t -> x] // 
      Reverse

or[equal[composite[rattimes[x_], INTTIMES, PLUS], 
          iterate[ratplus[x_], set[cart[Z, set[id[omega]]]]]], 
        not[member[x_, RATS]]] := True

Any binary homomorphism from  NATADD  to a group is the power sequence of its value at  1 = {0}.  For the group  RATADD, this yields:

Theorem.

SubstTest[or, 
        equal[x, iterate[composite[y, LEFT[APPLY[x, set[0]]]], set[e[y]]]], 
        not[member[x, binhom[NATADD, y]]], not[member[y, GROUPS]], 
        y -> RATADD] // Reverse

or[equal[x_, 
          iterate[ratplus[APPLY[x_, set[0]]], set[cart[Z, set[id[omega]]]]]], 
        not[member[x_, binhom[NATADD, RATADD]]]] := True

Theorem.

SubstTest[implies, member[x, binhom[u, v]], 
        member[x, map[fix[domain[u]], fix[domain[v]]]], {u -> NATADD, 
          v -> RATADD}] // Reverse

or[member[x_, map[omega, RATS]], 
        not[member[x_, binhom[NATADD, RATADD]]]] := True

Corollary.

Map[
      equal[V, #] &, dif[binhom[NATADD, RATADD], map[omega, RATS]] // 
          complement // Normality]

subclass[binhom[NATADD, RATADD], map[omega, RATS]] := True

Theorem.

SubstTest[implies, and[member[x, map[w, y]], member[s, w]], 
        member[APPLY[x, s], y], {w -> omega, s -> set[0]}] // 
      Reverse

or[member[APPLY[x_, set[0]], y_], not[member[x_, map[omega, y_]]]] := 
      True

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> member[x, binhom[NATADD, RATADD]], 
            p2 -> member[x, map[omega, RATS]], 
            p3 -> member[APPLY[x, set[0]], RATS]}]] // Reverse

or[member[APPLY[x_, set[0]], RATS], 
        not[member[x_, binhom[NATADD, RATADD]]]] := True

Main Theorem.  If  x  is a binary homomorphism from  NATADD  to  RATADD, then  x = rattimes[APPLY[x, {0}]] ∘ INTTIMES ∘ PLUS.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], implies[p2, p4], 
          implies[and[p3, p4], p5], 
          not[implies[p1, p5]], {p1 -> 
              member[x, binhom[NATADD, RATADD]], 
            p2 -> member[APPLY[x, set[0]], RATS], 
            p3 -> 
              equal[x, 
                iterate[ratplus[APPLY[x, set[0]]], 
                  set[cart[Z, 
                      set[id[omega]]]]]], 
p4 -> 
              equal[iterate[ratplus[APPLY[x, set[0]]], 
                  set[cart[Z, set[id[omega]]]]], 
                composite[rattimes[APPLY[x, set[0]]], INTTIMES, PLUS]], 
            p5 -> 
              equal[x, 
                composite[rattimes[APPLY[x, set[0]]], INTTIMES, PLUS]]}]] // 
      Reverse

or[equal[x_, composite[rattimes[APPLY[x_, set[0]]], INTTIMES, PLUS]], 
        not[member[x_, binhom[NATADD, RATADD]]]] := True