field1 http://www.openmath.org/cd http://www.openmath.org/cd/field1.ocd 2006-06-01 2004-06-01 1 2 experimental A CD of basic functions for field theory Written by Arjeh M. Cohen 2004-02-26 field 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}. This example represents the field of rational numbers. The field addition is binary addition, the field multiplication is binary multiplication. 0 1 1 carrier 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. The carrier of field(R,+,0,-,*,1,inv) is R. multiplication 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. The multiplication of field(R,+,0,-,*,1,inv) is *. minus 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. The minus of field(R,+,0,-,*,1,inv) is -. inverse 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. The inverse of field(R,+,0,-,*,1,inv) is inv. identity This symbols represents a unary function, whose argument should be a field. It returns the identity element of the field. The identity field(R,+,0,-,*,1,inv) is 1. zero This symbols represents a unary function, whose argument should be a field. It returns the zero element of the field. The identity field(R,+,0,-,*,1,inv) is 0. addition 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. The identity field(R,+,0,-,*,1,inv) is +. subtraction This symbols represents a unary function, whose argument should be a field. It returns the binary operation of subtraction on the field. The subtraction of field(R,+,0,-,*,1,inv) is the map sending the pair (r,s) of elements of R to r-s. is_commutative The unary boolean function whose value is true iff the argument is a commutative field. If is_commutative(G) then for all a,b in carrier(G) a*b = b*a is_subfield The binary boolean function whose value is true iff the second argument is a subfield of the second. 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. additive_group This symbol is a unary function, whose argument should be a field S. When applied to S its value is the monoid underlying S. multiplicative_group 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. subfield 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. This example represents the subfield of the multiplicative field of the nonzero reals generated by the constants Pi and E: 1 power 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. 3 2 0 1 1 9 expression 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. 0 1 63 18