Group Theory

Motivation

Basics

monoids::= See http://csci.csusb.edu/dick/maths/math_33_Monoids.html
|- (basis): monoids.
GROUP::=following
Net
1. Set::Sets,
2. op::=operation::Associative(Set),
3. u::=unit::units(Set,op).
4. |- (G0): MONOID(Set, op, u).
5. i::=inverse::Set->Set,
6. |- (G1): for all x:Set, x op i(x)=u=i(x) op x.
  [ Properties ]
(End of 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. Georges Pappy's book on Groups and Birkhoff and Bartee 70, page 213.
|-Group=$ PAPPY.
PAPPY::=following
Net
1. A semigroup in which equations can be solved.
2. |- (PG0): SEMIGROUP(Set, op).
3. u::Set.
4. i::Set---Set.
5. |- (PG1): for all a,b:Set, some x,y :Set (a op x = b = y op a).
6. (PG1)|- (PGu): u= the x (for all a (a op x=a=y op a)).
7. (PG1, PGu)|- (PGi): i= the i( for all a ( a op i(a) =u)).
  
  Proof of PGu
  
  Let
  1. |-a:G.
  2. (PG1(a=>a, b=>a))|-for some x,y:Set(a op x=a=y op a).
  3. (above)|-some left_units and some right_units.
  4. (above)|-one unit.
  (Close Let )
  
  Proof of PGi
  
  Let
  1. |-a:G,
  2. (PG1(a=>a, b=>u))|-inverses
  3. ...
  (Close Let )
(End of Net)
Properties
[ unique_inverses in math_33_Monoids ]
(above)|- (unique unit): For all Group G, one u:G ( for all x:G( x op u = u op x = x)).
(above)|- (unique inverse): For all Group G, one i:G ( for all x:G( x op i(x)= u )).
(above)|- (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).
(above)|- (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) ) .
(above)|- (inv unit): For G, i(u)=u.
(above)|- (dist inv): For G, i(a op b) = i(b) op i(a).
Note, that by the STANDARD defitions (op) is a serial operator, [ math_11_STANDARD.html ]
(above)|- (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? [ Gallian & Reid 93, "Abelian Forcing Sets", Am Math Monthly June-July 93 pp580-582] .
FREE_GROUP::=
Net{
1. Elements::Finite_sets.
2. Inverse::Elements --- Elements.
3. |-GROUP( Set=> #( Elements | Inverses), op=>(!), u=>(), i=>Inverse).
4. |-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, ...)}.
(above)|-Free_group(S,i)=Monoid( S || for all s( s i(s) = i(s) s = u ) ).

Multiplicative Groups
1. For G:m_group~numeric, x,y:G, x^y::=y^-1.x.y
2. For groups that contain numbers x^n is ambiguous - use x^^y for congruency
  Commutator
3. For G:m_group, x,y:G, [x,y]::=x^-1.y^-1.x.y
. . . . . . . . . ( end of section Multiplicative Groups) <<Contents | End>>

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 [ 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
1. G:: group(o, u, i) = given,
2. X:: Sets = given,
3. *::G >< X -> X.
4. |- (GA1): for all x, u * x = x
5. |- (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},
6. x1 ~ x2::= for some g, g*x1=x2.
7. G x::= x/~.
8. (above)|-for x, G x sub_group G.
9. (above)|-|G x| = |G : G[x]| = |G| / |G[x]|.
10. orbit = {G x || for some x}.
11. (above)|-(burnside_s_lemma) : |orbit| * |G| = +[g:G] (X[g]).
(End of 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).
(above)|-for H:@G(H sub_group G iff for all x,y:H(x op i(x) in H).
(above)|-{{u},G}==>sub_groups(G).
(above)|-(Set=>sub_groups(G),R=>==>)in poset.
For A:@G, <A>::=min{H:subgroups(G)||A==>H}.
(above)|-<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}. Birkhoff & Bartee 70
(above)|-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{
1. G::m_group,
2. H::sub_groups(G).
3. (def)|- (C1): x/H={y || y.H=x.H},
4. (def)|- (C2): left_cosets(H,G)= G/(=wrt H).
5. (def)|- (C3): For x,y,H, x=y wrt H iff y^-1.x in H
6. (above)|-(C4) for all x:G (x.H=x/H).
  Proof of C4
7. Let{ x:G,
8. (C4.0): x/H={y||y.H=x.H},
9. (above)|- (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).
10. LHS::= for all h,some g(y=x g h^-1)&for all h, some g(y=x h g^-1),
11. RHS::=for some h(y=x h).
12. (above)|- (C4.2): if LHS then RHS.
13. (above)|- (C4.3): if RHS then LHS.
14. 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,
(above)|- (C4.3.2): y=x h0.
(above)|- (C4.3.3): for some h,all g(y<>x g h^-1) or for some h, all g(y<>h g^-1)
(above)|- (C4.3.4): all g(y<>x g h1^-1) or all g(y<>x g h1^-1)
(above)|- (C4.3.5): either all g(y<>x h1 g^-1) or all g(y<>x h1 g^-1)
(above)|- (C4.3.6): y<>x h0 h1 h1^-1
(above)|- (C4.3.7): g=h1 h0
}.

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

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

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

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

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

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

Burnside's Theorem

(above)|- (burnside): For G:m_group, H:normal(G), |G| = |G/H| * |H|.

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

(above)|-for all G1,G2:group, f:(group)G1>--G2, |G1|=|G2|*|ker(f)|

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

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

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

(above)|- (GP0): for all s(G/s in m_group).

(above)|- (GP1): for all s(G/s(group)==>G).

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

(above)|-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 [click here

if you can fill this hole]

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.
(above)|-For all K, |G|= |fix[G](K)| . |Orb[G](K)|, #orbit(G)=+[g:G]|a/g|/|G|

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

. . . . . . . . . ( end of section Permutation Groups and the Symmetric Groups) <<Contents | End>>

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

[click here

if you can fill this hole]

. . . . . . . . . ( end of section Group Theory) <<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 = Net{radius:Positive Real, center:Point}.

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

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

Glossary

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

given::reason="I've been told that...", used to describe a problem.

given::variable="I'll be given a value or object like this...", used to describe a problem.

goal::theorem="The result I'm trying to prove right now".

goal::variable="The value or object I'm trying to find or construct".

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.

hyp::reason="I assumed this in my last Let/Case/Po/...".

QED::conclusion="Quite Easily Done" or "Quod Erat Demonstrandum", indicates that you have proved what you wanted to prove.

QEF::conclusion="Quite Easily Faked", -- indicate that you have proved that the object you constructed fitted the goal you were given.

RAA::conclusion="Reducto Ad Absurdum". This allows you to discard the last assumption (let) that you introduced.

Contents

Group Theory

Motivation

Proof of PGi

Congruency

Commutator

Proof of C4

Proof of C4.3

Proof of laplace

Glossary