[Skip Navigation] [CSUSB] / [CNS] / [CSE] / [R J Botting] / [ MATHS ] / math_33_Monoids
[Contents] [Source Text] || [Notation] || [Copyright] || [Contact] [Search ]
Sat May 19 08:01:58 PDT 2012




      Monoid have much of the structure normally taught as part of group theory. They are the algebra that underlies both numbers and strings. They turn up in many different domains - both in practice and theory.

      Basis of Monoids

    1. SEMIGROUP::= See http://cse.csusb.edu/dick/maths/math_32_Semigroups.html.


      The following is used in [ math_31_One_Associative_Op.html ] and [ math_34_Groups.html ]

      Definition of a Monoid

    2. MONOID::=SEMIGROUP and following,
      1. u::units(Set,op).
      2. (-1)|- (nt): nontrivial.
      3. (-2)|- (unit_sq): u op u = u.
      4. (-3)|- (unique_unit): for one v:Set( v in units(Set,op)).

        Proof of nt

      5. (u)|-u isa Set,
      6. (above)|-some Set,
      7. (SEMIGROUP.nontrivial)|-nontrivial.

        Proof of unique_unit

      8. (above)|- (given): u in units(Set,op).
      9. (given)|- (exists): for some v:Set( v in units(Set,op)).
        1. v:Set,
        2. (0): v in units(Set,op).
        3. (u is unit)|- (1): u op v = u.
        4. (v is unit)|- (2): u op v = v.
        5. (1, 2)|- (3): u=v.

        (Close Let )

      10. (above)|- (at_most_one): for all v:Set, if v in units(Set,op) then v=u.
      11. (at_most_one, exists)|-for one v:Set( v in units(Set,op)).

      (End of Net)

    3. |- (Monoid_algebra): ALGEBRA(MONOID, Monoid, monoid).
    4. Monoid::=$ MONOID.

      Examples of Monoids

    5. (numbers)|-(S=>Nat, op=>+, u=>0) in Monoid. [ math_42_Numbers.html ]
    6. (strings)|-(S=>#A, op=>., u=>{""})in Monoid. [ math_61_String_Theories.html ]


    7. monoid::={ Set:Sets || (Set,op,u) in $ MONOID},
    8. Monoid::=$ MONOID,
    9. For o, monoid(o)::={ Set:Sets || (Set,o,u) in $ MONOID},
    10. For o,u, monoid(o,u)::={ Set:Sets || (Set,o,u) in $ MONOID}.
    11. For *:infix(T), 1:units(T,*), monoid(*,1)::={S:@T1||MONOID(Set=>S,op=>*,u=>1)}

    12. (STANDARD)|-For (S, *, u):monoid, p:Nat0, x:S^p,
    13. ( *(x) in S
    14. and (if p=0 then *(x)=u)
    15. and (if p=1 then *(x)=x[1] )
    16. and( if p>1 then *(x)=*(x [1..p-1]) * x[p] )
    17. and( if p>1 then for all i:1..p-1( *(x) = *(x[1..i]) * *(x[i+1..p]) )
    18. )

      Extended Semigroups

    19. For S:semigroup(o), u:Things~Set, Λ(Set)=(S=>(Set||{u}),op=>*,u) where if a,b:S then a*b=a o b or else a*u=u*a=a.

    20. (above)|- (ext_semi): F in ((semigroup)S1 a S2 ->((monoid)Lambda(S1) a Lambda(S2))
    21. where F(m)=(m||{(u,u)}where m:(semigroup)S1 a S2)



      1. For M:=(X,o, u) ::Monoid.
      2. sub_monoid(M)::=@X & monoid(o, u),

      3. (above)|- (sub_mon): sub_monoid(M)={X:sub_semigroup(X, o)|| u in X}.
      4. For A:@X, A normal_sub_monoid M::= A normal_sub_semigroup M.(S,o) and u in A,


      5. For M1, M2:monoid(Y,*,v), a:Arrow, (monoid)M1 a M2 ::=(semigroup)M1.(Set,op) a M2.(Set,op) && (u)(M1) a M2.

        Kernel of a monoid morphism.

      6. For f:(monoid)M1 a M2, ker(f)::={x:X||f(x)=u.M2},
      7. (ker)|- (ker1): ker(f) in normal_sub_monoid(M1),
      8. (ker)|- (ker2): M1/f=(M1.Set/f, M1.op/f, ker(f)) in monoid,
      9. (ker)|- (ker3): for all a,b:M1(a/f o/f b/f = (a o b)/f)
      10. (ker)|- (ker4): for all B:M1/f (for some h:ker(f)->B)

        Unlike groups elements in coi(f)= { x./f || x:M2 } are not necessarilly in one-one corespondence.

        Abelian Monoids

      11. abelian_monoid::={ Set:Sets || (Set,op,u) in $ ABELIAN_MONOID},
      12. Abelian_monoid::=$ MONOID,
      13. For o, abelian_monoid(o)::={ Set:Sets || (Set,o,u) in $ ABELIAN_MONOID},
      14. For o,u, abelian_monoid(o,u)::={ Set:Sets || (Set,o,u) in $ ABELIAN_MONOID}.
      15. For *:infix(T), 1:units(T,*), abelian_monoid(*,1)::={S:@T1||ABELIAN_MONOID(Set=>S,op=>*,u=>1)}

      16. (STANDARD)|- (serial): For (Set=>S,op=>+,u=>0): Abelian_monoid, for all A,B:Finite_sets,+(A;f)=+(B;f) + +((A~B);f),
      17. (STANDARD)|- (serial): For (Set=>S,op=>+,u=>0): Abelian_monoid, for B:Finite_sets, p:B---B, +(B;f)=+(B;p;f).

      18. additive_monoid::={Set || $ MONOID(op=>+, u=>0) and Net{+ in commutative(Set)}}.

        When non-Abelian use multiplicative notation:

      19. multiplicative_monoid::={Set || MONOID(op=>(), u=>1) }


      20. For M:Monoid, a:M.Set, a^0::=u,
      21. For M:Monoid, a:M.Set, Nat n, a^n::=a op a^(n-1).
      22. (above)|- (eternal_recurrence_1): For all M:Monoid,a:M, i:0.., j:i+1..( if a^i=a^j then for all k:0.., a^(i+k)=a^(j+k) ).

      23. (above)|- (eternal_recurrence_2): For all M:Monoid,a:M, i:0.., j:i+1..( if a^i=a^j then for all p:0.., a^i=a^(i+p*(j-i)) ).

        These are proved under more restrictive conditions as a result in the theory of relations in Greis and Schneider's "A Logical Approach to Discrete Mathematics".

        Cyclic monoids

      24. cyclic_monoid::={ M:Monoid || for all b:M.Set(some n:Nat0 || b=a^n)},
      25. (above)|- (cyc_ab): cyclic_monoid are Abelian_monoid.
      26. For M:cyclic_monoid, generator(M)::={ b:M.Set || for all a:M.Set, some n:Nat0 (b=a^n)}.

      27. (above)|- (cyc_un_alg): for a:generator(M), (M.Set, map [x](a o x)) in unary_algebra.
      28. (above)|- (cyc_Nat): for M:cyclic_monoid (if not M.Set in Finite then
      29. (monoid)M---(Set=>Nat, op=>+, u=>0).

      30. (above)|- (cyc_fin): for M:cyclic_monoid(if M in finite then for some n,l:Nat, ((monoid)M --- (Set=>0..n, op=>o, u=>0)
      31. where n o m= if a+b<n the a+b else the t:0..n for some k(a+b=n+t+k*l)).

      32. (above)|- (cyc_fin_2): for M:cyclic_monoid(if M in finite then for all x, some n:Nat(x^n in idempotents(M.op)).


      33. For A:@M, #A={A^n||n=0..},
      34. For A:@M, For x,y:#A, x!y=map [i:1..|x|+|y|](if i<=|x| then x(i) else y(i-|x|+1)).
      35. For A:Finite_set, free(A)::=(Set=>#A,op=>(!),u=""),

      36. monoid_generated_by(A,M.op)::=min{B:sub_monoid(M)||A==>B}

      37. generators(M)::={A:@M||monoid_generated_by(A,M.op)=M.Set}

      38. for all A:finite_set(if A in generators(M) then free(A)>--M)
      39. 1::="",
      40. (above)|-1=""=() in A^0

        Monoids defined by generators and relations.

      41. Example::=
        1. What is the smallest monoid with unit 1, operation and element x, such that x x x=1?

        2. M::= (Set=>{1, x, xx}, u=> 1
        3. op=>
        4. ((1,1)+>1 | (1,x)+>x | (1,xx)+>xx |
        5. (x,1)+>x | (x,x)+> xx | (x, xx)+> 1 |
        6. (x, 1)+>xx | (xx, x)+>1 | (xx,xx)+>x ))
        7. )
        8. The above example is M=Monoid( {x} || {x x x} )

        9. Traditional notation is < x | x x x > for both this and the Group generated by x with relators x x x


      42. For A:Finite_set, S:@#A , Monoid(A||S)::=Free(A)/R where R=min{E:congruence(#A)||for all s:S(s E 1)}.

      43. ??For A:Finite_set, S:@#A , Monoid(A||S)=Free(A)/Free(S).?

        Source: Emil Post and others.

      . . . . . . . . . ( end of section Properties) <<Contents | End>>

      Special Cases


      1. SEMILATTICE::=ABELIAN and SEMIGROUP and Net{o in idempotent(S)}.
      2. semilattice::={ Set:Sets || (Set,op,u) in $ SEMILATTICE},
      3. Semilattice::=$ SEMILATTICE,
      4. For o, semilattice(o)::={ Set:Sets || (Set,o,u) in $ SEMILATTICE},

      5. For L:semilattice, (<=) ::=rel [x,y:L](x o y =x)
      6. (above)|- (sl0): (S=>L, relation=>(<=)) in poset
      7. (above)MINMAX and for all x,y, one lub({x,y}), (S,lub">|- (MINMAX and for all x,y, one lub({x,y}), (S,lub">sl1): For (S=>S, relation=>R) in $ MINMAX and for all x,y, one lub({x,y}), (S,lub): semilattice


        If S is a finite set (called the alphabet or vocabulary) then #S is the set of strings on S.

      8. #S::=free_monoid_generated_by(S)

        Operations on Sets

      9. (above)|- (endo_mon): endo(S) in monoid,
      10. (above)|- (maps_mon): (Set=>S^S, op=>;, u=>Id(S)) in monoid.

        Actions of a Monoid

        The edomorphisms of a set form a monoid.
      11. For set S, endo(S)::monoid= MONOID( S>--S, (o), Id(S) ).

        A monoid is an abstract model of most situations in which a set of actions tend to change objects.

      12. For M:monoid, S:set, actions(M,S)::=(monoid)(M)->endo(S).

      13. (above)|-If A in actions(M,S) then A(M.u)=Id(S) and for all a,b:M.Set(A(a M.op b) = A(a);A(b) ).

      14. For A:actions(M,X), m:M.Set, b:X, Operators(S)={Op:S->S||(Set=>Op, op=>(.), u=>1) in monoid and 1=Id(S) and (.)=map g,h(g o h) }.

      15. For M:Operators(S), m:M, m.s=m(s), A[b]::=map m(A(m)(b)),
      16. Field(A)::={A(m)||for some m}.
      17. (above)|-(monoid)Field(A)==>(Set=>X^X, op=>;,u=>I).
      18. Trace(A)::={A[b]||for some b}.

      19. (above)|-A is (monoid)M>--Field(A).
      20. (above)|-Trace(A) in Process(M).

      21. <A>::={(b1,b2):B^2||for some m:M(b2=A(m)(b1))}.
      22. (above)|-<A>=Union(Field(A)).
      23. (above)|-<A> in reflexive and transitive.

      24. For A:action(M,S),b:X,C:@X, invariant::={C||for all m,c:C(A(m)(b)in C)}
      25. (above)|-(Set=>invariant, glb=>&, lub=>|}in lattice

        Invertable elements in a monoid

      26. inverses(x)::={y:M || x o y = y o x = e}.
      27. (above)|- (unique_inverses): 0..1 inverses(x)
      28. Let{
      29. |- (1): y1,y2 in inverse(x),
      30. (1)|- (2): y2 = y2 o u = y2 o (x o y1) = (y2 o x) o y1 = y1,
      31. (trans =)|- (3): y2 = y1
      32. }

      33. invertable(M)::={x:M || some inverses(x)}.
      34. (above)|-u in invertable(M). (unique_inverses) |-For all x:invertable(M), inverse(x) ::= the inverses(y).
      35. (above)|-(invertable(M), o, inverse) in Group.

        Left and Right Operator Monoids

      36. (above)|-(u o_)=(_o u)=Id(M).
      37. (above)|-for x, y, (x o_);(y o _)=((x o y)o _) and (_o x);(_ o y)=(_ o (y o x)).

      38. (above)|-For M:monoid, S:=M.Set, MONOID( {(x o_) || x:S}, o , Id(X)) and MONOID( {(_o x) || x:S}, o , Id(X)).

      . . . . . . . . . ( end of section Special Cases) <<Contents | End>>

    . . . . . . . . . ( end of section Monoids) <<Contents | End>>

    Notes on MATHS Notation

    Special characters are defined in [ intro_characters.html ] that also outlines the syntax of expressions and a document.

    Proofs follow a natural deduction style that start with assumptions ("Let") and continue to a consequence ("Close Let") and then discard the assumptions and deduce a conclusion. Look here [ Block Structure in logic_25_Proofs ] for more on the structure and rules.

    The notation also allows you to create a new network of variables and constraints. A "Net" has a number of variables (including none) and a number of properties (including none) that connect variables. You can give them a name and then reuse them. The schema, formal system, or an elementary piece of documentation starts with "Net" and finishes "End of Net". For more, see [ notn_13_Docn_Syntax.html ] for these ways of defining and reusing pieces of logic and algebra in your documents. A quick example: a circle might be described by Net{radius:Positive Real, center:Point, area:=π*radius^2, ...}.

    For a complete listing of pages in this part of my site by topic see [ home.html ]

    Notes on the Underlying Logic of MATHS

    The notation used here is a formal language with syntax and a semantics described using traditional formal logic [ logic_0_Intro.html ] plus sets, functions, relations, and other mathematical extensions.

    For a more rigorous description of the standard notations see

  1. STANDARD::= See http://www.csci.csusb.edu/dick/maths/math_11_STANDARD.html


  2. above::reason="I'm too lazy to work out which of the above statements I need here", often the last 3 or 4 statements. The previous and previous but one statments are shown as (-1) and (-2).
  3. given::reason="I've been told that...", used to describe a problem.
  4. given::variable="I'll be given a value or object like this...", used to describe a problem.
  5. goal::theorem="The result I'm trying to prove right now".
  6. goal::variable="The value or object I'm trying to find or construct".
  7. let::reason="For the sake of argument let...", introduces a temporary hypothesis that survives until the end of the surrounding "Let...Close.Let" block or Case.
  8. hyp::reason="I assumed this in my last Let/Case/Po/...".
  9. QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.
  10. QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.
  11. RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.