algebraic_cats http://www.openmath.org/cd/algebraic_cats.ocd 2005-04-01 experimental 2002-06-17 0 0 generic_alg_cats logic1 meta_cats quant1 relation1 set1 A CD of basic algebraic category constructors. This CD holds constructors of individual instances of the categories, with defining properties of the categories and accessor symbols to allow access to attributes of the categories. monoid This is the constructor for monoids. A monoid comprises a set and an operation over elements of the set. The set must contain a unique identity element (relative to the operation). That is an element, I, such that I*a=a*I=a where a represents an arbitrary element of S and * represents the operation. The operation * must be associative over S. The monoid constructor takes three arguments, the set of the monoid, a binary function taking two elements of the set into itself to represent the operation of the monoid and an element of the set to represent the identity of the monoid. This constructor may be used to build monoids if (S,*,1) comprises a monoid then for all a,b,c in S | a*(b*c)=(a*b)*c the operation of the monoid is closed over the set of the monoid if (S,*,1) is a monoid then there exists a unique identity element in S the set of a monoid must contain at least one element monoid_set This symbol takes one argument which should be a monoid, it returns the set of the monoid. The set of the monoid (S,*,1) = S monoid_operation This symbol takes one argument which should be a monoid, it returns the operation of the monoid. The operation of the monoid (S,*,1) = * monoid_identity This symbol takes one argument which should be a monoid, it returns the identity of the monoid. The identity of the monoid (S,*,1) = 1 Abelian_monoid This is the constructor for Abelian monoids. An Abelian monoid is a monoid, such that the operation is commutative between members of the Abelian monoid. The Abelian_monoid constructor takes three arguments, the set of the Abelian monoid, a binary function taking two elements of the set into itself to represent the operation of the Abelian monoid and an element of the set to represent the identity of the Abelian monoid. This constructor may be used to build Abelian_monoids if (S,*,1) comprises an Abelian monoid then for all a,b in S | a*b=b*a Abelian_monoid_set This symbol takes one argument which should be an Abelian monoid, it returns the set of the Abelian monoid. The set of the Abelian monoid (S,*,1) = S Abelian_monoid_operation This symbol takes one argument which should be an Abelian monoid, it returns the operation of the Abelian monoid. The operation of the Abelian monoid (S,*,1)= * Abelian_monoid_identity This symbol takes one argument which should be an Abelian monoid, it returns the identity of the Abelian monoid. The identity of the Abelian monoid (S,*,1) = 1 ordered_monoid This is the constructor for ordered monoids, that is monoids on which there is an ordering relation. The ordered_monoid constructor takes four arguments, the set of the ordered monoid, a binary function taking two elements of the set into itself to represent the operation of the ordered monoid, an element of the set to represent the identity of the ordered monoid and a binary function taking two elements of the set into the booleans to represent the ordering on the ordered monoid. This constructor may be used to build ordered monoids if (S,*,1,\leq) represents an ordered monoid, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b ordered_monoid_set This symbol takes one argument which should be an ordered monoid. It returns a set which should be the set of the ordered monoid. The set of the ordered monoid (S,*,1,\leq) = S ordered_monoid_operation This symbol takes one argument which should be an ordered monoid. It returns a binary function between elements of the set of the ordered monoid, which should represent the operation of the ordered monoid. The operation of the ordered monoid (S,*,1,\leq) = * ordered_monoid_identity This symbol takes one argument which should be an ordered monoid. It returns an element of the set of the ordered monoid, which should be the identity of the ordered monoid. The identity of the ordered monoid (S,*,1,\leq) = 1 ordered_monoid_order This symbol takes one argument which should be an ordered monoid. It returns a binary function between elements of the set of the ordered monoid, which should represent the ordering relation on the ordered monoid. The order of the ordered monoid (S,*,1,\leq) = \leq ordered_Abelian_monoid This symbol is the constructor for ordered Abelian monoids, that is Abelian monoids on which there is an ordering relation. The ordered_Abelian_monoid constructor takes four arguments, the set of the ordered Abelian monoid, a binary function taking two elements of the set into itself to represent the operation of the ordered Abelian monoid, an element of the set to represent the identity of the ordered Abelian monoid and a binary function taking two elements of the set into the booleans to represent the ordering of the ordered Abelian monoid. This constructor may be used to build ordered Abelian monoids if (S,*,1,\leq) represents an ordered Abelian monoid, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b ordered_Abelian_monoid_set This symbol takes one argument which should be an ordered Abelian monoid. It returns a set which should be the set of the ordered Abelian monoid. The set of the ordered Abelian monoid (S,*,1,/leq) = S ordered_Abelian_monoid_operation This symbol takes one argument which should be an ordered Abelian monoid. It returns a binary function between elements of the set of the ordered Abelian monoid, which should represent the operation of the ordered Abelian monoid. The operation of the ordered Abelian monoid (S,*,1,/leq) = * ordered_Abelian_monoid_identity This symbol takes one argument which should be an ordered Abelian monoid. It returns an element of the set of the ordered Abelian monoid, which should be the identity of the ordered Abelian monoid. The identity of the ordered Abelian monoid (S,*,1,/leq) = 1 ordered_Abelian_monoid_order This symbol takes one argument which should be an ordered Abelian monoid. It returns a binary function between elements of the set of the ordered Abelian monoid, which should represent the ordering relation on the ordered Abelian monoid. The ordering of the ordered Abelian monoid (S,*,1,/leq) = /leq groupoid This symbol is the constructor for groupoids, that is an algebraic structure on a set, with a binary operation. The operator of the groupoid must be closed over the set of the groupoid. The groupoid constructor takes two arguments, the set of the groupoid and a binary function which represents the operation of the groupoid. This constructor may be used to build groupoids if (S,*) comprises a groupoid, then for all a,b in S | a*b is a member of S groupoid_set This symbol takes one argument which should be a groupoid. It returns the set of the groupoid. The set of the groupoid (S,*) = S groupoid_operation This symbol takes one argument which should be a groupoid. It returns a binary function which should represent the operation of the groupoid. The operation of the groupoid (S,*) = * semigroup This symbol is the constructor for semigroups, that is groupoids for which the operator of the semigroup is associative over the set of the semigroup. The semigroup constructor takes two arguments, the set of the semigroup and a binary function which represents the operation of the semigroup. This constructor may be used to build semigroups if (S,*) comprises a semigroup then for all a,b,c in S | a*(b*c)=(a*b)*c semigroup_set This symbol takes one argument which should be a semigroup. It returns the set of the semigroup. The set of the semigroup (S,*) = S semigroup_operation This symbol takes one argument which should be a semigroup. It returns a binary function which should represent the operation of the semigroup. The operation of the semigroup (S,*) = * Abelian_semigroup This symbol is the constructor for an Abelian semigroup, that is a semigroup which has an operator which is commutative over the set of the semigroup. The Abelian semigroup constructor takes two arguments, the set of the Abelian semigroup and a binary function which represents the operation of the Abelian semigroup. This constructor may be used to build Abelian semigroups If (S,*) comprises an Abelian semigroup, then for all a,b in S|a*b=b*a Abelian_semigroup_set This symbol takes one argument which should be an Abelian semigroup. It returns a set, which should be the set of the Abelian semigroup. The set of the Abelian semigroup (S,*) = S Abelian_semigroup_operation This symbol takes one argument which should be an Abelian semigroup. It returns a binary function, which should represent the operation of the Abelian semigroup. The operation of the Abelian semigroup (S,*) = * This symbol is an alternative model for the symbol declare_group in the CD group1 group This symbol is the constructor for groups, that is a monoid for which every element is invertible. The group constructor takes four arguments, the set of the group, a binary function taking two elements of the set into itself to represent the operation of the group, an element of the set to represent the identity of the group and a unary function taking the set into itself to specify inverse elements of the group. This symbol may be used to build groups if (S,*,1,inv:S->S) comprises a group then for all a in S | inv(a) is a member of S and inv(a)*a=a*inv(a)=1 group_set This symbol takes one argument which should be a group. It returns a set, which should be the set of the group. The set of the group (S,*,1,inv) = S group_operation This symbol takes one argument which should be a group. It returns a binary function, which represents the operation of the group. The operation of the group (S,*,1,inv) = * group_identity This symbol takes one argument which should be a group. It returns the identity of the group. The identity of the group (S,*,1,inv) = 1 group_inverse This symbol takes one argument which should be a group. It returns a unary function, which is the inverse mapping for the group. The inverse of the group (S,*,1,inv) = inv ordered_group This symbol is the constructor for ordered groups, that is a group on which there is an ordering relation. The ordered_group constructor takes five arguments, the set of the ordered group, a binary function taking two elements of the set into itself to represent the operation of the ordered group, an element of the set to represent the identity of the ordered group, a unary function taking the set into itself to specify inverse elements of the ordered group and a binary function taking two elements of the set into the booleans to specify the ordering of the ordered group. This constructor may be used to build ordered groups if (S,*,1,inv:S->S,\leq) represents an ordered group, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b ordered_group_set This symbol takes one argument which should be an ordered group. It returns the set of the ordered group. The set of the ordered group (S,*,1,inv,leq) = S ordered_group_operation This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the operation of the ordered group. The operation of the ordered group (S,*,1,inv,leq) = * ordered_group_identity This symbol takes one argument which should be an ordered group. It returns the identity of the ordered group. The identity of the ordered group (S,*,1,inv,leq) = 1 ordered_group_inverse This symbol takes one argument which should be an ordered group. It returns a unary function, which is the inverse function of the ordered group. The inverse of the ordered group (S,*,1,inv,leq) = inv ordered_group_order This symbol takes one argument which should be an ordered group. It returns a binary function, which represents the ordering of the ordered group. The order of the ordered group (S,*,1,inv,leq) = leq Abelian_group This symbol is the constructor for Abelian groups, that is a group such that the operation is commutative between members of the group. The Abelian_group constructor takes four arguments, the set of the Abelian group, a binary function taking two elements of the set into itself to represent the operation of the Abelian group, an element of the set to represent the identity of the Abelian group and a unary function taking the set into itself to specify inverse elements. This constructor builds Abelian groups if (S,*,1,inv) comprises an Abelian group then for all a,b in S | a*b = b*a Abelian_group_set This symbol takes one argument which should be an Abelian group. It returns the set of the Abelian group. The set of the Abelian group (S,*,1,inv) = S Abelian_group_operation This symbol takes one argument which should be an Abelian group. It returns a binary function, which represents the operation of the Abelian group. The operation of the Abelian group (S,*,1,inv) = * Abelian_group_identity This symbol takes one argument which should be an Abelian group. It returns the identity of the Abelian group. The identity of the Abelian group (S,*,1,inv) = 1 Abelian_group_inverse This symbol takes one argument which should be an Abelian group. It reurns a unary function, which should be the inverse function for the Abelian group. The inverse of the Abelian group (S,*,1,inv) = inv ordered_Abelian_group This symbol is the constructor for ordered Abelian groups, that is an Abelian group on which there is an ordering relation. The ordered_Abelian_group constructor takes five arguments, the set of the ordered Abelian group, a binary function taking two elements of the set into itself to represent the operation of the ordered Abelian group, an element of the set to represent the identity of the ordered Abelian group, a unary function taking the set into itself to specify inverse elements and a binary function taking two elements of the set into the booleans to specify the ordering of the ordered Abelian group. This constructor builds ordered Abelian groups if (S,*,1,inv:S->S,\leq) represents an ordered Abelian group, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b ordered_Abelian_group_set This symbol takes one argument which should be an ordered Abelian group. It returns the set of the ordered Abelian group. The set of the ordered Abelian group (S,*,1,inv,leq) = S ordered_Abelian_group_operation This symbol takes one argument which should be an ordered Abelian group. It returns a binary function, which represents the operation of the ordered Abelian group. The operation of the ordered Abelian group (S,*,1,inv,leq) = * ordered_Abelian_group_identity This symbol takes one argument which should be an ordered Abelian group. It returns the identity of the ordered Abelian group. The identity of the ordered Abelian group (S,*,1,inv,leq) = 1 ordered_Abelian_group_inverse This symbol takes one argument which should be an ordered Abelian group. It returns a unary function, which is the inverse function of the ordered Abelian group. The inverse of the ordered Abelian group (S,*,1,inv,leq) = inv ordered_Abelian_group_order This symbol takes one argument which should be an ordered Abelian group. It returns a binary function, which should represent the ordering of the ordered Abelian group. The order of the ordered Abelian group (S,*,1,inv,leq) = leq ringoid This symbol is the constructor for ringoids. A ringoid is a set together with two operations + and *. * is left and right distributive over +. The ringoid constructor takes three arguments, the set of the ringoid, a binary function from the set into itself to represent the * operation and a binary function from the set into itself to represent the + operation. The ringoid constructor builds ringoids if (a,*,+) comprises a ringoid then for all a,b,c in S | a*(b+c) = a*b+a*c (b+c)*a = b*a+c*a ringoid_set This symbol takes one argument which should be a ringoid. It returns a set which represents the set of the ringoid. The set of the ringoid (S,*,+) = S ringoid_times This symbol takes one argument which should be a ringoid. It returns a binary function which represents the multiplicative operation (*) of the ringoid. The mulitplication operation of the ringoid (S,*,+) = S ringoid_plus This symbol takes one argument which should be a ringoid. It returns a binary function which represents the additive operation (+) of the ringoid. The addition operation of the ringoid (S,*,+) = + ring This symbol is the constructor for rings. A ring is a set together with two operations + and *. A ring is an Abelian group under + and a semigroup under *. A ring has a further rule which associates the two operation, that is left and right distributivity. The ring constructor takes five arguments, the set of the ring, a binary function from the set into itself to represent the * operation, a binary function from the set into itself to represent the + operation, an element of the set of the ring to represent the additive identity 0 and a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives). This constructor builds rings A ring is a ringoid if (S,*,+,0,neg:S->S) comprises a ring then * is both left and right distributive over +. That is: For all a,b,c in S, a*(b+c)=(a*b)+(a*c) and (b+c)*a=(b*a)+(c*a) ring_set This symbol takes one argument which should be a ring. It returns the set of the ring. The set of the ring (S,*,+,0,neg) = S ring_times This symbol takes one argument which should be a ring. It returns a binary function which represents the multiplicative operation of the ring. The times of the ring (S,*,+,0,neg) = * ring_plus This symbol takes one argument which should be a ring. It returns a binary function which represents the additive operation of the ring. The plus of the ring (S,*,+,0,neg) = + ring_zero This symbol takes one argument which should be a ring. It returns the additive identity of the ring. The zero of the ring (S,*,+,0,neg) = 0 ring_negative This symbol takes one argument which should be a ring. It returns a unary function which should be the negative function of the ring. The negative function of the ring (S,*,+,0,neg) = neg ordered_ring This symbol is the constructor for ordered rings, that is a ring on which there is an ordering relation. The ordered_ring constructor takes six arguments, the set of the ordered ring, a binary function from the set into itself to represent the multiplicative operation (*), a binary function from the set into itself to represent the additive operation (+), an element of the set of the ordered ring to represent the additive identity 0, a unary function from the set into itself to represent additive inverses (i.e. inverses under +, or negatives) and a binary function from the set into the booleans to represent the ordering relation. This constructor builds ordered rings if (S,*,+,0,neg:S->S,\leq) constitutes an ordered ring, then for all a,b in S | a \leq b or b \leq a and for all a,b,c in S | if a\leq b and b\leq c then a\leq c and for all a,b in S | if a\leq b and b\leq a then a=b ordered_ring_set This symbol takes one argument which should be an ordered ring. It returns the set of the ordered ring. The set of the ordered ring (S,*,+,0,-,leq) = * ordered_ring_times This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the multiplicative operation of the ordered ring. The times of the ordered ring (S,*,+,0,-,leq) = * ordered_ring_plus This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the additive operation of the ordered ring. The + of the ordered ring (S,*,+,0,-,leq) = + ordered_ring_zero This symbol takes one argument which should be an ordered ring. It returns the zero of the ordered ring. The zero of the ordered ring (S,*,+,0,-,leq) = 0 ordered_ring_negative This symbol takes one argument which should be an ordered ring. It returns a unary function to represent the additive inverse function of the ordered ring. The negative of the ordered ring (S,*,+,0,-,leq) = - ordered_ring_order This symbol takes one argument which should be an ordered ring. It returns a binary function, which represents the order function on the ordered ring. The order of the ordered ring (S,*,+,0,-,leq) = leq non_commutative_ring This symbol is the constructor for non commutative rings, these are rings over which the * operator is not commutative. the non_commutative_ring constructor takes five arguments: The set of the non-commutative ring. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the non-commutative ring to specify the additive identity, 0. And a unary function taking the set of the non-commutative ring into itself to represent the additive inverses of the non-commutative ring (i.e. inverses under +, or negatives). This constructor builds non-commutative rings if (S,*,+,0,neg:S->S) constitutes a non-commutative ring, then there exist a,b in S such that a*b~=b*a non_commutative_ring_set This symbol takes one argument which should be a non-commutative ring. It returns the set of the non-commutative ring. The set of the non-commutative ring (S,*,+,0,-) = S non_commutative_ring_times This symbol takes one argument which should be a non-commutative ring. It returns a binary function, which represents the multiplicative function of the non-commutative ring. The times of the non-commutative ring (S,*,+,0,-) = * non_commutative_ring_plus This symbol takes one argument which should be a non-commutative ring. It returns a binary function, which represents the additive function of the non-commutative ring. The plus of the non-commutative ring (S,*,+,0,-) = + non_commutative_ring_zero This symbol takes one argument which should be a non-commutative ring. It returns the zero of the non-commutative ring. The zero of the non-commutative ring (S,*,+,0,-) = 0 non_commutative_ring_negative This symbol takes one argument which should be a non-commutative ring. It returns a unary function, which represents the multiplicative inverse of the non-commutative ring. The negative of the non-commutative ring (S,*,+,0,-) = - Euclidean_domain This symbol is the constructor for Euclidean domains. A Euclidean domain is a ring on which there is no zero divisors together with an integer norm function. The Euclidean_domain constructor takes six arguments: The set of the Euclidean domain. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the Euclidean domain to specify the additive identity, 0. A unary function taking the set of the Euclidean domain into itself to represent the additive inverses (i.e. inverses under +, or negatives). And a unary function taking elements of the set into the positive integers, to represent the integer norm function. This constructor builds Euclidean domains if (S,*,+,0,neg:S->S,abs:S->Z^+) constitutes a Euclidean domain then for every a,b ~= 0 in S then abs(a*b) >= abs(a) and abs(a*b) >= abs(b) and for every a,b ~= 0 in S then there exists q and r in S such that a=q*b + r and abs(r) < abs(B) or r=0 Euclidean_domain_set This symbol takes one argument which should be a Euclidean domain. It returns the set of the Euclidean domain. The set of the Euclidean domain (S,*,+,0,-,abs) = S Euclidean_domain_times This symbol takes one argument which should be a Euclidean domain. It returns a binary function, which represents the multiplicative operation of the Euclidean domain. The times of the Euclidean domain (S,*,+,0,-,abs) = * Euclidean_domain_plus This symbol takes one argument which should be a Euclidean domain. It returns a binary function, which represents the additive operation of the Euclidean domain. The plus of the Euclidean domain (S,*,+,0,-,abs) = + Euclidean_domain_zero This symbol takes one argument which should be a Euclidean domain. It returns the additive identity of the Euclidean domain. The zero of the Euclidean domain (S,*,+,0,-,abs) = 0 Euclidean_domain_negative This symbol takes one argument which should be a Euclidean domain. It returns a unary function, which represents additive inverses of the Euclidean domain. The negative of the Euclidean domain (S,*,+,0,-,abs) = - Euclidean_domain_abs This symbol takes one argument which should be a Euclidean domain. It returns a unary function, which is the absolute value function of the Euclidean domain. The absolute value function of the Euclidean domain (S,*,+,0,-,abs) = abs field This symbol is the constructor for fields. A field is an Abelian group under +, the set of the field complement {0} with * is an Abelian group, a field has a further rule which associates the two operations, that is left and right distributivity. The field constructor takes seven arguments: The set of the field. A binary function into itself to represent the multiplication operation, *. A binary function into itself to represent the addition operation, +. A member of the set of the field to specify the multiplicative identity, 1. A member of the set of the field to specify the additive identity, 0. A unary function taking the set of the field into itself to represent the multiplicative inverses (i.e. inverses under *). A unary function taking the set of the field into itself to represent the additive inverses (i.e. inverses under +, or negatives). This constructor builds fields