MATH.7:4.3 - Define the receiving operations and relations

For a source operation op_X:X^n→X, define:

op_Y(y1,...,yn)=h(op_X(r(y1),...,r(yn))).

In words: decode each input, perform the source operation, then encode the output. Constants have no inputs, so a source constant c becomes h(c). A source relation R becomes:

R_Y(y1,...,yn) holds exactly when R_X(r(y1),...,r(yn)) holds.

The construction can have different input and output sets. For op:X1×...×Xn→Z, use a bijection h_i:Xi→Yi for each input and k:Z→W for the output. Then:

op_target(y1,...,yn)=k(op(h_1^-1(y1),...,h_n^-1(yn))).

An unchanged scalar result uses the identity map on that scalar set. Thus transporting a length calculation changes its input coordinates while retaining the numerical length.

For a partial source operation, transport its domain too. The receiving tuple is allowed precisely when its decoded tuple is in the source domain; define its output there by the same formula. A larger independently supplied receiving domain needs its own comparison before its extra inputs are used.

Calculate one small case in both descriptions. Use it to check the direction of the maps, the constants and the operation being performed. The general preservation result comes from the defining formula and inverse equations.