OpenMath Content Dictionary: field1

Canonical URL:

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

CD File:

field1.ocd

CD as XML Encoded OpenMath:

field1.omcd

Defines:

addition, additive_group, carrier, expression, field, identity, inverse, is_commutative, is_subfield, minus, multiplication, multiplicative_group, power, subfield, subtraction, zero

Date:

2004-06-01

Version:

1 (Revision 2)

Review Date:

2006-06-01

Status:

experimental

A CD of basic functions for field theory

Written by Arjeh M. Cohen 2004-02-26

field

Description:

This symbol is a constructor for fields. It takes seven arguments R, a, o, n, m, e, i: which are, respectively, a set R to specify the elements in the field, a binary operation a on R, an element o of R, and a unary operation n on R such that [R,a,o,n] is a commutative group, a binary operation m on R, an element e of R, and a map from R - {o} to itself such that [R,m,e] is a monoid and such that [R - {o},m',e,i] is a group, where m' is the restriction of m to R -{o}.

Example:

This example represents the field of rational numbers. The field addition is binary addition, the field multiplication is binary multiplication.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
<OMA><OMS cd="field1" name="field"/>
     <OMS cd="setname1" name="Q"/>
     <OMS cd="arith1" name="plus"/>
     <OMI>0</OMI>
     <OMS cd="arith1" name="minus"/>
     <OMS cd="arith1" name="times"/>
     <OMI>1</OMI>
     <OMBIND><OMS cd="fns1" name="lambda"/>
         <OMBVAR>  <OMV name="x"/>  </OMBVAR>
         <OMA><OMS cd="arith1" name="divide"/>
              <OMI> 1 </OMI>  <OMV name="x"/>
         </OMA>
     </OMBIND>
</OMA>
</OMOBJ>

field (Q, plus, 0, minus, times, 1, lambda [ x ] . (divide ( 1 , x) ) )

$$\mathrm{field}(\mathbb{Q},+,0,-,\times ,1,\lambda \hspace{0.17em}x.\frac{1}{x})$$

Signatures:

sts

carrier

Description:

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

Example:

The carrier of field(R,+,0,-,*,1,inv) is R.

xml prefix mathml

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

eq (carrier (field ( R, plus, zero, minus, times, one, inv) ) , R)

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

Signatures:

sts

multiplication

Description:

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

Example:

The multiplication of field(R,+,0,-,*,1,inv) is *.

xml prefix mathml

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

eq (multiplication (field ( R, plus, zero, minus, times, one, inv) ) , times)

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

Signatures:

sts

minus

Description:

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

Example:

The minus of field(R,+,0,-,*,1,inv) is -.

xml prefix mathml

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

eq (minus (field ( R, plus, zero, minus, times, one, inv) ) , minus)

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

Signatures:

sts

inverse

Description:

This symbol represents a unary function, whose argument should be a field S. It returns the map sending a nonzero element of S to its multiplicative inverse.

Example:

The inverse of field(R,+,0,-,*,1,inv) is inv.

xml prefix mathml

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

eq (inverse (field ( R, plus, zero, minus, times, one, inv) ) , inv)

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

Signatures:

sts

identity

Description:

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

Example:

The identity field(R,+,0,-,*,1,inv) is 1.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="field1" name="identity"/>
            <OMA><OMS cd="field1" name="field"/>


                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
                 <OMV name="inv"/>
            </OMA>
       </OMA>
       <OMV name="one"/>
  </OMA>
</OMOBJ>

eq (identity (field ( R, plus, zero, minus, times, one, inv) ) , one)

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

Signatures:

sts

zero

Description:

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

Example:

The identity field(R,+,0,-,*,1,inv) is 0.

xml prefix mathml

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

eq (zero (field ( R, plus, zero, minus, times, one, inv) ) , zero)

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

Signatures:

sts

addition

Description:

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

Example:

The identity field(R,+,0,-,*,1,inv) is +.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
  <OMA><OMS cd="relation1" name="eq"/>
       <OMA><OMS cd="field1" name="identity"/>
            <OMA><OMS cd="field1" name="field"/>


                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
                 <OMV name="inv"/>
            </OMA>
       </OMA>
       <OMV name="plus"/>
  </OMA>
</OMOBJ>

eq (identity (field ( R, plus, zero, minus, times, one, inv) ) , plus)

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

Signatures:

sts

subtraction

Description:

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

Example:

The subtraction of field(R,+,0,-,*,1,inv) 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="field1" name="subtraction"/>
            <OMA><OMS cd="field1" name="field"/>
                 <OMV name="R"/>
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
                 <OMV name="inv"/>
            </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 (field ( R, plus, zero, minus, times, one, inv) ) , lambda [ x y ] . ( plus ( x, minus ( y) ) ) )

$$\mathrm{subtraction}\left(\mathrm{field}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv})\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 field.

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="field1" 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="field1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
          <OMA>
            <OMS cd="set1" name="in"/>
            <OMV name="b"/>
            <OMA>
              <OMS cd="field1" name="carrier"/>
              <OMV name="G"/>
            </OMA>
          </OMA>
        </OMA>
        <OMA>
          <OMS cd="relation1" name="eq"/>
            <OMA>
              <OMS cd="field1" name="multiplication"/>
              <OMV name="G"/>
            </OMA>
            <OMV name="a"/>
            <OMV name="b"/>
          </OMA>
          <OMA>
            <OMA>
              <OMS cd="field1" 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_subfield

Description:

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

Commented Mathematical property (CMP):

If is_subfield(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 field 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="field1" name="additive_group"/>
               <OMA><OMS cd="field1" name="field"/>
                    <OMV name="R"/> 
                 <OMV name="plus"/>
                 <OMV name="zero"/>
                 <OMV name="minus"/>
                 <OMV name="times"/>
                 <OMV name="one"/>
                 <OMV name="inv"/>
               </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 (field ( R, plus, zero, minus, times, one, inv) ) , group ( R, plus, zero, minus) )

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

Signatures:

sts

multiplicative_group

Description:

This symbol is a unary function, whose argument should be a field S. When applied to S its value is the multiplicative group on the nonzero elements of S.

Example:

xml prefix mathml

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

eq (multiplicative_group (field ( R, plus, zero, minus, times, one, inv) ) , group ( R, times, one, inv) )

$$\mathrm{multiplicative\_group}\left(\mathrm{field}(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv})\right)=\mathrm{group}(R,\mathrm{times},\mathrm{one},\mathrm{inv})$$

Signatures:

sts

subfield

Description:

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

Example:

xml prefix mathml

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

subfield ( D, G)

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

Example:

This example represents the subfield of the multiplicative field 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="field1" name="subfield"/>
     <OMA>
       <OMS cd="list1" name="list"/>
         <OMS cd="nums1" name="pi"/>
         <OMS cd="nums1" name="e"/>
     </OMA>
     <OMA><OMS cd="field1" name="field"/>
          <OMA><OMS cd="set1" name="suchthat"/>
               <OMS cd="setname1" name="R"/>
               <OMBIND><OMS cd="fns1" name="lambda"/>
                       <OMBVAR> <OMV name="x"/>
                       </OMBVAR>
                       <OMA><OMS cd="relation1" name="neq"/>
                            <OMV name="x"/>
                            <OMS cd="alg1" name="zero"/>
                       </OMA>
               </OMBIND>
          </OMA>
          <OMS cd="arith1" name="times"/>
          <OMS cd="arith2" name="inverse"/>
          <OMI> 1 </OMI>
     </OMA>
</OMA>
</OMOBJ>

subfield (list (pi, e) , field (suchthat (R, lambda [ x ] . (neq ( x, zero) ) ) , times, inverse, 1 ) )

$$\mathrm{subfield}((\pi ,e),\mathrm{field}(\left\{x\in \mathbb{R}\right|x\ne 0\},\times ,\mathrm{inverse},1))$$

Signatures:

sts

power

Description:

This is a symbol with two or three arguments. Its first argument should be an element g of a field and the second argument should be an integer. The optional third argument is the field 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="field1" name="power"/>
              <OMI>3</OMI>
              <OMI>2</OMI>
              <OMA><OMS cd="field1" name="field"/>
                   <OMS cd="setname1" name="Q"/>
                   <OMS cd="arith1" name="plus"/>
                   <OMI>0</OMI>
                   <OMS cd="arith1" name="minus"/>
                   <OMS cd="arith1" name="times"/>
                   <OMI>1</OMI>
                   <OMBIND><OMS cd="fns1" name="lambda"/>
                           <OMBVAR>  <OMV name="x"/>  </OMBVAR>
                           <OMA><OMS cd="arith1" name="divide"/>
                                <OMI> 1 </OMI>  <OMV name="x"/>
                           </OMA>
                   </OMBIND>
              </OMA>
         </OMA>
         <OMI>9</OMI>
    </OMA>
  </OMOBJ>

eq (power (3, 2, field (Q, plus, 0, minus, times, 1, lambda [ x ] . (divide ( 1 , x) ) ) ) , 9)

$$\mathrm{power}(3,2,\mathrm{field}(\mathbb{Q},+,0,-,\times ,1,\lambda \hspace{0.17em}x.\frac{1}{x}))=9$$

Signatures:

sts

expression

Description:

This symbol is a function with two arguments. Its first argument should be a field. 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. When applied to G and A, it denotes the element (of G) that is the element obtained from the leaves of A by applying the operations of G instead of those from the CD arith1 according to A. Here multiplication, addition, subtraction, minus, and power take over the roles of times, plus, minus, unary_minus, and power, respectively. Also, an integer m occurring in A 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.

Example:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
    <OMA><OMS cd="relation1" name="eq"/>
         <OMA><OMS cd="group1" name="expression"/>
              <OMA><OMS cd="field1" name="field"/>
                   <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 (field (Z, plus, 0, unary_minus, times, 1) , times (6, 3) ) , 18)

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

Signatures:

sts