OpenMath

OpenMath is an extensible standard for representing the semantics of mathematical objects.

https://openmath.org

OpenMath Content Dictionary: gp1

Canonical URL:
http://www.openmath.org/cd/gp1.ocd
CD Base:
http://www.openmath.org/cd
CD File:
gp1.ocd
CD as XML Encoded OpenMath:
gp1.omcd
Defines:
character_table, character_table_of_group, conjugacy_class, declare_group, derived_subgroup, element_set, group, is_abelian, is_normal, is_subgroup, normal_closure, quotient_group, right_transversal, sylow_subgroup
Date:
2004-03-30
Version:
3 (Revision 1)
Review Date:
2017-12-31
Status:
experimental

     This document is distributed in the hope that it will be useful, 
     but WITHOUT ANY WARRANTY; without even the implied warranty of 
     MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

     The copyright holder grants you permission to redistribute this 
     document freely as a verbatim copy. Furthermore, the copyright
     holder permits you to develop any derived work from this document
     provided that the following conditions are met.
       a) The derived work acknowledges the fact that it is derived from
          this document, and maintains a prominent reference in the 
          work to the original source.
       b) The fact that the derived work is not the original OpenMath 
          document is stated prominently in the derived work.  Moreover if
          both this document and the derived work are Content Dictionaries
          then the derived work must include a different CDName element,
          chosen so that it cannot be confused with any works adopted by
          the OpenMath Society.  In particular, if there is a Content 
          Dictionary Group whose name is, for example, `math' containing
          Content Dictionaries named `math1', `math2' etc., then you should 
          not name a derived Content Dictionary `mathN' where N is an integer.
          However you are free to name it `private_mathN' or some such.  This
          is because the names `mathN' may be used by the OpenMath Society
          for future extensions.
       c) The derived work is distributed under terms that allow the
          compilation of derived works, but keep paragraphs a) and b)
          intact.  The simplest way to do this is to distribute the derived
          work under the OpenMath license, but this is not a requirement.
     If you have questions about this license please contact the OpenMath
     society at http://www.openmath.org.

  Author: OpenMath Consortium
  SourceURL: https://github.com/OpenMath/CDs

A CD of functions for group theory 

Written by A. Solomon on 1998-11-19
Modified by David Carlisle 1998-04-28
This is the old version of group1.
It is now deprecated in facour of the Cds in the riaca_algebra CD group.

declare_group

Role:
application
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.

Commented Mathematical property (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.
Formal Mathematical property (FMP):
G = declare_group ⁡ ( set , binop , unop , elt ) ⇒ ( x ∈ set ∧ y ∈ set ⇒ binop ⁡ ( x , y ) ∈ set ) ∧ binop ⁡ ( x , binop ⁡ ( y , z ) ) = binop ⁡ ( binop ⁡ ( x , y ) , z ) ∧ elt ∈ set ∧ ∀   x . x ∈ set ⇒ binop ⁡ ( elt , x ) = x ∧ binop ⁡ ( x , elt ) = x ∧ ∀   x . x ∈ set ⇒ binop ⁡ ( x , unop ⁡ ( x ) ) = elt
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.
declare_group ⁡ ( { x ∈ Z | x 2 ∈ Z } , + , - , 0 )
Signatures:
sts

[Next: is_abelian] [Last: character_table] [Top]

is_abelian

Role:
application
Description:

The unary boolean function whose value is true iff the argument is an abelian group

Commented Mathematical property (CMP):
If is_abelian(G) then for all a,b in element_set(G) a*b = b*a
Formal Mathematical property (FMP):
is_abelian ⁡ ( G ) ⇒ ∀   a , b . a ∈ element_set ⁡ ( G ) ∧ b ∈ element_set ⁡ ( G ) ⇒ a ⁢ b = b ⁢ a
Signatures:
sts

[Next: group] [Previous: declare_group] [Top]

group

Role:
application
Description:

The n-ary function Group. The group generated by its arguments. The arguments must have a natural group operation associated with them.

Signatures:
sts

[Next: element_set] [Previous: is_abelian] [Top]

element_set

Role:
application
Description:

The unary function which returns the set of elements of a group.

Signatures:
sts

[Next: is_subgroup] [Previous: group] [Top]

is_subgroup

Role:
application
Description:

The binary function whose value is true if the second argument is a subgroup of the first.

Commented Mathematical property (CMP):
A is a subgroup of B implies element_set(A) is a subset of element_set(B)
Formal Mathematical property (FMP):
is_subgroup ⁡ ( B , A ) ⇒ element_set ⁡ ( A ) ⊂ element_set ⁡ ( B )
Signatures:
sts

[Next: right_transversal] [Previous: element_set] [Top]

right_transversal

Role:
application
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.

Signatures:
sts

[Next: normal_closure] [Previous: is_subgroup] [Top]

normal_closure

Role:
application
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.

Commented Mathematical property (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
Formal Mathematical property (FMP):
n ∈ normal_closure ⁡ ( A , B ) ⇒ ∃   a , b . a ∈ element_set ⁡ ( A ) ∧ b ∈ element_set ⁡ ( B ) ∧ n = invb ⁢ a ⁢ b ∧ invb ⁢ b = 1
Signatures:
sts

[Next: is_normal] [Previous: right_transversal] [Top]

is_normal

Role:
application
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.

Commented Mathematical property (CMP):
is_normal(G,H) implies that for all g in G and h in H then g^-1*h*g is in H
Formal Mathematical property (FMP):
is_normal ⁡ ( G , H ) ⇒ ∀   g , h . g ∈ element_set ⁡ ( G ) ∧ h ∈ element_set ⁡ ( H ) ∧ invg ⁢ h ⁢ g ∈ element_set ⁡ ( H )
Signatures:
sts

[Next: quotient_group] [Previous: normal_closure] [Top]

quotient_group

Role:
application
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.

Signatures:
sts

[Next: conjugacy_class] [Previous: is_normal] [Top]

conjugacy_class

Role:
application
Description:

The binary function whose value is the set of elements which are conjugate to the second argument in the first.

Commented Mathematical property (CMP):
The conjugacy class in G with respect to h = {g^(-1) h g | g in G}
Formal Mathematical property (FMP):
conjugacy_class ⁡ ( G , h ) = { conj ∈ element_set ⁡ ( G ) | conj = invg ⁢ h ⁢ g ∧ invg ⁡ ( g ) = 1 ∧ conj ∈ element_set ⁡ ( G ) ∧ g ∈ element_set ⁡ ( G ) }
Signatures:
sts

[Next: derived_subgroup] [Previous: quotient_group] [Top]

derived_subgroup

Role:
application
Description:

The unary function whose value is the subgroup of argument generated by all products of the form xyx^-1y^-1.

Commented Mathematical property (CMP):
d in the derived subgroup of G implies there exist x,y in G such that d=x y x^(-1) y^(-1)
Formal Mathematical property (FMP):
d ∈ element_set ⁡ ( G ) ⇒ ∃   x , y . x ∈ element_set ⁡ ( G ) ∧ y ∈ element_set ⁡ ( G ) ∧ d = x ⁢ y ⁢ invx ⁢ invy ∧ invx ⁢ x = 1 ∧ invy ⁢ y = 1
Signatures:
sts

[Next: sylow_subgroup] [Previous: conjugacy_class] [Top]

sylow_subgroup

Role:
application
Description:

The largest p-subgroup of the argument (up to conjugacy).

Signatures:
sts

[Next: character_table_of_group] [Previous: derived_subgroup] [Top]

character_table_of_group

Role:
application
Description:

Refers to the character table of its argument which must be a group.

Signatures:
sts

[Next: character_table] [Previous: sylow_subgroup] [Top]

character_table

Role:
application
Description:

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.

Signatures:
sts

[First: declare_group] [Previous: character_table_of_group] [Top]