Aclosure for unital submonoids

Johan G. F. Belinfante
2013 September 11

SetDirectory["l:"]; << goedel.13sep10a

summary

The set of unital submonoids of a monoid  x  is closed under arbitrary (non-empty) intersections.  The key to deriving this result is a characterization of unital submonoids as submonoids that hold the point  pair[pair[e[x], e[x]], e[x]].

a characterization of unital submonoids

Theorem.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p2, p3], 
          not[implies[p1, p3]], {p1 -> member[w, MONOIDS], 
            p2 -> member[w, SEMIGPS], 
            p3 -> or[equal[e[w], e[x]], not[member[x, MONOIDS]], 
                not[member[pair[pair[e[x], e[x]], e[x]], w]], 
                not[subclass[w, x]]]}]] // Reverse

or[equal[e[w_], e[x_]], not[member[w_, MONOIDS]], 
        not[member[x_, MONOIDS]], 
        not[member[pair[pair[e[x_], e[x_]], e[x_]], w_]], 
        not[subclass[w_, x_]]] := True

Observation.

implies[and[member[w, MONOIDS], subclass[w, x], member[x, MONOIDS]], 
          equiv[equal[e[w], e[x]], member[pair[pair[e[x], e[x]], e[x]], w]]] // 
        not // not

the main theorem

For convenience, the wrapper  monoid[x] will be used.  In general  monoid[x]  could be either empty or a monoid.  In the present situation however the hypothesis  pair[pair[monoid[x], monoid[x]], monoid[x]] ∈ w  rules out the possibility that  monoid[x]  be empty.

Lemma.

SubstTest[Aclosure, intersection[SEMIGPS, P[semigp[t]]], 
        t -> monoid[x]] // Reverse

Aclosure[intersection[SEMIGPS, P[monoid[x_]]]] := 
      intersection[SEMIGPS, P[monoid[x]]]

Theorem.

SubstTest[implies, subclass[u, v], 
        subclass[Aclosure[u], 
          Aclosure[v]], {u -> 
            intersection[MONOIDS, 
              complement[
                P[complement[
                    set[pair[pair[e[monoid[x]], e[monoid[x]]], 
                        e[monoid[x]]]]]]], P[monoid[x]]], 
          v -> intersection[SEMIGPS, P[monoid[x]]]}] // Reverse

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

Lemma.

SubstTest[implies, and[subclass[u, v], subclass[v, w]], 
        subclass[u, 
          w], {u -> Aclosure[
              intersection[MONOIDS, 
                complement[
                  P[complement[
                      set[pair[pair[e[monoid[x]], e[monoid[x]]], 
                          e[monoid[x]]]]]]], P[monoid[x]]]], 
          v -> intersection[SEMIGPS, 
              complement[
                P[complement[
                    set[pair[pair[e[monoid[x]], e[monoid[x]]], 
                        e[monoid[x]]]]]]], P[monoid[x]]], 
          w -> MONOIDS}] // Reverse

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

Main Theorem.  The class of unital submonoids of a monoid is closed under arbitrary intersections.

SubstTest[implies, subclass[Aclosure[t], t], equal[Aclosure[t], t], 
        t -> intersection[MONOIDS, 
            complement[
              P[complement[
                  set[pair[pair[e[monoid[x]], e[monoid[x]]], 
                      e[monoid[x]]]]]]], P[monoid[x]]]] // Reverse

Aclosure[
        intersection[MONOIDS, 
          complement[
            P[complement[
                set[pair[pair[e[monoid[x_]], e[monoid[x_]]], 
                    e[monoid[x_]]]]]]], P[monoid[x_]]]] := 
      intersection[MONOIDS, 
        complement[
          P[complement[
              set[pair[pair[e[monoid[x]], e[monoid[x]]], e[monoid[x]]]]]]], 
        P[monoid[x]]]

Corollary.  (Eliminating the monoid wrapper.)

SubstTest[implies, equal[x, monoid[t]], 
          equal[Aclosure[
              intersection[MONOIDS, 
                complement[P[complement[set[pair[pair[e[x], e[x]], e[x]]]]]], 
                P[x]]], 
            intersection[MONOIDS, 
              complement[P[complement[set[pair[pair[e[x], e[x]], e[x]]]]]], 
              P[x]]], t -> x] // Reverse // MapNotNot

or[equal[
          Aclosure[
            intersection[MONOIDS, 
              complement[
                P[complement[set[pair[pair[e[x_], e[x_]], e[x_]]]]]], 
              P[x_]]], 
          intersection[MONOIDS, 
            complement[P[complement[set[pair[pair[e[x_], e[x_]], e[x_]]]]]], 
            P[x_]]], not[member[x_, MONOIDS]]] := True

Observation.  One can replace  Aclosure[–] with  fix[HULL[–]]  because the class of unital submonoids of  a monoid is a set.

fix[
      HULL[intersection[MONOIDS, 
          complement[
            P[complement[
                set[pair[pair[e[monoid[x]], e[monoid[x]]], e[monoid[x]]]]]]], 
          P[monoid[x]]]]]

Theorem.  The intersection of any non-empty collection of unital submonoids of  monoid[x]  is a monoid.

SubstTest[implies, 
          and[equal[fix[HULL[t]], t], subclass[w, t], not[empty[w]]], 
          member[A[w], t], 
          t -> intersection[MONOIDS, 
              complement[
                P[complement[
                    set[pair[pair[e[monoid[x]], e[monoid[x]]], 
                        e[monoid[x]]]]]]], P[monoid[x]]]] // Reverse // 
      MapNotNot

or[equal[0, w_], member[A[w_], MONOIDS], 
        not[member[pair[pair[e[monoid[x_]], e[monoid[x_]]], e[monoid[x_]]], 
            A[w_]]], not[subclass[w_, MONOIDS]], 
        not[subclass[U[w_], monoid[x_]]]] := True

Corollary.  (Eliminating the monoid wrapper.)

SubstTest[implies, equal[x, monoid[t]], 
          or[equal[0, w], member[A[w], MONOIDS], 
            not[member[pair[pair[e[x], e[x]], e[x]], A[w]]], 
            not[subclass[w, MONOIDS]], not[subclass[U[w], x]]], t -> x] // 
        Reverse // MapNotNot

or[equal[0, w_], member[A[w_], MONOIDS], 
        not[member[pair[pair[e[x_], e[x_]], e[x_]], A[w_]]], 
        not[member[x_, MONOIDS]], not[subclass[w_, MONOIDS]], 
        not[subclass[U[w_], x_]]] := True

Theorem.  The submonoid  A[w]  is unital.

Map[not, 
        SubstTest[and, implies[p1, p2], implies[p1, p3], 
          implies[and[p1, p2, p3], p4], 
          not[implies[p1, p4]], {p1 -> 
              and[subclass[w, MONOIDS], not[empty[w]], subclass[U[w], x], 
                member[x, MONOIDS], 
                member[pair[pair[e[x], e[x]], e[x]], A[w]]], 
            p2 -> member[A[w], MONOIDS], p3 -> subclass[A[w], x], 
            p4 -> equal[e[A[w]], e[x]]}]] // Reverse

or[equal[0, w_], equal[e[A[w_]], e[x_]], 
        not[member[pair[pair[e[x_], e[x_]], e[x_]], A[w_]]], 
        not[member[x_, MONOIDS]], not[subclass[w_, MONOIDS]], 
        not[subclass[U[w_], x_]]] := True