# OpenMath Content Dictionary: field1

Canonical URL:
http://www.openmath.org/cd/field1.ocd
CD Base:
http://www.openmath.org/cd
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.
$\mathrm{field}\left(\mathbb{Q},+,0,-,×,1,\lambda x.\frac{1}{x}\right)$
Signatures:
sts

 [Next: carrier] [Last: expression] [Top]

## 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.
$\mathrm{carrier}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=R$
Signatures:
sts

 [Next: multiplication] [Previous: field] [Top]

## 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 *.
$\mathrm{multiplication}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\mathrm{times}$
Signatures:
sts

 [Next: minus] [Previous: carrier] [Top]

## 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 -.
$\mathrm{minus}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\mathrm{minus}$
Signatures:
sts

 [Next: inverse] [Previous: multiplication] [Top]

## 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.
$\mathrm{inverse}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\mathrm{inv}$
Signatures:
sts

 [Next: identity] [Previous: minus] [Top]

## 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.
$\mathrm{identity}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\mathrm{one}$
Signatures:
sts

 [Next: zero] [Previous: inverse] [Top]

## 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.
$\mathrm{zero}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\mathrm{zero}$
Signatures:
sts

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

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

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

## 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.
$\mathrm{subtraction}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\lambda x,y.\mathrm{plus}\left(x,\mathrm{minus}\left(y\right)\right)$
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 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):
$\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_subfield] [Previous: subtraction] [Top]

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

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

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

 [Next: multiplicative_group] [Previous: is_subfield] [Top]

## 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:
$\mathrm{multiplicative_group}\left(\mathrm{field}\left(R,\mathrm{plus},\mathrm{zero},\mathrm{minus},\mathrm{times},\mathrm{one},\mathrm{inv}\right)\right)=\mathrm{group}\left(R,\mathrm{times},\mathrm{one},\mathrm{inv}\right)$
Signatures:
sts

 [Next: subfield] [Previous: additive_group] [Top]

## 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:
$\mathrm{subfield}\left(D,G\right)$
Example:
This example represents the subfield of the multiplicative field of the nonzero reals generated by the constants Pi and E:
$\mathrm{subfield}\left(\left(\pi ,e\right),\mathrm{field}\left(\left\{x\in \mathbb{R}|x\ne 0\right\},×,\mathrm{inverse},1\right)\right)$
Signatures:
sts

 [Next: power] [Previous: multiplicative_group] [Top]

## 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:
$\mathrm{power}\left(3,2,\mathrm{field}\left(\mathbb{Q},+,0,-,×,1,\lambda x.\frac{1}{x}\right)\right)=9$
Signatures:
sts

 [Next: expression] [Previous: subfield] [Top]

## 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:
$\mathrm{expression}\left(\mathrm{field}\left(\mathbb{Z},+,0,-,×,1\right),6×3\right)=18$
Signatures:
sts

 [First: field] [Previous: power] [Top]