hull[RATS, x]

Johan G. F. Belinfante
2012 August 3

SetDirectory["l:"];  << goedel.12jul29a

summary

If  x  is a subset of the rational number  y, then  y = hull[RATS, x]  unless  x  is empty or is the singleton of the origin of the integer plane  Z × Z.

intersections of sets of rationals

The class of all rational numbers is  RATS.   If  x ⊂ RATS, then  A[x]  is either a rational number, or is the origin of  Z × Z.   A concise variable-free statement of this is available in the form of a rewrite rule:

Aclosure[RATS]

In this section a restatement of this fact is derived, introducing a variable  x  for a set of rationals.

Theorem.  Any subclass of  RATS  is a set.

SubstTest[implies, and[subclass[x, y], member[y, V]], member[x, V], 
        y -> RATS] // Reverse

or[member[x_, V], not[subclass[x_, RATS]]] := True

Corollary.  A simplification rule.

equiv[and[member[x, V], subclass[x, RATS]], 
      subclass[x, RATS]]

and[member[x_, V], subclass[x_, RATS]] := subclass[x, RATS]

The following lemma introduces a variable into the statement that the class  Aclosure[RATS]  is the union of RATS and the singleton of the origin of  Z × Z.  Since the class  RATS  is a set, one has  Aclosure[RATS] = fix[HULL[RATS]].  In general  fix[HULL[x]]  holds  A[y]  for any non-empty subclass  y ⊂ x, whereas  Aclosure[x]  holds  A[y]  for  y ⊂ x  only when  y  is a set.

Theorem.  If  x  is a non-empty set of rationals, then either  A[x]  is a rational number or is the origin of  Z × Z.

Map[implies[and[member[x, P[RATS]], not[empty[x]]], #] &, 
        SubstTest[member, A[x], fix[HULL[y]], y -> RATS]] // 
      Reverse

or[equal[0, x_], equal[A[x_], cart[set[id[omega]], set[id[omega]]]], 
        member[A[x_], RATS], not[subclass[x_, RATS]]] := True

Comment.  The main application of this result will be to computing rational hulls, that is, sets of the form  hull[RATS, x].

trivial hulls

In this section a rewrite rule is derived to dispose of the case that the rational hull of a set is the origin of the integer plane.

Lemma.  A general result.

SubstTest[implies, equal[u, v], 
        equal[A[u], A[v]], {u -> x, 
          v -> intersection[x, image[S, set[y]]]}] // Reverse

(% /. {x -> x_, y -> y_}) /. 
      Equal -> SetDelayed

Theorem.  A better rewrite rule.

equiv[equal[A[x], hull[x, y]], subclass[y, A[x]]]

equal[A[x_], hull[x_, y_]] := subclass[y, A[x]]

Corollary.  (Application to the case of rational hulls.)

SubstTest[equal, hull[t, x], A[t], t -> RATS] // 
      Reverse

equal[cart[set[id[omega]], set[id[omega]]], hull[RATS, x_]] := 
      subclass[x, cart[set[id[omega]], set[id[omega]]]]

computing rational hulls

The rational hull  hull[RATS, x]  of a class  x  is the intersection of all rational numbers that contain  x.  The rational hull  of  x  is the universal class V  if  x  is not a subset of any rational number.

equal[V, hull[RATS, x]]

Theorem.

SubstTest[implies, and[equal[u, v], member[v, V]], 
        member[u, V], {u -> hull[RATS, x], 
          v -> cart[set[id[omega]], set[id[omega]]]}] // Reverse

or[member[x_, image[inverse[S], RATS]], 
        not[subclass[x_, cart[set[id[omega]], set[id[omega]]]]]] := 
      True

Corollary.  Simplification rule.

and[equal[cart[set[id[omega]], set[id[omega]]], hull[RATS, x]], 
      member[x, image[inverse[S], RATS]]]

equiv[
      and[member[x, image[inverse[S], RATS]], 
        subclass[x, cart[set[id[omega]], set[id[omega]]]]], 
      subclass[x, cart[set[id[omega]], set[id[omega]]]]]

and[member[x_, image[inverse[S], RATS]], 
        subclass[x_, cart[set[id[omega]], set[id[omega]]]]] := 
      subclass[x, cart[set[id[omega]], set[id[omega]]]]

Theorem.  A class x  is a subset of some rational number if and only if its rational hull is a rational number or  x ⊂ {id[ω]} ×{id[ω]}.

SubstTest[member, APPLY[funpart[t], x], range[funpart[t]], 
        t -> HULL[RATS]] // Reverse

or[member[hull[RATS, x_], RATS], 
        subclass[x_, cart[set[id[omega]], set[id[omega]]]]] := 
      member[x, image[inverse[S], RATS]]

If  x  is a subset of the rational number  y, then either hull[RATS, x] is a rational number or  x ⊂ {id[ω]} ×{id[ω]}.

or[subclass[x, cart[set[id[omega]], set[id[omega]]]], 
      member[hull[RATS, x], RATS], not[member[y, RATS]], 
      not[subclass[x, y]]]

A more precise statement is useful.  It is shown below that if  x  is a subset of a rational number  y, then its rational hull is either the origin or the rational number  y.

Theorem.  If  x  is a subset of the rational number  y, then  y = hull[RATS, x]  unless  x  is empty or is the singleton of the origin.

Map[not, 
        SubstTest[and, 
          implies[and[p1, p2], 
            or[p4, p5]],    
          implies[and[p1, p7], p5],  
          not[implies[and[p1, p2], or[p5, p6]]], {p1 -> subclass[x, y], 
            p2 -> member[y, RATS], p4 -> member[hull[RATS, x], RATS], 
            p5 -> subclass[x, cart[set[id[omega]], set[id[omega]]]], 
            p6 -> equal[hull[RATS, x], y], 
            p7 -> 
              equal[intersection[y, hull[RATS, x]], 
                cart[set[id[omega]], set[id[omega]]]]}]] // 
      Reverse

or[equal[hull[RATS, x_], y_], not[member[y_, RATS]], 
        not[subclass[x_, y_]], 
        subclass[x_, cart[set[id[omega]], set[id[omega]]]]] := 
      True

rational hulls of singletons

Theorem.  If  pair[x,y] ∈ domain[RATIO], then hull[RATS, {x} × {y}] = APPLY[RATIO, pair[x,y]].

SubstTest[or, equal[v, hull[RATS, u]], not[member[v, RATS]], 
        not[subclass[u, v]], 
        subclass[u, 
          cart[set[id[omega]], set[id[omega]]]], {u -> set[PAIR[x, y]], 
          v -> composite[inverse[inttimes[x]], inttimes[y]]}] // 
      Reverse

or[equal[composite[inverse[inttimes[x_]], inttimes[y_]], 
          hull[RATS, cart[set[x_], set[y_]]]], equal[id[omega], x_], 
        not[member[x_, Z]], not[member[y_, Z]]] := True

Lemma.  (Eliminating the variables.)

Map[empty[composite[Id, complement[#]]] &, 
      SubstTest[class, pair[x, y], 
        implies[member[pair[x, y], t], 
          equal[APPLY[funpart[u], PAIR[x, y]], 
            APPLY[funpart[v], PAIR[x, y]]]], {t -> domain[RATIO], 
          u -> composite[HULL[RATS], SINGLETON], 
          v -> RATIO}]]

% /. Equal -> SetDelayed

Lemma.  An inclusion.

SubstTest[subclass, domain[funpart[v]], 
      fix[composite[inverse[funpart[u]], funpart[v]]], {u -> 
          composite[HULL[RATS], SINGLETON], v -> RATIO}]

% /. Equal -> SetDelayed

Lemma.  The singleton of the origin is a subset of a rational number.  (In fact, it is a subset of every rational number.)

member[cart[set[id[omega]], set[id[omega]]], image[inverse[S], RATS]] // 
      AssertTest

member[cart[set[id[omega]], set[id[omega]]], image[inverse[S], RATS]] := 
      True

Theorem.  A rewrite rule for  HULL[RATS] ∘ SINGLETON.

SubstTest[equal, u, 
        composite[funpart[v], 
          id[domain[u]]], {u -> 
            union[RATIO, composite[SINGLETON, id[A[RATS]]]], 
          v -> composite[HULL[RATS], SINGLETON]}] // Reverse

composite[HULL[RATS], SINGLETON] := 
      union[RATIO, 
        cart[cart[set[id[omega]], set[id[omega]]], 
          set[cart[set[id[omega]], set[id[omega]]]]]]

The final theorem restates this result, introducing a single variable for a point in the integer plane not on the vertical axis through the origin.

Theorem.  If  x ∈ domain[RATIO], then  APPLY[RATIO, x] = hull[RATS, {x}].

SubstTest[implies, equal[x, PAIR[u, v]], 
          or[equal[APPLY[RATIO, x], hull[RATS, set[x]]], 
            equal[first[x], id[omega]], not[member[first[x], Z]], 
            not[member[second[x], Z]]], {u -> first[x], 
            v -> second[x]}] // MapNotNot // Reverse

or[equal[APPLY[RATIO, x_], hull[RATS, set[x_]]], 
        equal[first[x_], id[omega]], not[member[first[x_], Z]], 
        not[member[second[x_], Z]]] := True