OpenMath Content Dictionary: magma1

Canonical URL:
http://www.openmath.org/cd/magma1.ocd
CD Base:
http://www.openmath.org/cd
CD File:
magma1.ocd
CD as XML Encoded OpenMath:
magma1.omcd
Defines:
is_identity, multiplication, carrier, is_associative, is_commutative, is_submagma, left_divides, left_expression, magma, right_divides, right_expression, submagma
Date:
2004-06-01
Version:
1 (Revision 2)
Review Date:
2006-06-01
Status:
experimental

Basic functions for magma theory

Initiated by Arjeh M. Cohen 2003-10-03
Edited by AMC 2004-0302

magma

Description:

This symbol is a constructor for magmas. It takes two arguments in the following order: a set to specify the elements in the magma and a binary operation to specify the magma operation. The binary operation should act on elements of the set and return an element of the set.

Commented Mathematical property (CMP):
A magma is closed under its operation.
Formal Mathematical property (FMP):
G = magma ( set , binop ) x set y set binop ( x , y ) set
Example:
This example represents the magma which has as elements all integers, and the magma operation is addition of the square of the first argument to the second.
magma ( Z , λ x , y . x 2 + y )
Signatures:
sts


[Next: carrier] [Last: right_expression] [Top]

carrier

Description:

This symbol represents a unary function, whose argument should be a magma G (for instance constructed by magma). When applied to G, its value should be the set of elements of a magma.

Example:
The carrier of magma(G,*) is G.
carrier ( magma ( G , times ) ) = G
Signatures:
sts


[Next: multiplication] [Previous: magma] [Top]

multiplication

Description:

This symbol represents a unary function, whose argument should be a magma G. It returns the multiplication map on G. We allow for the map to be n-ary.

Example:
The multiplication of magma(G,*) is *.
multiplication ( group ( G , times ) ) = times
Signatures:
sts


[Next: is_commutative] [Previous: carrier] [Top]

is_commutative

Description:

The unary boolean function whose value is true iff the argument is a commutative magma.

Commented Mathematical property (CMP):
If is_commutative(G) then for all a,b in carrier(G) a*b = b*a
Formal Mathematical property (FMP):
is_commutative ( G ) a , b . a carrier ( G ) b carrier ( G ) ( multiplication ( G ) ) ( a , b ) = ( multiplication ( G ) ) ( b , a )
Signatures:
sts


[Next: is_associative] [Previous: multiplication] [Top]

is_associative

Description:

The unary boolean function whose value is true iff the argument is an associative magma.

Commented Mathematical property (CMP):
If is_associative(G) then for all a,b in carrier(G) (a*b) * c = a*(b*c)
Formal Mathematical property (FMP):
is_associative ( G ) a , b , c . a carrier ( G ) b carrier ( G ) c carrier ( G ) ( multiplication ( G ) ) ( ( multiplication ( G ) ) ( a , b ) , c ) = ( multiplication ( G ) ) ( a , ( multiplication ( G ) ) ( b , c ) )
Signatures:
sts


[Next: is_submagma] [Previous: is_commutative] [Top]

is_submagma

Description:

The binary boolean function whose value is true iff the second argument is a submagma of the first.

Commented Mathematical property (CMP):
If is_submagma(G,H) then H is a set of elements of G and H is closed under multiplication.
Signatures:
sts


[Next: is_identity] [Previous: is_associative] [Top]

is_identity

Description:

This symbols represents a binary boolean function, whose arguments should be a magma and an element of the element set of the magma. When applied to the arguments M and x, it returns true if the element x is an identity of the magma M, that is, x*y = y* x = y for all elements y of M.

Signatures:
sts


[Next: submagma] [Previous: is_submagma] [Top]

submagma

Description:

This symbol is a constructor symbol with two arguments. The first argument is a magma M, the second a list or set, D, of elements of M. When applied to M and D, it denotes the submagma of M generated by D.

Example:
submagma ( M , D )
Example:
This example represents the submagma of the multiplicative magma of the nonzero reals generated by the constants Pi and E:
magma ( magma ( { x R | x 0 } , × ) , ( π , e ) )
Signatures:
sts


[Next: left_divides] [Previous: is_identity] [Top]

left_divides

Description:

This symbol is a ternary function. Its first argument should be a magma M and the second and third arguments should be elements of M. When applied to M, a, and b, it denotes the fact that a is a left_divisor of b in M. This means that there is v in M such that av=b.

Example:
left_divides ( M , a , b )
Signatures:
sts


[Next: right_divides] [Previous: submagma] [Top]

right_divides

Description:

This symbol is a ternary function. Its first argument should be a magma M and the second and third arguments should be elements of M. When applied to M, a, and b, it denotes the fact that a is a right_divisor of b in M. This means that there is v in M such that va = b.

Example:
right_divides ( M , a , b )
Signatures:
sts


[Next: left_expression] [Previous: left_divides] [Top]

left_expression

Description:

This symbol is a binary function. Its first argument should be a magma M, the second argument a list L of elements of M. When applied to M and L, it denotes the left product (L[1] * ( ... (L[n-1] * L[n]) ... )) of all elements in the list L.

Example:
left_expression ( magma ( Z , × ) , ( 3 , 2 ) ) = 6
Signatures:
sts


[Next: right_expression] [Previous: right_divides] [Top]

right_expression

Description:

This symbol is a binary function. Its first argument should be a magma M, the second argument a list L of elements of M When applied to M and L, it denotes the right product (( ... (L[1] * L[2]) * ... ) * L[n]) of all elements in the list L.

Example:
right_expression ( magma ( Z , × ) , ( 3 , 2 ) ) = 6
Signatures:
sts


[First: magma] [Previous: left_expression] [Top]