OpenMath Content Dictionary: ring1

Canonical URL:

http://www.openmath.org/cd/ring1.ocd

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):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
 <OMA><OMS cd="logic1" name="implies"/>
      <OMA><OMS cd="relation1" name="eq"/>
           <OMV name="S"/>
           <OMA><OMS cd="ring1" name="ring"/>
                <OMV name="R"/>
                <OMV name="add"/>
                <OMV name="zero"/>
                <OMV name="minus"/>
                <OMV name="mult"/>
                <OMV name="unit"/>
           </OMA>
           <OMBIND><OMS cd="quant1" name="forall"/>
                <OMBVAR><OMV name="x"/><OMV name="y"/><OMV name="z"/>
                </OMBVAR>
                <OMA><OMS cd="logic1" name="implies"/>
                     <OMA><OMS cd="logic1" name="and"/>
                          <OMA><OMS cd="set1" name="in"/>
                               <OMV name="x"/><OMV name="R"/>
                          </OMA>
                          <OMA><OMS cd="set1" name="in"/>
                               <OMV name="y"/><OMV name="R"/>
                          </OMA>
                          <OMA><OMS cd="set1" name="in"/>
                               <OMV name="z"/><OMV name="R"/>
                          </OMA>
                     </OMA>
                     <OMA><OMS cd="logic1" name="and"/>
                          <OMA><OMS cd="relation1" name="eq"/>
                               <OMA><OMV name="mult"/>
                                    <OMV name="x"/>
                                    <OMA><OMV name="add"/>
                                         <OMV name="y"/><OMV name="z"/>
                                    </OMA>
                               </OMA>
                               <OMA><OMV name="add"/>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="x"/> <OMV name="y"/>
                                    </OMA>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="x"/><OMV name="z"/>
                                    </OMA>
                               </OMA>
                          </OMA>
                          <OMA><OMS cd="relation1" name="eq"/>
                               <OMA><OMV name="mult"/>
                                    <OMA><OMV name="add"/>
                                         <OMV name="y"/><OMV name="z"/>
                                    </OMA>
                                    <OMV name="x"/>
                               </OMA>
                               <OMA><OMV name="add"/>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="y"/> <OMV name="x"/>
                                    </OMA>
                                    <OMA><OMV name="mult"/>
                                         <OMV name="z"/><OMV name="x"/>
                                    </OMA>
                               </OMA>
                          </OMA>
                     </OMA>
                </OMA>
            </OMBIND>
       </OMA>
  </OMA>
</OMOBJ>

implies (eq ( S, ring ( R, add, zero, minus, mult, unit) , forall [ x y z ] . (implies (and (in ( x, R) , in ( y, R) , in ( z, R) ) , and (eq ( mult ( x, add ( y, z) ) , add ( mult ( x, y) , mult ( x, z) ) ) , eq ( mult ( add ( y, z) , x) , add ( mult ( y, x) , mult ( z, x) ) ) ) ) ) ) )

$$S=\mathrm{ring}(R,\mathrm{add},\mathrm{zero},\mathrm{minus},\mathrm{mult},\mathrm{unit})=\forall \hspace{0.17em}x,y,z.x\in R\wedge y\in R\wedge z\in R\Rightarrow \mathrm{mult}(x,\mathrm{add}(y,z))=\mathrm{add}(\mathrm{mult}(x,y),\mathrm{mult}(x,z))\wedge \mathrm{mult}(\mathrm{add}(y,z),x)=\mathrm{add}(\mathrm{mult}(y,x),\mathrm{mult}(z,x))\Rightarrow$$

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="ring1" name="ring"/>
     <OMA><OMS cd="setname1" name="Z"/>
          <OMS cd="arith1" name="plus"/>
          <OMI>0</OMI>
          <OMS cd="arith1" name="minus"/>
          <OMS cd="arith1" name="times"/>
          <OMI>1</OMI>
     </OMA>
</OMA>
</OMOBJ>

ring (Z (plus, 0, minus, times, 1) )

$$\mathrm{ring}\left(\mathbb{Z}\right)$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="carrier"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="R"/>
  </OMA>
</OMOBJ>

eq (carrier (ring ( R, plus, zero, minus, times, one) ) , R)

$$\mathrm{carrier}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=R$$

Signatures:

sts

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

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="multiplication"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="times"/>
  </OMA>
</OMOBJ>

eq (multiplication (ring ( R, plus, zero, minus, times, one) ) , times)

$$\mathrm{multiplication}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{times}$$

Signatures:

sts

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

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="negation"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="minus"/>
  </OMA>
</OMOBJ>

eq (negation (ring ( R, plus, zero, minus, times, one) ) , minus)

$$\mathrm{negation}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{minus}$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="identity"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="one"/>
  </OMA>
</OMOBJ>

eq (identity (ring ( R, plus, zero, minus, times, one) ) , one)

$$\mathrm{identity}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{one}$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="zero"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="zero"/>
  </OMA>
</OMOBJ>

eq (zero (ring ( R, plus, zero, minus, times, one) ) , zero)

$$\mathrm{zero}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{zero}$$

Signatures:

sts

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

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="identity"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMV name="plus"/>
  </OMA>
</OMOBJ>

eq (identity (ring ( R, plus, zero, minus, times, one) ) , plus)

$$\mathrm{identity}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{plus}$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="ring1" name="subtraction"/>
            <OMA><OMS cd="ring1" name="ring"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
            </OMA>
       </OMA>
       <OMBIND><OMS cd="fns1" name="lambda"/>
            <OMBVAR><OMV name="x"/><OMV name="y"/>
            </OMBVAR>
            <OMA><OMV name="plus"/>
                 <OMV name="x"/>
                 <OMA><OMV name="minus"/>
                      <OMV name="y"/>
                 </OMA>
            </OMA>
       </OMBIND>
  </OMA>
</OMOBJ>

eq (subtraction (ring ( R, plus, zero, minus, times, one) ) , lambda [ x y ] . ( plus ( x, minus ( y) ) ) )

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

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA>
    <OMS cd="logic1" name="implies"/>
    <OMA>
      <OMS cd="ring1" name="is_commutative"/>
      <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="ring1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="ring1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMS cd="ring1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
          <OMA>
            <OMA>
              <OMS cd="ring1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
            <OMV name="b"/>
            <OMV name="a"/>
          </OMA>
        </OMA>
    </OMBIND>
  </OMA>
</OMOBJ>

implies (is_commutative ( G) , forall [ a b ] . (implies (and (in ( a, carrier ( G) ) , in ( b, carrier ( G) ) ) , eq (multiplication ( G) , a, b) , multiplication ( G) ( b, a) ) ) )

$$\mathrm{is\_commutative}\left(G\right)\Rightarrow \forall \hspace{0.17em}a,b.a\in \mathrm{carrier}\left(G\right)\wedge b\in \mathrm{carrier}\left(G\right)\Rightarrow \mathrm{multiplication}\left(G\right)=a=b$$

Signatures:

sts

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

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="relation1" name="eq"/>
          <OMA><OMS cd="ring1" name="additive_group"/>
               <OMA><OMS cd="ring1" name="ring"/>
                    <OMV name="R"/> 
                    <OMV name="plus"/>
                    <OMV name="zero"/>
                    <OMV name="minus"/>
                    <OMV name="times"/>
                    <OMV name="one"/>
               </OMA>
          </OMA>
          <OMA><OMS cd="group1" name="group"/>
               <OMV name="R"/> 
               <OMV name="plus"/>
               <OMV name="zero"/>
               <OMV name="minus"/>
          </OMA>
     </OMA>
    </OMOBJ>

eq (additive_group (ring ( R, plus, zero, minus, times, one) ) , group ( R, plus, zero, minus) )

$$\mathrm{additive\_group}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{group}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus})$$

Signatures:

sts

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="relation1" name="eq"/>
          <OMA><OMS cd="ring1" name="multiplicative_monoid"/>
               <OMA><OMS cd="ring1" name="ring"/>
                    <OMV name="R"/> 
                    <OMV name="plus"/>
                    <OMV name="zero"/>
                    <OMV name="minus"/>
                    <OMV name="times"/>
                    <OMV name="one"/>
               </OMA>
          </OMA>
          <OMA><OMS cd="group1" name="monoid"/>
               <OMV name="R"/> 
               <OMV name="times"/>
               <OMV name="one"/>
          </OMA>
     </OMA>
    </OMOBJ>

eq (multiplicative_monoid (ring ( R, plus, zero, minus, times, one) ) , monoid ( R, times, one) )

$$\mathrm{multiplicative\_monoid}\left(\mathrm{ring}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one})\right)=\mathrm{monoid}(R,\mathrm{times},\mathrm{one})$$

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
         <OMA><OMS cd="ring1" name="expression"/>
              <OMA><OMS cd="ring1" name="ring"/>
                   <OMS cd="setname1" name="Z"/>
                   <OMS cd="arith1" name="plus"/>
                   <OMI>0</OMI>
                   <OMS cd="arith1" name="unary_minus"/>
                   <OMS cd="arith1" name="times"/>
                   <OMI>1</OMI>
              </OMA>
              <OMA><OMS cd="arith1" name="times"/>
                   <OMI>6</OMI><OMI>3</OMI>
              </OMA>
         </OMA>
         <OMI>18</OMI>
    </OMA>
  </OMOBJ>

eq (expression (ring (Z, plus, 0, unary_minus, times, 1) , times (6, 3) ) , 18)

$$\mathrm{expression}(\mathrm{ring}(\mathbb{Z},+,0,-,\times ,1),6\times 3)=18$$

Signatures:

sts

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
     <OMA><OMS cd="ring1" name="subring"/>
          <OMV name="D"/> <OMV name="G"/>
     </OMA>
    </OMOBJ>

subring ( D, G)

$$\mathrm{subring}(D,G)$$

Example:

This example represents the subring of the multiplicative ring of the nonzero reals generated by the constants Pi and E:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="ring1" name="subring"/>
     <OMA>
       <OMS cd="list1" name="list"/>
         <OMS cd="nums1" name="pi"/>
         <OMS cd="nums1" name="e"/>
     </OMA>
     <OMA><OMS cd="ring1" name="ring"/>
          <OMS cd="setname1" name="R"/>
          <OMS cd="arith1" name="plus"/>
          <OMI>0</OMI>
          <OMS cd="arith1" name="unary_minus"/>
          <OMS cd="arith1" name="times"/>
          <OMI> 1 </OMI>
     </OMA>
</OMA>
</OMOBJ>

subring (list (pi, e) , ring (R, plus, 0, unary_minus, times, 1 ) )

$$\mathrm{subring}((\pi ,e),\mathrm{ring}(\mathbb{R},+,0,-,\times ,1))$$

Signatures:

sts

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:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
        <OMA><OMS cd="ring1" name="power"/>
            <OMI>3</OMI>
            <OMI>2</OMI>
            <OMA><OMS cd="ring1" name="ring"/>
                <OMS cd="setname1" name="Z"/>
                <OMS cd="arith1" name="plus"/>
                <OMI>0</OMI>
                <OMS cd="arith1" name="unary_minus"/>
                <OMS cd="arith1" name="times"/>
                <OMI>1</OMI>
            </OMA>
        </OMA>
        <OMI>6</OMI>
    </OMA>
  </OMOBJ>

eq (power (3, 2, ring (Z, plus, 0, unary_minus, times, 1) ) , 6)

$$\mathrm{power}(3,2,\mathrm{ring}(\mathbb{Z},+,0,-,\times ,1))=6$$

Signatures:

sts