the class image[VS,EQV]

Johan G. F. Belinfante
2006 October 19

SetDirectory["l:"]; << goedel86.18a; << tools.m

summary

In this notebook it is shown that a (small) function is a canonical projection of an equivalence relation if and only if it can be written in the form composite[id[x], E] for some set x.

canonical projections of equivalences

If q is an equivalence relation, the function VERTSECT[q] maps any set x to its vertical section image[q, set[x]].  This vertical section is the equivalence class of x, provided x belongs to the domain of q.

class[pair[x, y], equal[y, image[q, set[x]]]]

When q is a set, the restriction of the function VERTSECT[q] to the domain of q is also a set.  The function VS takes q to this restriction.  Comment: The combination VERTSECT[reify[q, ... ]] is equivalent to lambda[q, ... ], but works more efficiently.

VERTSECT[reify[q, composite[VERTSECT[q], id[domain[q]]]]]

Thus the canonical projection for a (small) equivalence relation eqv[setpart[x]] can be obtained by applying the function VS.

APPLY[VS, eqv[setpart[x]]]

The canonical projection for a (small) equivalence relation q is the function f = APPLY[VS, q].  The class image[VS, EQV] is therefore the class of all canonical projections of (small) equalence relations.  One can recover an equivalence relation q from its canonical projection f  by the formula q = composite[inverse[f], f].  A variable-free version of this fact is:

Map[range, 
        SubstTest[reify, x, 
          image[composite[COMPOSE, 
              intersection[composite[inverse[FIRST], INVERSE], 
                composite[inverse[SECOND], IMAGE[id[cart[V, V]]]]], VS, w], 
            set[setpart[x]]], w -> EQUIV]] // Reverse

image[COMPOSE, composite[id[image[VS, EQV]], INVERSE]] := 
      EQV

co-restrictions

The class of restrictions of any class x is:

class[z, exists[y, equal[z, composite[x, id[y]]]]]

The class of co-restrictions of x is the class of inverse of restrictions of the inverse of x.

class[z, assert[exists[y, equal[z, composite[id[y], x]]]]]

Another formula for this class will be derived in this section.  It is analogous to the following result for restrictions:

range[IMAGE[composite[id[x], inverse[FIRST]]]]

Lemma.  A temporary rewrite rule.

(image[INVERSE, RS[inverse[x]]] // Normality // 
        Reverse)

intersection[invar[composite[id[x_], inverse[SECOND], SECOND]], 
        P[composite[id[domain[VERTSECT[inverse[x_]]]], x_]]] := 
      image[INVERSE, RS[inverse[x]]]

Theorem.  A formula for the class of co-restrictions of x.

(range[IMAGE[composite[id[x], inverse[SECOND]]]] // 
        Renormality)

range[IMAGE[composite[id[x_], inverse[SECOND]]]] := 
      image[INVERSE, RS[inverse[x]]]

canonical projections of equivalences

Canonical projections are functions, but not every function is the canonical projection of an equivalence relation.  Canonical projections of thin equivalence relations are of the form composite[id[x], E], where x is the set of equivalence classes. To derive a variable-free formulation of this result, the thinpart wrapper is first replaced with a setpart wrapper.

SubstTest[composite, inverse[E], 
      id[range[composite[VERTSECT[eqv[thinpart[y]]], 
            id[fix[eqv[thinpart[y]]]]]]], y -> setpart[x]]

composite[inverse[E], 
        id[image[VERTSECT[eqv[setpart[x_]]], fix[eqv[setpart[x_]]]]]] := 
      composite[id[fix[eqv[setpart[x]]]], 
        inverse[VERTSECT[eqv[setpart[x]]]]]

Next the eqv and setpart wrappers are removed:

SubstTest[implies, equal[x, eqv[setpart[y]]], 
      member[x, 
        image[inverse[VS], image[inverse[IMAGE[SWAP]], RS[inverse[E]]]]], 
      y -> x]

(% /. x -> x_) /. Equal -> SetDelayed

The variable x can now be eliminated as follows:

Map[equal[V, #] &, 
        SubstTest[class, x, 
          implies[member[x, u], member[x, v]], {u -> EQV, 
            v -> 
              image[inverse[VS], 
                image[inverse[IMAGE[SWAP]], RS[inverse[E]]]]}]] // 
      Reverse

% /. Equal -> SetDelayed

Lemma.

ImageComp[INVERSE, IMAGE[SWAP], x] // Reverse

image[INVERSE, image[IMAGE[SWAP], x_]] := 
      image[IMAGE[id[cart[V, V]]], x]

Lemma.

ImageComp[IMAGE[id[cart[V, V]]], VS, x] // Reverse

image[IMAGE[id[cart[V, V]]], image[VS, x_]] := image[VS, x]

One can now reformulate this property of canonical projections as follows:

SubstTest[implies, subclass[u, v], 
      subclass[image[w, u], 
        image[w, v]], 
{u -> 
          image[IMAGE[SWAP], image[VS, EQV]], v -> RS[inverse[E]], 
        w -> INVERSE}]

subclass[image[VS, EQV], image[INVERSE, RS[inverse[E]]]] := 
      True

It will be shown in this notebook that the reverse inclusion also holds.  In other words, canonical projections of (small) equivalences are characterized by the property of being co-restrictions of E.

an observation

The class of all functions of the form APPLY[VS, x] is the class of functions whose range does not hold the empty set.

range[VS]

This observation can be made more explicit:  If the range of a function y does not hold the empty set, then y can be written as composite[VERTSECT[z], id[domain[z]]] for the relation z = composite[inverse[E], y].

implies[
      and[equal[y, funpart[w]], not[member[0, range[y]]], 
        equal[z, composite[inverse[E], y]]], 
equal[y, 
        composite[VERTSECT[z], id[domain[z]]]]]

The removal of the funpart wrapper yields:

SubstTest[implies, 
      and[equal[y, funpart[w]], not[member[0, range[y]]], 
        equal[z, composite[inverse[E], y]]], 
equal[y, 
        composite[VERTSECT[z], id[domain[z]]]], w -> y]

or[equal[y_, composite[VERTSECT[z_], id[domain[z_]]]], 
        member[0, range[y_]], not[equal[z_, composite[inverse[E], y_]]], 
        not[FUNCTION[y_]]] := True

For functions of the form  composite[id[x], E], the class x must be pairwise disjoint.

FUNCTION[composite[id[x], E]]

Specializing the characterization of VERTSECT functions to those of the form composite[id[x], E] yields this corollary:

SubstTest[or, equal[y, composite[VERTSECT[z], id[domain[z]]]], 
      member[0, range[y]], not[equal[z, composite[inverse[E], y]]], 
      not[FUNCTION[y]], y -> composite[id[x], E]]

(% /. {x -> x_, z -> z_}) /. 
      Equal -> SetDelayed

A variable-free formulation of the following statement will now be derived:

implies[
      and[FUNCTION[z], equal[z, composite[id[x], E]], 
        equal[y, composite[inverse[z], z]]], 
      equal[z, composite[VERTSECT[y], id[domain[y]]]]]

There are three variables to be eliminated.  One can eliminate the variable  x  by simply rewriting the statement as follows:

implies[
      and[FUNCTION[z], member[z, image[INVERSE, RS[inverse[E]]]], 
        equal[y, composite[inverse[z], z]]], 
      equal[z, composite[VERTSECT[y], id[domain[y]]]]]

Lemma.

(member[pair[x, y], composite[w, id[INVERSE], inverse[SECOND]]] // 
          AssertTest) /. w -> COMPOSE

member[pair[x_, y_], composite[COMPOSE, id[INVERSE], inverse[SECOND]]] := 
      and[equal[y, composite[inverse[x], x]], member[x, V], member[y, V], 
        subclass[x, cart[V, V]]]

The remaining variables can now be eliminated as follows.

Map[empty[composite[Id, complement[#]]] &, 
        SubstTest[class, pair[x, y], 
          implies[and[member[x, u], member[pair[x, setpart[y]], v]], 
            member[pair[setpart[y], x], w]], {u -> 
              intersection[FUNS, image[INVERSE, RS[inverse[E]]]], 
            v -> composite[COMPOSE, id[INVERSE], inverse[SECOND]], 
            w -> VS}]] // Reverse

% /. Equal -> SetDelayed

Lemma.

SubstTest[fix, 
        composite[id[u], v], {u -> FUNS, v -> composite[VS, x]}] // 
      Reverse

intersection[FUNS, fix[composite[VS, x_]]] := 
      fix[composite[VS, x]]

Lemma.

SubstTest[subclass, fix[z], range[z], 
        z -> composite[VS, COMPOSE, id[INVERSE], inverse[s], id[FUNS]]] /. 
      s -> SECOND

% /. Equal -> SetDelayed

Theorem.  Every (small) function which is a co-restriction of E is the canonical projection of some equivalence relation.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
      subclass[u, 
        w], 
{u -> 
          intersection[FUNS, image[INVERSE, RS[inverse[E]]]], 
        v -> fix[composite[VS, COMPOSE, id[INVERSE], inverse[SECOND]]], 
        w -> image[VS, EQV]}]

% /. Equal -> SetDelayed

Combining this result with the reverse inclusion yields an equation.

SubstTest[and, subclass[u, v], 
      subclass[v, 
        u], {u -> intersection[FUNS, image[INVERSE, RS[inverse[E]]]], 
        v -> image[VS, EQV]}]

intersection[FUNS, image[INVERSE, RS[inverse[E]]]] := 
      image[VS, EQV]

comment

The class of co-restrictions of the membership relation E that appears in the formula for image[VS,EQV] can also be written as a certain subclass of the power class P[E] as follows:

image[INVERSE, RS[inverse[E]]] // Normality // Reverse

intersection[invar[composite[id[E], inverse[SECOND], SECOND]], P[E]] := 
      image[INVERSE, RS[inverse[E]]]