# 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=\mathrm{ring}\left(R,\mathrm{add},\mathrm{zero},\mathrm{minus},\mathrm{mult},\mathrm{unit}\right)=\forall x,y,z.x\in R\wedge y\in R\wedge z\in R⇒\mathrm{mult}\left(x,\mathrm{add}\left(y,z\right)\right)=\mathrm{add}\left(\mathrm{mult}\left(x,y\right),\mathrm{mult}\left(x,z\right)\right)\wedge \mathrm{mult}\left(\mathrm{add}\left(y,z\right),x\right)=\mathrm{add}\left(\mathrm{mult}\left(y,x\right),\mathrm{mult}\left(z,x\right)\right)⇒$
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.
$\mathrm{ring}\left(\mathbb{Z}\right)$
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.
$\mathrm{carrier}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=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 *.
$\mathrm{multiplication}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{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 -.
$\mathrm{negation}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{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.
$\mathrm{identity}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{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.
$\mathrm{zero}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{zero}$
Signatures:
sts

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 +.
$\mathrm{identity}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{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.
$\mathrm{subtraction}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\lambda x,y.\mathrm{plus}\left(x,\mathrm{minus}\left(y\right)\right)$
Signatures:
sts

## 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):
$\mathrm{is_commutative}\left(G\right)⇒\forall a,b.a\in \mathrm{carrier}\left(G\right)\wedge b\in \mathrm{carrier}\left(G\right)⇒\mathrm{multiplication}\left(G\right)=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

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:
$\mathrm{additive_group}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{group}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus}\right)$
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:
$\mathrm{multiplicative_monoid}\left(\mathrm{ring}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one}\right)\right)=\mathrm{monoid}\left(R,\mathrm{times},\mathrm{one}\right)$
Signatures:
sts

## 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:
$\mathrm{expression}\left(\mathrm{ring}\left(\mathbb{Z},+,0,-,×,1\right),6×3\right)=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:
$\mathrm{subring}\left(D,G\right)$
Example:
This example represents the subring of the multiplicative ring of the nonzero reals generated by the constants Pi and E:
$\mathrm{subring}\left(\left(\pi ,e\right),\mathrm{ring}\left(\mathbb{R},+,0,-,×,1\right)\right)$
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:
$\mathrm{power}\left(3,2,\mathrm{ring}\left(\mathbb{Z},+,0,-,×,1\right)\right)=6$
Signatures:
sts

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