<CD>
<CDName> group1 </CDName>
<CDURL> http://www.openmath.org/cd/group1.ocd </CDURL>
<CDReviewDate> 2000-09-01 </CDReviewDate>
<CDDate> 1999-05-10 </CDDate>
<CDVersion> 2 </CDVersion>
<CDRevision> 0 </CDRevision>
<CDStatus> experimental </CDStatus>
<CDUses>
  <CDName>alg1</CDName>
  <CDName>arith1</CDName>
  <CDName>fns1</CDName>
  <CDName>fns2</CDName>
  <CDName>logic1</CDName>
  <CDName>nums1</CDName>
  <CDName>quant1</CDName>
  <CDName>relation1</CDName>
  <CDName>set1</CDName>
  <CDName>setname1</CDName>
</CDUses>
<Description> A CD of functions for group theory   </Description>

<CDComment>
Written by A. Solomon on 1998-11-19
Modified by David Carlisle 1998-04-28
</CDComment>

<CDDefinition>
<Name> declare_group </Name>
<Description>
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.
</Description>

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

<OMOBJ>
<OMA>
  <OMS cd="group1" name="declare_group"/>
  <OMA>
    <OMS cd="set1" name="suchthat"/>
    <OMS cd="nums1" name="Z"/>
    <OMBIND>
      <OMS cd="fns1" name="lambda"/>
      <OMBVAR>
        <OMV name="x"/>
      </OMBVAR>
      <OMA>
        <OMS cd="set1" name="in"/>
        <OMA>
          <OMS cd="arith1" name="divide"/>
          <OMV name="x"/>
          <OMI> 2 </OMI>
        </OMA>
        <OMS cd="setname1" name="Z"/>
      </OMA>
    </OMBIND>
  </OMA>
  <OMS cd="arith1" name="plus"/>
  <OMS cd="arith1" name="unary_minus"/>
  <OMS cd="alg1" name="zero"/>
</OMA>
</OMOBJ>
</Example>

</CDDefinition>

<CDDefinition>
<Name> is_abelian </Name>
<Description>
The unary boolean function whose value is true iff the argument is an abelian group
</Description>

<CMP>
If is_abelian(G) then for all a,b in element_set(G) a*b = b*a
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="group1" name="is_abelian"/>
      <OMV name="G"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="a"/>
        <OMV name="b"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="group1" name="element_set"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="group1" name="element_set"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="b"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>

<CDDefinition>
<Name> group </Name>
<Description>
The n-ary function Group. The group generated by its arguments.
The arguments must have a natural group operation associated with them.
</Description>

<CMP>
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.
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="G"/>
      <OMA>
        <OMS cd="fns2" name="apply_to_list"/>
        <OMS cd="group1" name="group"/>
        <OMV name="listofgens"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="a"/>
        <OMV name="b"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="implies"/>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="a"/>
            <OMA>
              <OMS cd="group1" name="element_set"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="group1" name="element_set"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
        <OMBIND>
          <OMS cd="quant1" name="exists"/>
          <OMBVAR>
            <OMV name="c"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="and"/>
            <OMA>
              <OMS cd="set1" name="in"/>
              <OMV name="c"/>
              <OMA>
                <OMS cd="group1" name="element_set"/>
                <OMV name="G"/>
              </OMA>
            </OMA>
            <OMS cd="relation1" name="eq"/>
            <OMV name="c"/>
            <OMA>
              <OMS cd="arith1" name="times"/>
              <OMV name="a"/>
              <OMV name="b"/>
            </OMA>
          </OMA>
        </OMBIND>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="G"/>
      <OMA>
        <OMS cd="fns2" name="apply_to_list"/>
        <OMS cd="group1" name="group"/>
        <OMV name="listofgens"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="g"/>
        <OMV name="h"/>
        <OMV name="k"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="g"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="h"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="k"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMA>
              <OMS cd="arith1" name="times"/>
              <OMV name="g"/>
              <OMV name="h"/>
            </OMA>
            <OMV name="k"/>
          </OMA>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="g"/>
            <OMA>
              <OMS cd="arith1" name="times"/>
              <OMV name="h"/>
              <OMV name="k"/>
            </OMA>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="G"/>
      <OMA>
        <OMS cd="fns2" name="apply_to_list"/>
        <OMS cd="group1" name="group"/>
        <OMV name="listofgens"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="id"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="id"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMBIND>
          <OMS cd="quant1" name="forall"/>
          <OMBVAR>
            <OMV name="g"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="and"/>
            <OMA>
              <OMS cd="set1" name="in"/>
              <OMV name="g"/>
              <OMA>
                <OMS cd="group1" name="element_set"/>
                <OMV name="G"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMS cd="arith1" name="times"/>
                <OMV name="id"/>
                <OMV name="g"/>
              </OMA>
              <OMV name="g"/>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMS cd="arith1" name="times"/>
                <OMV name="g"/>
                <OMV name="id"/>
              </OMA>
              <OMV name="g"/>
            </OMA>
          </OMA>
        </OMBIND>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="relation1" name="eq"/>
      <OMV name="G"/>
      <OMA>
        <OMS cd="fns2" name="apply_to_list"/>
        <OMS cd="group1" name="group"/>
        <OMV name="listofgens"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="g"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="g"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMBIND>
          <OMS cd="quant1" name="exists"/>
          <OMBVAR>
            <OMV name="inv"/>
          </OMBVAR>
          <OMA>
            <OMS cd="logic1" name="and"/>
            <OMA>
              <OMS cd="set1" name="in"/>
              <OMV name="inv"/>
              <OMA>
                <OMS cd="group1" name="element_set"/>
                <OMV name="G"/>
              </OMA>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMS cd="arith1" name="times"/>
                <OMV name="g"/>
                <OMV name="inv"/>
              </OMA>
              <OMS cd="alg1" name="one"/>
            </OMA>
            <OMA>
              <OMS cd="relation1" name="eq"/>
              <OMA>
                <OMS cd="arith1" name="times"/>
                <OMV name="inv"/>
                <OMV name="g"/>
              </OMA>
              <OMS cd="alg1" name="one"/>
            </OMA>
          </OMA>
        </OMBIND>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>


<CDDefinition>
<Name> element_set </Name>
<Description>
The unary function which returns the set of elements of a group.
</Description>
</CDDefinition>


<CDDefinition>
<Name> is_subgroup </Name>
<Description>
The binary function whose value is true if the second argument is  a subgroup of the first.
</Description>

<CMP>
A is a subgroup of B implies element_set(A) is a subset of element_set(B)
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="group1" name="is_subgroup"/>
      <OMV name="B"/>
      <OMV name="A"/>
    </OMA>
    <OMA>
      <OMS cd="set1" name="subset"/>
      <OMA>
        <OMS cd="group1" name="element_set"/>
        <OMV name="A"/>
      </OMA>
      <OMA>
        <OMS cd="group1" name="element_set"/>
        <OMV name="B"/>
      </OMA>
    </OMA>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>

<CDDefinition>
<Name> right_transversal </Name>
<Description>
The binary function whose value is a set of representatives for the right cosets 
of the second argument as a subgroup of the first.
</Description>
</CDDefinition>

<CDDefinition>
<Name> normal_closure </Name>
<Description>
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.
</Description>

<CMP>
n in the normal closure (A,B) implies
there exists a in A and b in B s.t. n = b^(-1) a b
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="n"/>
      <OMA>
        <OMS cd="group1" name="normal_closure"/>
        <OMV name="A"/>
        <OMV name="B"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="a"/>
        <OMV name="b"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="a"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="A"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="b"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="B"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMV name="n"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="invb"/>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="invb"/>
            <OMV name="b"/>
          </OMA>
          <OMS cd="alg1" name="one"/>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>

<CDDefinition>
<Name> is_normal </Name>
<Description>
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.
</Description>

<CMP>
is_normal(G,H) implies that for all g in G and h in H then 
g^-1*h*g is in H
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="group1" name="is_normal"/>
      <OMV name="G"/>
      <OMV name="H"/>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="forall"/>
      <OMBVAR>
        <OMV name="g"/>
        <OMV name="h"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="g"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="h"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="H"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="invg"/>
            <OMV name="h"/>
            <OMV name="g"/>
          </OMA>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="H"/>
          </OMA>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="invg"/>
            <OMV name="g"/>
          </OMA>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>


<CDDefinition>
<Name> quotient_group </Name>
<Description>
The binary function whose value is the factor group of the first argument by the 
second, assuming the second is normal in the first.
</Description>
</CDDefinition>

<CDDefinition>
<Name> conjugacy_class </Name>
<Description>
The binary function whose value is the set of elements which 
are conjugate to the second argument in the first.
</Description>

<CMP>
The conjugacy class in G with respect to h = {g^(-1) h g | g in G}
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="relation1" name="eq"/>
    <OMA>
      <OMS cd="group1" name="conjugacy_class"/>
      <OMV name="G"/>
      <OMV name="h"/>
    </OMA>
    <OMA>
      <OMS cd="set1" name="suchthat"/>
      <OMA>
        <OMS cd="group1" name="element_set"/>
        <OMV name="G"/>
      </OMA>
      <OMBIND>
        <OMS cd="fns1" name="lambda"/>
        <OMBVAR>
          <OMV name="conj"/>
        </OMBVAR>
        <OMA>
          <OMS cd="logic1" name="and"/>
          <OMA>
            <OMS cd="relation1" name="eq"/>
            <OMV name="conj"/>
            <OMA>
              <OMS cd="arith1" name="times"/>
              <OMV name="invg"/>
              <OMV name="h"/>
              <OMV name="g"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMV name="invg"/>
              <OMV name="g"/>
            </OMA>
            <OMS cd="alg1" name="one"/>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="conj"/>
            <OMA>
              <OMS cd="group1" name="element_set"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="g"/>
            <OMA>
              <OMS cd="group1" name="element_set"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
      </OMBIND>
    </OMA>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>


<CDDefinition>
<Name> derived_subgroup </Name>
<Description>
The unary function whose value is the subgroup of argument
generated by all products of the form xyx^-1y^-1.
</Description>

<CMP>
d in the derived subgroup of G implies
there exist x,y in G such that d=x y x^(-1) y^(-1)
</CMP>

<FMP>
<OMOBJ>
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="set1" name="in"/>
      <OMV name="d"/>
      <OMA>
        <OMS cd="group1" name="element_set"/>
        <OMV name="G"/>
      </OMA>
    </OMA>
    <OMBIND>
      <OMS cd="quant1" name="exists"/>
      <OMBVAR>
        <OMV name="x"/>
        <OMV name="y"/>
      </OMBVAR>
      <OMA>
        <OMS cd="logic1" name="and"/>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="x"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="set1" name="in"/>
          <OMV name="y"/>
          <OMA>
            <OMS cd="group1" name="element_set"/>
            <OMV name="G"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMV name="d"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="x"/>
            <OMV name="y"/>
            <OMV name="invx"/>
            <OMV name="invy"/>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="invx"/>
            <OMV name="x"/>
          </OMA>
          <OMS cd="alg1" name="one"/>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
          <OMA>
            <OMS cd="arith1" name="times"/>
            <OMV name="invy"/>
            <OMV name="y"/>
          </OMA>
          <OMS cd="alg1" name="one"/>
        </OMA>
      </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>
</FMP>
</CDDefinition>



<CDDefinition>
<Name> sylow_subgroup </Name>
<Description>
The largest p-subgroup of the argument (up to conjugacy).
</Description>
</CDDefinition>


<CDDefinition>
<Name> character_table_of_group </Name>
<Description>
Refers to the character table of its argument 
which must be a group.

An actual character table is just a list of lists
as described below, annotated with 
the reference describing what it's a character table of:
e.g CharacterTable(G)
</Description>
</CDDefinition>


<CDDefinition>
<Name> character_table</Name>
<Description>
This is the constructor for a character table.
Usage:

CharacterTable(class_names, 
centralizer_sizes, centralizer_primes, centralizer_indices,
power_map, 
class_sizes, orders_class_reps, 
irreducibles_matrix, irreducible_values)

If G has n conjugacy classes then:
* classnames is a list of n strings which name the conjugacy classes
in line with the convention used in the Atlas of Finite Groups
The first class is always the class of the identity.

* centralizer_sizes[k] is the size of the centralizer
of the kth conjugacy class.

* centralizer_primes[k] is a list of primes of  the form
[p1, .., pk] i &lt; j implies that pi &lt; pj and 
the pi are precisely the primes which divide the 
centralizer_sizes[k].


* centralizer_indices is of the form 
[[i11, ...,i1k] ... [in1,...ink]]
so the centralizer of class 1 has order p1^i11 ... pk^i1k etc


* class_sizes - sizes of the conjugacy classes

* orders_class_reps - every element in a conjugacy class has the same order

* 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. These 
values may be expressions involving variables.

* irreducibles_values: a list of pairs of the form (var = val) where
val is an  irrational cyclotomic and var appears in expressions for 
values in the irreducibles_matrix.


</Description>
</CDDefinition>


</CD>

