range[SINGLETON as a partition

Johan G. F. Belinfante
2006 October 10

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

summary

The general theory of (thin) equivalence relations is illustrated by means of the simplest of all equivalence relations, namely, identity relations.  Singletons are the equivalence classes of the global identity relation Id. The class range[SINGLETON] of all singletons is a partition of the universal class V.  The function SINGLETON is the canonical mapping which takes each set to the equivalence class to which it belongs.

the class of singletons as a partition

Theorem.  The class of singletons is pairwise disjoint.

subclass[cart[range[SINGLETON], range[SINGLETON]], 
        union[DISJOINT, Id]] // AssertTest

subclass[cart[range[SINGLETON], range[SINGLETON]], 
        union[DISJOINT, Id]] := True

The canonical mapping for Id is SINGLETON.

composite[id[range[SINGLETON]], E]

The inverse rewrite rule is also in place.

composite[inverse[E], id[range[SINGLETON]]]

The identity relation is the union of the class of cartesian squares of its equivalence classes.

composite[inverse[E], id[range[SINGLETON]], E]

generalization

Theorem.  The canonical map corresponding to the identity relation on any class x is a restriction of SINGLETON.

composite[id[image[SINGLETON, x]], E] // VSNormality

composite[id[image[SINGLETON, x_]], E] := 
      composite[SINGLETON, id[x]]

Corollary.

composite[inverse[E], id[image[SINGLETON, x]]] // 
      DoubleInverse

composite[inverse[E], id[image[SINGLETON, x_]]] := 
      composite[id[x], inverse[SINGLETON]]

The union of the cartesian squares of the equivalence classes is the equivalence relation id[x].

composite[inverse[E], id[image[SINGLETON, x]], E]