category of sets (functions)

Johan G. F. Belinfante
2005 August 1

SetDirectory["i:"]; << goedel71.31a; << tools.m

summary

The morphisms in the category of sets are ordered pairs  PAIR[x,y], where x is a (small) function and y is a set (called the codomain of the morphism) which contains the range of x.  The function  CATOFUNS  is the (partial) binary composition for morphisms of the category of sets.  Some rules about this function are derived.

FUNCTION and domain rules

Since CATOFUNS is a restriction of CATORELN, it follows that it is a function.

SubstTest[FUNCTION, 
      composite[funpart[x], id[y]], {x -> CATORELN, 
        y -> cart[cart[FUNS, V], cart[FUNS, V]]}]

FUNCTION[CATOFUNS] := True

A similar argument yields a formula for the domain:

IminComp[CATORELN, id[cart[cart[FUNS, V], cart[FUNS, V]]], 
      V]

domain[CATOFUNS] := 
      composite[id[composite[S, IMAGE[SECOND], id[FUNS]]], inverse[SECOND], 
        IMAGE[FIRST], FIRST, 
        id[composite[S, IMAGE[SECOND], id[FUNS]]]]

an abbreviation

The following abbreviation is convenient.

direct[x_, y_] := composite[cross[x, y], TWIST]

The connection with CATOFUNS is:

equal[CATOFUNS, 
      composite[direct[COMPOSE, FIRST], id[domain[CATOFUNS]]]]

range

Map[
      inverse, composite[FIRST, 
            id[composite[IMAGE[DUP], IMAGE[FIRST], id[FUNS]]], 
            inverse[COMPOSE]] // inverse // VSNormality]

composite[FIRST, id[composite[IMAGE[DUP], IMAGE[FIRST], id[FUNS]]], 
        inverse[COMPOSE]] := id[FUNS]

Map[subclass[range[#], range[CATOFUNS]] &, 
      Assoc[direct[COMPOSE, FIRST], id[domain[CATOFUNS]], 
        cross[Id, 
          composite[id[inverse[IMAGE[DUP]]], inverse[SECOND]]]]]

% /. Equal -> SetDelayed

Map[
        implies[subclass[#, range[CATORELN]], 
            subclass[range[CATOFUNS], composite[S, IMAGE[SECOND]]]] &, 
        ImageComp[CATORELN, id[cart[cart[FUNS, V], cart[FUNS, V]]], V]] // 
      Reverse

% /. Equal -> SetDelayed

Map[subclass[#, cart[FUNS, V]] &, 
      ImageComp[direct[COMPOSE, FIRST], id[domain[CATOFUNS]], V]]

% /. Equal -> SetDelayed

SubstTest[and, subclass[u, v], 
      subclass[v, u], {u -> range[CATOFUNS], 
        v -> domain[domain[CATOFUNS]]}]

range[CATOFUNS] := composite[S, IMAGE[SECOND], id[FUNS]]

endomorphisms

equal[intersection[FUNS, U[image[MAP, Id]]], 
      U[image[MAP, Id]]]

intersection[FUNS, U[image[MAP, Id]]] := U[image[MAP, Id]]

SubstTest[implies, and[subclass[u, v], FUNCTION[v]], 
      equal[u, composite[v, id[domain[u]]]], {u -> 
          fix[domain[CATOFUNS]], 
        v -> composite[IMAGE[FIRST], id[FUNS]]}]

composite[intersection[composite[S, IMAGE[SECOND]], IMAGE[FIRST]], 
        id[FUNS]] := 
      composite[IMAGE[FIRST], id[U[image[MAP, Id]]]]

a consequence of associativity

The associative property of the (partial) binary composition for morphisms of the category of relations implies:

SubstTest[implies, associative[x], 
      equal[composite[x, cross[Id, x], ASSOC], composite[x, cross[x, Id]]], 
      x -> CATORELN]

composite[CATORELN, cross[Id, CATORELN], ASSOC] := 
      composite[CATORELN, cross[CATORELN, Id]]

A similar rule holds in the category of sets.

SubstTest[implies, associative[x], 
      equal[composite[x, cross[Id, x], ASSOC], composite[x, cross[x, Id]]], 
      x -> CATOFUNS]

composite[CATOFUNS, cross[Id, CATOFUNS], ASSOC] := 
      composite[CATOFUNS, cross[CATOFUNS, Id]]

membership rules

Lemma.

equiv[
      and[equal[z, composite[x, y]], member[x, V], member[y, V], 
        member[z, V]], 
      and[equal[z, composite[x, y]], member[x, V], member[y, V]]]

and[equal[z_, composite[x_, y_]], member[x_, V], member[y_, V], 
        member[z_, V]] := 
      and[equal[z, composite[x, y]], member[x, V], member[y, V]]

Lemma.

member[pair[pair[pair[u, v], pair[x, y]], pair[w, z]], 
        composite[t, TWIST]] // AssertTest

member[pair[pair[pair[u_, v_], pair[x_, y_]], pair[w_, z_]], 
        composite[t_, TWIST]] := 
      and[member[u, V], member[v, V], member[x, V], member[y, V], 
        member[pair[pair[pair[u, x], pair[v, y]], pair[w, z]], t]]

Membership rule for CATORELN.

SubstTest[member, pair[pair[pair[u, v], pair[x, y]], pair[w, z]], 
      composite[direct[COMPOSE, FIRST], id[t]], 
      t -> domain[CATORELN]]

member[pair[pair[pair[u_, v_], pair[x_, y_]], pair[w_, z_]], CATORELN] := 
      and[equal[v, z], equal[w, composite[u, x]], equal[y, domain[u]], 
        member[u, V], member[v, V], member[x, V], member[y, V], 
        subclass[u, cart[V, V]], subclass[x, cart[V, V]], 
        subclass[range[u], v], subclass[range[x], y]]

Membership rule for CATOFUNS.

SubstTest[member, pair[pair[pair[u, v], pair[x, y]], pair[w, z]], 
      composite[direct[COMPOSE, FIRST], id[t]], 
      t -> domain[CATOFUNS]]

member[pair[pair[pair[u_, v_], pair[x_, y_]], pair[w_, z_]], CATOFUNS] := 
      and[equal[v, z], equal[w, composite[u, x]], equal[y, domain[u]], 
        FUNCTION[u], FUNCTION[x], member[u, V], member[v, V], member[x, V], 
        member[y, V], subclass[range[u], v], 
        subclass[range[x], y]]

normalization

The membership rules in the preceding section are too special to have any effect on the usual Normality tests.  The following substitutes are provided.

class[pair[pair[pair[u, v], pair[x, y]], pair[w, z]], 
      and[equal[v, z], equal[w, composite[u, x]], equal[y, domain[u]], 
        FUNCTION[u], FUNCTION[x], member[u, V], member[v, V], member[x, V], 
        member[y, V], subclass[range[u], v], 
        subclass[range[x], y]]]

class[pair[pair[pair[u, v], pair[x, y]], pair[w, z]], 
      and[equal[v, z], equal[w, composite[u, x]], equal[y, domain[u]], 
        member[u, V], member[v, V], member[x, V], member[y, V], 
        subclass[u, cart[V, V]], subclass[x, cart[V, V]], 
        subclass[range[u], v], subclass[range[x], y]]]