composites of constant functions

Johan G. F. Belinfante
2006 June 10

SetDirectory["l:"]; << goedel82.09b; << tools.m

summary

The composite of a constant function with any function, in either order, is again a constant function.  The composite could be empty.  The empty function is considered here to be a constant function:

member[0, CONST]

composite in one order

The formula in one order is an immediate consequence of a rewrite rule for composite[COMPOSE, cross[Id,CART]]:

ImageComp[COMPOSE, cross[Id, CART], 
        cart[FUNS, cart[V, range[SINGLETON]]]] // Reverse

image[COMPOSE, cart[FUNS, CONST]] := CONST

a lemma

One is tempted to try the same strategy for the composite in the other order.  The first step is to derive an analog of the rewrite rule used above.  This is easy:

Map[
        rotate[rotate[
              rotate[composite[#, SWAP, cross[SWAP, IMAGE[SWAP]]]]]] &, 
        Assoc[IMAGE[SWAP], COMPOSE, cross[Id, CART]]] // Reverse

composite[COMPOSE, cross[CART, Id]] := 
      composite[CART, cross[IMG, Id], ROT, cross[Id, IMAGE[SWAP]]]

The direct analog of the attack used above does not succeed, but a useful lemma is obtained when one replaces FUNS with P[Id]:

ImageComp[COMPOSE, cross[CART, Id], 
        cart[cart[V, range[SINGLETON]], P[Id]]] // Reverse

image[COMPOSE, cart[CONST, P[Id]]] := CONST

composite in the other order

Lemma.  The composite of a cartesian product with anything is again a cartesian product.

Map[equal[0, #] &, 
      dif[cart[range[CART], x], image[inverse[COMPOSE], range[CART]]] // 
        VSNormality]

subclass[image[COMPOSE, cart[range[CART], x_]], range[CART]] := 
      True

Since constant functions are cartesian products, the following corollary is obtained:

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, w], 
{u -> cart[CONST, x], 
        v -> cart[range[CART], V], 
        w -> image[inverse[COMPOSE], range[CART]]}]

subclass[image[COMPOSE, cart[CONST, x_]], range[CART]] := 
      True

Since the composite of two functions is a function, this is true in particular for constant functions:

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, w], 
{u -> cart[CONST, FUNS], 
        v -> cart[FUNS, FUNS], 
        w -> image[inverse[COMPOSE], FUNS]}]

% /. Equal -> SetDelayed

Combining these results, one obtains an inclusion:

SubstTest[subclass, w, 
      intersection[x, y], {w -> image[COMPOSE, cart[CONST, FUNS]], 
        x -> FUNS, y -> range[CART]}]

% /. Equal -> SetDelayed

The lemma derived in the preceding section yields an inclusion in the opposite direction:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> cart[CONST, P[Id]], 
        v -> cart[CONST, FUNS], w -> COMPOSE}]

% /. Equal -> SetDelayed

Combining these two inclusions yields the desired equation:

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> CONST, 
        v -> image[COMPOSE, cart[CONST, FUNS]]}]

image[COMPOSE, cart[CONST, FUNS]] := CONST