ranges of subgroups are closed under chain unions

Johan G. F. Belinfante
2011 November 19

SetDirectory["l:"];  << goedel.11nov17a

summary

The union of a nonempty chain of ranges of subgroups of a group is the range of a subgroup.

derivation

Theorem.

SubstTest[union, 
      intersection[binclosed[u], complement[set[0]], fix[IMAGE[v]]], 
      set[0], {u -> gp[x], v -> inv[gp[x]]}]

intersection[binclosed[gp[x_]], fix[IMAGE[inv[gp[x_]]]]] := 
      union[image[IMAGE[SECOND], intersection[GROUPS, P[gp[x]]]], 
        set[0]]

Theorem.

SubstTest[Uchains, 
        intersection[binclosed[u], fix[IMAGE[v]]], {u -> gp[x], 
          v -> inv[gp[x]]}] // Reverse

Uchains[image[IMAGE[SECOND], intersection[GROUPS, P[gp[x_]]]]] := 
      union[image[IMAGE[SECOND], intersection[GROUPS, P[gp[x]]]], 
        set[0]]

Corollary.

SubstTest[Uchains, 
        image[IMAGE[SECOND], intersection[GROUPS, P[gp[x]]]], 
        x -> INTADD] // Reverse

Uchains[image[VERTSECT[INTDIV], Z]] := 
      range[VERTSECT[INTDIV]]

Corollary.

SubstTest[Uchains, union[x, set[0]], x -> image[VERTSECT[INTDIV], Z]] // 
      Reverse

Uchains[range[VERTSECT[INTDIV]]] := range[VERTSECT[INTDIV]]

similar results for DIV

Theorem.

SubstTest[Uchains, 
        intersection[binclosed[u], binclosed[v], P[w]], {u -> NATADD, 
          v -> rotate[NATADD], w -> omega}] // Reverse

Uchains[range[VERTSECT[DIV]]] := range[VERTSECT[DIV]]

Corollary.

SubstTest[Uchains, dif[x, set[0]], x -> range[VERTSECT[DIV]]] // 
      Reverse

Uchains[image[VERTSECT[DIV], omega]] := range[VERTSECT[DIV]]