.Open Monoids
. Motivation
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
The following is used in
.See http://www/dick/maths/math_31_One_Associative_Op.html
and
.See http://www/dick/maths/math_34_Groups.html
MONOID::=SEMIGROUP and following,
.Net
	u::units(Set,op). 
	()|-(nt):nontrivial.
	()|-(unit_sq): u op u = u.
	()|-(unique_unit): for one v:Set( v in units(Set,op)).

. Proof of nt
	(u)|-u isa Set,
	()|- some Set,
	(SEMIGROUP.nontrivial)|-nontrivial.

. Proof of unique_unit
()|-(given): u in units(Set,op).
(given)|-(exists): for some v:Set( v in units(Set,op)).
.Let 
	v:Set, 
	(0): v in units(Set,op).
	(u is unit) |-(1): u op v = u.
	(v is unit) |-(2): u op v = v.
	(1,2)|-(3): u=v.
.Close.Let
()|-(at_most_one): for all v:Set, if v in units(Set,op) then v=u.
(at_most_one, exists)|- for one v:Set( v in units(Set,op)).

.Close.Net

	|- (Monoid_algebra):ALGEBRA(MONOID, Monoid, monoid).
Monoid ::=$ $MONOID.	
. Examples
	(numbers)|- (S=>Nat,  op=>`+`, u=>0) in Monoid.
.See http://www/dick/maths/math_42_Numbers.html
	(strings)|- (S=>#A, op=>`.`, u=>{""})in Monoid.
.See http://www/dick/maths/math_61_String_Theories.html

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

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


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

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

.Open Properties

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

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

. Morphisms
 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.
   For f:(monoid)M1 a M2, ker(f) ::={x:X||f(x)=u.M2},
	(ker)|-(ker1):   ker(f) in normal_sub_monoid(M1),
	(ker)|-(ker2):  M1/f=(M1.Set/f, M1.op/f, ker(f)) in monoid,
	(ker)|-(ker3):for all a,b:M1(a/f o/f b/f = (a o b)/f)
	(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
abelian_monoid::={ Set:Sets || (Set,op,u) in $ $ABELIAN_MONOID}, 
Abelian_monoid::=$ $MONOID, 
 For o, abelian_monoid(o) ::={ Set:Sets || (Set,o,u) in $ $ABELIAN_MONOID}, 
 For o,u, abelian_monoid(o,u) ::={ Set:Sets || (Set,o,u) in $ $ABELIAN_MONOID}.
 For *:infix(T), 1:units(T,*), abelian_monoid(*,1) ::={S:@T1||ABELIAN_MONOID(Set=>S,op=>*,u=>1)}

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

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

When non-Abelian use multiplicative notation:
multiplicative_monoid::={Set || MONOID(op=>(), u=>1) }

. Powers
 For M:Monoid, a:M.Set, a^0::=u, 
 For M:Monoid, a:M.Set, Nat n, a^n::=a op a^(n-1).
 ()|- (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) ).

 ()|- (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
    cyclic_monoid ::={ M:Monoid || for all b:M.Set(some n:Nat0 || b=a^n)},
()|-(cyc_ab):   cyclic_monoid are Abelian_monoid.
    For M:cyclic_monoid, generator(M) ::={ b:M.Set || for all a:M.Set, some n:Nat0 (b=a^n)}.

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

    ()|-(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)
                        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)).

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

. Generation
 For A:@M, #A={A^n||n=0..},
 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)).
     For A:Finite_set, free(A) ::=(Set=>#A,op=>(!),u=""),

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

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

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

. Monoids defined by generators and relations.


    Example::=Net{ 
	What is the smallest monoid with unit 1, operation ` ` and element x, such that x x x=1?

             M::= (Set=>{1, x, xx}, u=> 1
               op=>
               ((1,1)+>1 | (1,x)+>x | (1,xx)+>xx |
                 (x,1)+>x | (x,x)+>  xx | (x, xx)+> 1 |
                  (x, 1)+>xx | (xx, x)+>1 | (xx,xx)+>x ))
              )
 	The above example  is M=Monoid( {x} || {x x x} )

	Traditional notation is `< x | x x x >` for both this and the Group generated by x with relators x x x
	}=::Example.

       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)}.

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

.Source Emil Post and others.
.Close Properties

.Open Special Cases
. Semilattices
SEMILATTICE::=ABELIAN and SEMIGROUP and Net{o in idempotent(S)}.
semilattice::={ Set:Sets || (Set,op,u) in $ $SEMILATTICE}, 
Semilattice::=$ $SEMILATTICE, 
 For o, semilattice(o) ::={ Set:Sets || (Set,o,u) in $ $SEMILATTICE}, 

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

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

	#S::=free_monoid_generated_by(S)

. Operations on Sets

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

. Actions of a Monoid
The edomorphisms of a set form a monoid.
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.

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

()|- 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) ).

 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) }.

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

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

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

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

. Invertable elements in a monoid
      inverses(x) ::={y:M ||  x o y = y o x = e}.
   ()|-(unique_inverses): 0..1 inverses(x)
      Let{ 
	|-(1): y1,y2 in inverse(x),
          (1) |- (2): y2 = y2 o u = y2 o (x o y1)  = (y2 o x) o y1 = y1,
             (trans =) |- (3): y2 = y1
      }

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

. Left and Right Operator Monoids
()|- (u o_)=(_o u)=Id(M).
()|-for x, y, (x o_);(y o _)=((x o y)o _) and (_o x);(_ o y)=(_ o (y o x)).

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

.Close Special Cases

.Close Monoids