OpenMath Content Dictionary: ring1

Canonical URL:
http://www.openmath.org/cd/ring1.ocd
CD Base:
http://www.openmath.org/cd
CD File:
ring1.ocd
CD as XML Encoded OpenMath:
ring1.omcd
Defines:
addition, additive_group, carrier, expression, identity, is_commutative, is_subring, multiplication, multiplicative_monoid, negation, power, ring, subring, subtraction, zero
Date:
2004-06-01
Version:
1 (Revision 1)
Review Date:
2006-06-01
Status:
experimental

A CD of basic functions for ring theory

Written by Arjeh M. Cohen 2004-02-25

ring

Description:

This symbol is a constructor for rings. It takes six arguments R, a, o, i, m, e,: which are, respectively, a set R to specify the elements in the ring, a binary operation a on R, an element o of R, and a unary operation i on R such that [R,a,o,i] is a commutative group, a binary operation m on R and an element e of R such that [R,m,e] is a monoid.

Commented Mathematical property (CMP):
The distributive laws m(x,a(y,z)) = a(m(x,y),m(x,z)) and m(a(y,z),x) = a(m(y,x),m(z,x)), where x,y,z are elements of R, should hold.
Formal Mathematical property (FMP):
S = ring ( R , add , zero , minus , mult , unit ) = x , y , z . x R y R z R mult ( x , add ( y , z ) ) = add ( mult ( x , y ) , mult ( x , z ) ) mult ( add ( y , z ) , x ) = add ( mult ( y , x ) , mult ( z , x ) )
Example:
This example represents the ring which has as elements all rational integers. The ring addition is binary addition, the ring multiplication is binary multiplication.
ring ( Z )
Signatures:
sts


[Next: carrier] [Last: power] [Top]

carrier

Description:

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

Example:
The carrier of ring(R,+,0,-,*,1) is R.
carrier ( ring ( R , plus , zero , minus , times , one ) ) = R
Signatures:
sts


[Next: multiplication] [Previous: ring] [Top]

multiplication

Description:

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

Example:
The multiplication of ring(R,+,0,-,*,1) is *.
multiplication ( ring ( R , plus , zero , minus , times , one ) ) = times
Signatures:
sts


[Next: negation] [Previous: carrier] [Top]

negation

Description:

This symbol represents a unary function, whose argument should be a ring S. It returns the map sending an element of S to its additive inverse.

Example:
The minus of ring(R,+,0,-,*,1) is -.
negation ( ring ( R , plus , zero , minus , times , one ) ) = minus
Signatures:
sts


[Next: identity] [Previous: multiplication] [Top]

identity

Description:

This symbols represents a unary function, whose argument should be a ring. It returns the identity element of the ring.

Example:
The identity ring(R,+,0,-,*,1) is 1.
identity ( ring ( R , plus , zero , minus , times , one ) ) = one
Signatures:
sts


[Next: zero] [Previous: negation] [Top]

zero

Description:

This symbols represents a unary function, whose argument should be a ring. It returns the zero element of the ring.

Example:
The identity ring(R,+,0,-,*,1) is 0.
zero ( ring ( R , plus , zero , minus , times , one ) ) = zero
Signatures:
sts


[Next: addition] [Previous: identity] [Top]

addition

Description:

This symbols represents a unary function, whose argument should be a ring. It returns the addition on the ring. We will allow for the map to be n-ary.

Example:
The identity ring(R,+,0,-,*,1) is +.
identity ( ring ( R , plus , zero , minus , times , one ) ) = plus
Signatures:
sts


[Next: subtraction] [Previous: zero] [Top]

subtraction

Description:

This symbols represents a unary function, whose argument should be a ring. It returns the binary operation of subtraction on the ring.

Example:
The subtraction of ring(R,+,0,-,*,1) is the map sending the pair (r,s) of elements of R to r-s.
subtraction ( ring ( R , plus , zero , minus , times , one ) ) = λ x , y . plus ( x , minus ( y ) )
Signatures:
sts


[Next: is_commutative] [Previous: addition] [Top]

is_commutative

Description:

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

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
Signatures:
sts


[Next: is_subring] [Previous: subtraction] [Top]

is_subring

Description:

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

Commented Mathematical property (CMP):
If is_subring(G,H) then H is a nonempty set of elements of the carrier of G and H is closed under multiplication and taking inverses.
Signatures:
sts


[Next: additive_group] [Previous: is_commutative] [Top]

additive_group

Description:

This symbol is a unary function, whose argument should be a ring S. When applied to S its value is the monoid underlying S.

Example:
additive_group ( ring ( R , plus , zero , minus , times , one ) ) = group ( R , plus , zero , minus )
Signatures:
sts


[Next: multiplicative_monoid] [Previous: is_subring] [Top]

multiplicative_monoid

Description:

This symbol is a unary function, whose argument should be a ring S. When applied to S its value is the monoid underlying S.

Example:
multiplicative_monoid ( ring ( R , plus , zero , minus , times , one ) ) = monoid ( R , times , one )
Signatures:
sts


[Next: expression] [Previous: additive_group] [Top]

expression

Description:

This symbol is a function with two arguments. Its first argument should be a ring. The second should be an arithmetic expression A, whose operators are times, plus, minus, unary_minus, and power, and whose leaves are members of the carrier of G. (Here an integer m will be interpreted as a member of G by interpreting it as the sum of m copies of the identity element, the symbol alg1.one will be interpreted as the identity, and the symbol alg1.zero will be interpreted as the zero of G.) When applied to G and A, it denotes the element (of G) that is the element obtained from the leaves by applying the arithmetic operations of G instead of those from the CD arith1.

Example:
expression ( ring ( Z , + , 0 , - , × , 1 ) , 6 × 3 ) = 18
Signatures:
sts


[Next: subring] [Previous: multiplicative_monoid] [Top]

subring

Description:

This symbol is a constructor symbol with one or two arguments. The first argument is a list or set, D, of ring elements. The optional second argument is the ring G containing D. It denotes the subring of G generated by D.

Example:
subring ( D , G )
Example:
This example represents the subring of the multiplicative ring of the nonzero reals generated by the constants Pi and E:
subring ( ( π , e ) , ring ( R , + , 0 , - , × , 1 ) )
Signatures:
sts


[Next: power] [Previous: expression] [Top]

power

Description:

This is a symbol with two or three arguments. Its first argument should be a an element g of a ring and the second argument should be an integer. The optional third argument is the ring G containing g. It denotes the element g^k in G.

Example:
power ( 3 , 2 , ring ( Z , + , 0 , - , × , 1 ) ) = 6
Signatures:
sts


[First: ring] [Previous: subring] [Top]