ring1 http://www.openmath.org/cd http://www.openmath.org/cd/ring1.ocd 2006-06-01 2004-06-01 1 1 experimental A CD of basic functions for ring theory Written by Arjeh M. Cohen 2004-02-25 ring 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. 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. This example represents the ring which has as elements all rational integers. The ring addition is binary addition, the ring multiplication is binary multiplication. 0 1 carrier 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. The carrier of ring(R,+,0,-,*,1) is R. multiplication 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. The multiplication of ring(R,+,0,-,*,1) is *. negation 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. The minus of ring(R,+,0,-,*,1) is -. identity This symbols represents a unary function, whose argument should be a ring. It returns the identity element of the ring. The identity ring(R,+,0,-,*,1) is 1. zero This symbols represents a unary function, whose argument should be a ring. It returns the zero element of the ring. The identity ring(R,+,0,-,*,1) is 0. addition 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. The identity ring(R,+,0,-,*,1) is +. subtraction This symbols represents a unary function, whose argument should be a ring. It returns the binary operation of subtraction on the ring. The subtraction of ring(R,+,0,-,*,1) 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 ring. If is_commutative(G) then for all a,b in carrier(G) a*b = b*a is_subring The binary boolean function whose value is true iff the second argument is a subring of the second. 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. additive_group This symbol is a unary function, whose argument should be a ring S. When applied to S its value is the monoid underlying S. multiplicative_monoid This symbol is a unary function, whose argument should be a ring S. When applied to S its value is the monoid underlying S. expression 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. 0 1 63 18 subring 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. This example represents the subring of the multiplicative ring of the nonzero reals generated by the constants Pi and E: 0 1 power 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. 3 2 0 1 6