characterizing RATADD endomorphisms

Johan G. F. Belinfante
2013 March 10

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

summary

Any endomorphism  f  of rational addition is the operation of multiplying by the rational number APPLY[f , id[Z]].

implies[member[f, binhom[RATADD, RATADD]], 
      equal[f, rattimes[APPLY[f, id[Z]]]]]

In this notebook a succinct variable-free reformulation of this fact is derived.

derivation

Lemma.  (Inclusion in easy direction.)

SubstTest[subclass, fix[composite[u, v]], 
        range[u], {u -> RATTIMES, v -> eval[id[Z]]}] // 
      Reverse

% /. Equal -> SetDelayed

Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, w], {u -> binhom[RATADD, RATADD], v -> map[RATS, RATS], 
          w -> domain[eval[id[Z]]]}] // Reverse

% /. Equal -> SetDelayed

Lemma.

Assoc[eval[id[Z]], RATTIMES, inverse[RATTIMES]]

composite[eval[id[Z]], id[binhom[RATADD, RATADD]]] := 
      inverse[RATTIMES]

Corollary.

composite[id[binhom[RATADD, RATADD]], inverse[eval[id[Z]]]] // 
      DoubleInverse

composite[id[binhom[RATADD, RATADD]], inverse[eval[id[Z]]]] := 
      RATTIMES

Lemma.

SubstTest[implies, subclass[u, v], 
        subclass[composite[t, u], 
          composite[t, v]], {t -> id[binhom[RATADD, RATADD]], 
          u -> id[binhom[RATADD, RATADD]], 
          v -> composite[inverse[eval[id[Z]]], eval[id[Z]]]}] // 
      Reverse

% /. Equal -> SetDelayed

Theorem.

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> fix[composite[RATTIMES, eval[id[Z]]]], 
        v -> binhom[RATADD, RATADD]}]

fix[composite[RATTIMES, eval[id[Z]]]] := 
      binhom[RATADD, RATADD]