.Open Group Theory
. Motivation
Groups turn up whenever we have a set of reversible operations.  The
numbers with adddition, numbers (without zero) and multiplication, the
movements of a figure on the plane, or a beer glass in space all
follow a similar pattern of operations that we call a group.
A group is anything that has most of the algebraic properties of the 
numbers with
respect either addition.  Groups are are a rich and well 
explored algebra.

. Basics
monoids::=http://www/dick/maths/math_33_Monoids.html

|-(basis): $monoids.

GROUP::=following
.Net
	Set::Sets,
	 op::=operation::Associative(Set),
	 u::=unit::units(Set,op).
	|-(G0): MONOID(Set, op, u).
	 i::=inverse::Set->Set,
        |-(G1): for all x:Set, x op i(x)=u=i(x) op x.

.See Properties
.Close.Net



	|-(Group_is_algebra): ALGEBRA($GROUP, Group, group).

	(Group_is_algebra)|- Group::=$ $GROUP. 
	(Group_is_algebra)|- group::={Set:Sets || $GROUP(Set, op, u, i)}, 

group::={Set:Sets || $GROUP(Set, operation=>(1st), unit=>(2nd), inverse=>(3rd))}.
monoid::Group->Monoid=(Set=>(_).Set, operation=>(_).operator, unit=>(_).unit).
semigroup::Group->Semigroup=(Set=>(_).Set, operator=>(_).operator).
congruence::Group->Equivalence_relations=congruence(monoid(_)).


. Alternative definition 
	|-(one-sided): Given just left identities and inverse then a monoid must be a group.
.Source Georges Pappy's book on Groups and Birkhoff and Bartee 70, page 213.
|- Group=$ $PAPPY.
PAPPY::=following
.Net
  A semigroup in which equations can be solved.
	|-(PG0): SEMIGROUP(Set, op).   
	u::Set.  
	i::Set---Set.
	|-(PG1): for all a,b:Set, some x,y :Set (a op x = b = y op a). 
	(PG1)|-(PGu): u= the x (for all a (a op x=a=y op a)).
	(PG1,PGu)|-(PGi): i= the i( for all a ( a op i(a) =u)).

. Proof of PGu
.Let
	|- a:G.
	 (PG1(a=>a, b=>a))|- for some x,y:Set(a op x=a=y op a).
		()|- some left_units and some right_units.
		()|-one unit.
.Close.Let
. Proof of PGi
.Let
	|- a:G,
	(PG1(a=>a, b=>u)) |- inverses
		...
.Close.Let
.Close.Net

. Properties
.See http://www/dick/maths/math_33_Monoids.html#unique_inverses
()|- (unique unit): For all Group G, one u:G ( for all x:G( x op u = u op x = x)).
()|-  (unique inverse): For all Group G, one i:G ( for all x:G( x op i(x)= u )).
()|-  (cancelation): For all Group G, for all a:G ( for all x,y(if a op x = a op y then x=y) and for all x,y(if x op a = y op a then x=y).
()|-  (solve equation): For all G,a,b( for one x( a op x =b) and one x ( x op a =b ) ) 
	and For all G,a,b( the x( a op x =b)=  i(a) op b and the x ( x op a =b )=b op i(a)  ) .
()|-(inv unit): For G, i(u)=u.
()|-(dist inv): For G, i(a op b) = i(b) op i(a).

Note, that by the STANDARD defitions (op) is a serial operator,
.See http://www/dick/maths/math_11_STANDARD.html

()|-(sum): For G, A,B:Finite_Sets, f:G^(A|B),  op(f) = op(f o B) op op(f o B) op i( op(f o (A&B))).


. Special groups
m_group::=multiplicative_group.
multiplicative_group::={Set||$GROUP(op=>., u=>1, i=>map s(s^-1)) and Net{ For x,y:Set, (x y):=x.y}}.

a_group::=additive_group.
additive_group::={Set||$GROUP(op=>+, u=>0, i=>-) and Net{+ in commutative(Set)}}.

Abelian_group::=$ $GROUP and Net{ op in commutative(Set)}
   Traditionally commutative groups use additive notation while non_commutative groups use the multiplicative notation:

Do properties like (ab)^n=a^n b^n force a group to be abelian?
.See Gallian & Reid 93, "Abelian Forcing Sets", Am Math Monthly June-July 93 pp580-582.

FREE_GROUP::=Net{
	Elements::Finite_sets.
	 Inverse::Elements --- Elements.
	|- $GROUP( Set=> #( Elements |  Inverses), op=>(!), u=>(), i=>Inverse).
	|- For all s1,s2:Set, e:Elements,  s1 ! e ! Inverse(e) ! s2 = s1! s2.
}=::FREE_GROUP.

 For S:Finite_sets, i:S---S, Free_group(S, i)={Set || FREE_GROUP( Elements=>S, Inverse=>i, ...)}.

	()|- Free_group(S,i)=Monoid( S ||  for all s( s i(s) = i(s) s = u ) ).

.Open Multiplicative Groups
. Congruency
   For G:m_group~`numeric`, x,y:G, x^y::=y^-1.x.y
    For groups that contain numbers x^n is ambiguous - use x^^y for congruency
. Commutator
	For G:m_group, x,y:G, [x,y]::=x^-1.y^-1.x.y
.Close Multiplicative Groups

. Actions of a Group
The isomorphisms of a set form a group.
For set S, iso(S)::group= $GROUP( S---S, (o), Id(S), (map[i](/i)) ).

As in $monoid theory, we can define the actions of a group -- but the actions must be reversible:
For M:group, S:set, actions(M,S)::=(group)(M)->iso(S).

Most of the results
.See ./math_33_Monoids.html#Actions of a Monoid
for monoids can be applied to Actions of a Group as well.
We can also show some new results like the Burnside Lemma

Here is a more traditional presentation of actions of a group action
GROUP_ACTION::=following
.Net
	G:: group(o, u, i) = $given,
	X:: Sets = $given,
	*:: G >< X -> X.
	|-(GA1): for all x, u * x = x
	|-(GA2): for all x, g1,g2, (g1 o g2) * x = g1 * ( g2 * x).
	
We say that X is a G-Set.

	G[x] ::= {g || g*x = x},
	X[g] ::= {x || g*x = x},
	x1 ~ x2 ::= for some g, g*x1=x2.
	G x ::= x/~.
(above)|- for x, G x $sub_group G.

(above)|- |G x| = |G : G[x]| = |G| / |G[x]|.

	orbit = {G x || for some x}.

(above)|- (burnside_s_lemma) : |orbit| * |G| = +[g:G] (X[g]).



	

.Close.Net GROUP_ACTION

. Subgroups
 For G:$ $GROUP, subgroups(G) ::={ H:@G||H in $ $GROUP},
 For H,G, H sub_group G::= H in subgroups(G).
     ()|- for H:@G(H sub_group G iff for all x,y:H(x op i(x) in H).
     ()|- {{u},G}==>sub_groups(G).
     ()|- (Set=>sub_groups(G),R=>`==>`)in poset.
    For A:@G,  <A>::=min{H:subgroups(G)||A==>H}.
     ()|-<A>={op(x)||x:#(A|i(A))} =( H:@G||for all a:A,h:H({h^-1, a op h, h op a}==>H)).

normal(G) ::=normal_subgroups(G)::={H:subgroups(G)||for all x:G(x.H=H.x)}.

 For X,Y:subgroups(G), X orthogonal Y::@=( X&Y={u} and X op Y =G).

. Generators and Relators

 For S:@G, generated_group(S) ::=the smallest { H : subgroups(G) || S==> H }.
.Example 
DIHEDRAL::=Net{n:Nat. n>2.  m_group(#{R, V}).  V V=1.  R^n=1. R V  = V R^-1.}

    For A:Finite_set, i: A---A, S:@#A , Group(A||S) ::=Free_group(A, i )/R
              where R=min{E:congruence(#A)||for all s:S(s E 1)}
So the Dihedral group G in $ $DIHEDRAL is isomorphic to Group({R,V}|| VV, V^-1 R V R^-1, R^n).

. Morphisms
 For G1,G2:$ $GROUP, a:arrow, (group)G1 a G2::=(monoid) Monoid(G1) a  Monoid(G2)& {f || f o i=i o f}.
.Source Birkhoff & Bartee 70
()|- For G1,G2:$ $GROUP, a:arrow, (group)G1 a G2 :- (semigroup) Semigroup(G1) a  Semigroup(G2).
.Note However a semigroup morphism between monoids may not be a monoid morphism.

. Left Cosets.
 For G:m_group, H: sub_groups(G), x,y:G, (x = y wrt H) ::=(x.H=y.H),
     (=wrt H) ::=rel [x,y](x=y wrt H),
      for x:G, x/H::=x/(=wrt H),
       left_cosets(H,G) ::=G/H.

|-(LC0): For G,H,  (=wrt H) in congruence(monoid(G)).

COSETS::=Net{ 
	G::m_group, 
	H::sub_groups(G).
  (def)|-(C1): x/H={y || y.H=x.H},
 (def) |-(C2): left_cosets(H,G)= G/(=wrt H).
  (def)|-(C3): For x,y,H, x=y wrt H iff y^-1.x in H
  ()|-(C4) for all x:G (x.H=x/H).
. Proof of C4
         Let{ x:G,   
		(C4.0): x/H={y||y.H=x.H},
            ()|-(C4.1):  ( for all h,some g(y=x g h^-1) and for all h, some g(y=x h g^-1)  iff for some h(y=x h).
               LHS::= for all h,some g(y=x g h^-1)&for all h, some g(y=x h g^-1),
               RHS::=for some h(y=x h).
            ()|-(C4.2): if LHS then RHS.
            ()|-(C4.3): if RHS then LHS.
               x/H= {y||for some h(y=xh)}
         }.

. Proof of C4.2
                Let{ 
	|-	(C4.2.0): LHS, 
	|-	(C4.2.1):not RHS.
                  (C4.2.1)|- (C4.2.2): for all h(y<>x h).
                  (C4.2.0)|- (C4.2.3): for all h, some g(y=x g h^-1).
                  (C4.2.0)|- (C4.2.4): for all h, some g(y=x h g^-1).
     (C4.2.3, h:=h0, g:=g0) |-(C4.2.5):        y=x g0 h0^-1  .
      (C4.2.2, h:=g0 h0^-1) |- (C4.2.6):       y<>x g0 h0^-1  .
	(C4.2.5, C4.2.6)|- y <> y.
                  }.
. Proof of C4.3
           Let{ 
	|-(C4.3.0): not LHS, 
	|-(C4.3.1): RHS, 
                  ()|-(C4.3.2):y=x h0.
                  ()|-(C4.3.3): for some h,all g(y<>x g h^-1) or for some h, all g(y<>h g^-1)
                  ()|-(C4.3.4): all g(y<>x g h1^-1) or all g(y<>x g h1^-1)
                  ()|-(C4.3.5):   either all g(y<>x h1 g^-1) or all g(y<>x h1 g^-1)
                  ()|-(C4.3.6):  y<>x h0 h1 h1^-1
                  ()|-(C4.3.7):  g=h1 h0
                }.

         ()|-(C4.4):for all x:G(x.H in G/H).

         ()|-(C4.5): for all x:G (A;(x._) in A---x.A).

         ()|-(C4.6):for all x:G, (x.A);(x^-1._) = / (x._).

         ()|-(C4.7): for all A:G/H( A---H ).

()|- (C4.8): If H in normal(G),  map[x](x/H) in (group)G>==G/H
}=::COSETS.

()|- For all G,H(COSETS).

.  Burnside's Theorem
 ()|-(burnside): For G:m_group, H:normal(G), |G| = |G/H| * |H|.

()|-For G1,G2:group, f:(group)G1->G2, ker(f) in normal(G1) and G1/ker(f)=coi(f)

()|-for all G1,G2:group, f:(group)G1>--G2, |G1|=|G2|*|ker(f)|
()|-For H,K:normal(G), if H==>K then G/H>--G/K
|-For G,X:group, x:(group)G->X, some Y:group, y:(group)G->Y ( G---$ Net{x:X y:Y}and ker(x)orthogonal ker(y) ).

. Direct Sum
 ()|-For H,K:sub_group(G), G---H><K iff H orthogonal K and for all h:H,k:K(h.k=k.h)

. Abelian Direct sums
 ()|-For G:a_group, A,B:sub_group(G), G---A><B iff A orthogonal B.

. Direct products of Groups
     For G:m_group, p:1.., G^p=G^(1..p).
     For G:m_group, S:Set, G^S in m_group and
	for all f,g:G^S
		 f.g=map x(f(x).g(x))
	    and	f^-1=map x((f(x))^-1)
	    and	1= map x(1).

     For G1,G2:m_group, S:Set, h:(group)G1->G2, (h o (_)) in G1^S(group)->G2^S.
     For G1,G2:group, G1><G2::= the $GROUP( Set=> G1.Set><G2.set, op=>  map x,y:Set((x(1) G1.op y(1),x(2) G2.op y(2))), u=>   (G1.u, G2.u), i=>    map x((G1.i(x(1)),G2.i(x(2))))  ).

. Bilinear Maps in Abelian Groups
	For A,B,C:a_group,(bilinear) A><B->C::={f^C(A><B) || for all a:A( (f(a,(_)))in (group)B->C) and for all b:B((f((_),b)) in (group) A->C).


. Groups of permutations of a set
 For S:Set, permutations(S) ::={G:operators(S)||for g in G(g:S---S)}

 For A are G, T are S, A.T={g.s||g in A and s in T},
              G/s::={g || g.s=s},
              S/g::={s || g.s=s},
              Orbit(T) ::={G.{s} || s in T},
              Isotropy(G,s) ::={/s || s in S,
              invariant(T)(G) ::={T/g || g in G},
              s1(= mod G)s2::=s1=s2 wrt G ::= for some g(x=g y).

    ()|-(GP0): for all s(G/s in m_group).
    ()|-(GP1): for all s(G/s(group)==>G).
    ()|-(GP2): (=mod G) in equivalence_relation
(burnside) |-(GP3): |S/(=mod G)| = +[g:G](|S/g|)/|G|
                `Average orbit`

 For S:Set, G:permutations(S), base(S,G) ::={B:@S|| G.B=S and no (G~{1}).B &B}.

      for all s:S, one (b,g):B><G(s=g.b),
 ??     for all B'=>>B, B' not_in base,           ?
 ??     for all B'<<=B, B' not_in base(s,G),    ?
      for all B1,B2:Base(S,G)( B1---B2),  S---B><G.

 ()|-For S:Set, G:permtuations(S), s:S, G/s={g || g.s=s}, some (group)G/S->G
   For S:Set, G:permutations(S), s:S, x,y:G, x=y wrt s ::= x.s=y.s.

|-For S:Set, G:permutations(S), s:S, x,y:G, 
              		x=y wrt s in equivalence_relation(G)
              	and	x=y wrt G/S iff x=y wrt s
.Hole

.Open Permutation Groups and the Symmetric Groups

 For n:Nat, S(n) ::=Symmetric_group(n)::=(Set=>(1..n---1..n), op=>o, u=>I, i=>(/))
            Use multiplicative notation

. Cycle notation            
   for l:1..m-->1..n,
     cycle(l)=if j=l^-1(i) then
                 if j<m then l(j+1)
                  else l(1)
               else i

for f:Nat, f_cycle(p)={q || for some m:Nat0(q=f^n(p))},
                f_period(p)=min{m:Nat0||f^m(p)=p}


. Cannonical decomposition
 For f:S[n], f=Pi i:1..l(cycle(l(i)))
         and for all i<j ( no (img(l[i])&img(l[j] and l[i](1)=l[j](1))
         and for all i(l[i](1)=min img l[i])

. Congruent permutations
 For G sub_group S[n]
              for s,t:G, s--t ::= for some g:G(s=g t g^-1)

. Type of a permutation in S[n]
type(f) ::=map i(|l[i]| where l=`the cannonical cyclic decomposition`)
|- s--t iff type(s)=type(t)

. Orbits
 For G subgroup S[n], X=1..n,
   (x=y wrt G) ::= some g in G(x=g(y)),
   orbit(G) ::=X/=wrt G,
   fix[G](K) ::= {g:G||g[k]=g},
   Orb[G](K) ::=k/=wrt G.

()|- For all K, |G|= |fix[G](K)| . |Orb[G](K)|, #orbit(G)=+[g:G]|a/g|/|G|

. Laplace's Theorem
()|- (laplace): for all G:Finite&Group, some n:Nat0((group)G-->S[n])
. Proof of laplace
Let {
	|-n=|G|, 
	()|- some c: G---1..n.(c:G---1..n)
	()|- c in G---1..n  and /c in 1..n---G and c;/c=Id(G) and /c;c=Id(1..n).
	e:=map [x:G](/c;(x._);c).
	()|- (1): for each a, e(x) in S[n],
	()|- (2): e(1)=S[n].unit.
	()|- (3): e(a.b)=e(a) e(b).
(1,2,3)	|- (4): e in (group)G->S[n]
	()|- (5): for a<>b, e(a)<> e(b).
       (5)	|- e in (group)G-->S[n]
}
.Close Permutation Groups and the Symmetric Groups

. Geometries, pattern and symmetry

Studying the symmetry groups of objects in space is a way of studying space itself.

It is also put to use in chemistry and physics wherein the categorisation of all possible symetries in 3 and 4 dimensional space has some significant implications.  M C Escher's research into the symetry's of 2 dimensional space is the basis of much of his art.

. Supplements and factors
.Hole

.Close Group Theory