group1
http://www.openmath.org/cd/group1.ocd
2003-04-01
1999-05-10
2
0
experimental
alg1
arith1
fns1
fns2
logic1
nums1
quant1
relation1
set1
setname1
A CD of functions for group theory
Written by A. Solomon on 1998-11-19
Modified by David Carlisle 1998-04-28
declare_group
This symbol is a constructor for groups. It takes four arguments in
the following order; a set to specify the elements in the group, a
binary operation to specify the group operation, a unary operation to
specify inverses of group elements and an element to specify the
identity. Both the binary and unary operations should act on elements
of the set and return an element of the set.
A group is closed under its operation.
A groups operation is associative.
A group has an identity element.
Every element of a group has an inverse.
This example represents the group which has as elements all positive
and negative even numbers, the group operation is binary addition,
inverses are the negative of the element and the identity is the zero
element.
2
is_abelian
The unary boolean function whose value is true iff the argument is an abelian group
If is_abelian(G) then for all a,b in element_set(G) a*b = b*a
group
The n-ary function Group. The group generated by its arguments.
The arguments must have a natural group operation associated with them.
element_set
The unary function which returns the set of elements of a group.
is_subgroup
The binary function whose value is true if the second argument is a subgroup of the first.
A is a subgroup of B implies element_set(A) is a subset of element_set(B)
right_transversal
The binary function whose value is a set of representatives for the right cosets
of the second argument as a subgroup of the first.
normal_closure
The binary function whose value is the set of conjugates of
the elements of the second group by elements of the first,
where multiplication between them is defined.
n in the normal closure (A,B) implies
there exists a in A and b in B s.t. n = b^(-1) a b
is_normal
If G, H are the group arguments, then IsNormal(G,H) returns true precisely when
G is normal in H. That is, g^-1*h*g is defined and contained in H for
all h in H and g in G.
is_normal(G,H) implies that for all g in G and h in H then
g^-1*h*g is in H
quotient_group
The binary function whose value is the factor group of the first argument by the
second, assuming the second is normal in the first.
conjugacy_class
The binary function whose value is the set of elements which
are conjugate to the second argument in the first.
The conjugacy class in G with respect to h = {g^(-1) h g | g in G}
derived_subgroup
The unary function whose value is the subgroup of argument
generated by all products of the form xyx^-1y^-1.
d in the derived subgroup of G implies
there exist x,y in G such that d=x y x^(-1) y^(-1)
sylow_subgroup
The largest p-subgroup of the argument (up to conjugacy).
character_table_of_group
Refers to the character table of its argument
which must be a group.
character_table
This is the constructor for a character table.
Usage:
CharacterTable(centralizer_primes, centralizer_indices,
classnames, power_map, irreducibles_matrix)
If G has n conjugacy classes then:
* centralizer_primes is of the form
[p1, .., pk] i < j implies that pi < pj and
the pi are precisely the primes which divide the order of
some centralizer of a conjugacy class
* centralizer_indices is of the form
[[i11, ...,i1k] ... [in1,...ink]]
so the centralizer of class 1 has order p1^i11 ... pk^i1k etc
* classnames is a list of n strings which name the conjugacy classes
in line with the convention used in the Atlas of Finite Groups
* power_map is of the form [list1, ..., listk]
where listi[j] is the name of the class where elements of class j go when
raised to the power pi.
* irreducibles_matrix: rows correspond to irreducible characters,
columns are conjugacy classes. Entries are the value of an element of the
column's conjugacy class under the character of the row.