OpenMath

OpenMath is an extensible standard for representing the semantics of mathematical objects.

https://openmath.org

OpenMath Content Dictionary: order1

Canonical URL:
http://www.win.tue.nl/SCIEnce/cds/order1.ocd
CD File:
order1.ocd
CD as XML Encoded OpenMath:
order1.omcd
Defines:
algebraic_integer, algebraic_number, is_Dedekind, is_maximal_order, is_nonzero_divisor, is_principal_ideal_domain, maximal_order, number_field, order, primitive_element, ring_integers
Date:
2009-07-02
Version:
1 (Revision 7)
Review Date:
2017-09-30
Status:
experimental

This CD defines the basic functions and constructors for orders of number fields. Written by S. Lesseni (lesseni@math.tu-berlin.de). 

	A CD of basic functions for orders of number fields written for SCIEnce project. Note that all the rings used here will be considered unital.
	The reference textbooks are: 
	(1) M. Pohst and H. Zassenhaus, Algorithmic Algebraic Number Theory, Cambridge
	Univ. Press, 1989.
	(2) H. Cohen, A course in Computational Algebraic Number Theory. Berlin, Springer-Verlag (1993).

is_Dedekind

Role:
application
Description:

This symbol represents a unary boolean function. The argument should be a ring R. When evaluated on R, the function returns true if R is a Dedekind ring and false otherwise. Note that a ring R is a Dedekind ring if it is Noetherian, integrally closed (so integral) and such that every non-zero prime ideal is maximal.

Commented Mathematical property (CMP):
if R is a Dedekind ring and a subring of the rational field Q then R = Z.
Formal Mathematical property (FMP):
is_Dedekind ⁡ ( R ) ∧ is_subring ⁡ ( Q , R ) ⇒ R = Z
Example:
if the ring (R,+,0,-,*,1) is a principal ideal domain then (R,+,0,-,*,1) is a Dedekind ring.
∀   R , plus , zero , minus , times , one . is_principal_ideal_domain ⁡ ( ring ⁡ ( R , plus , zero , minus , times , one ) ) ⇒ is_Dedekind ⁡ ( ring ⁡ ( R , plus , zero , minus , times , one ) )
Signatures:
sts

[Next: is_nonzero_divisor] [Last: primitive_element] [Top]

is_nonzero_divisor

Role:
application
Description:

This symbol represents a boolean binary function. The first argument is a ring R, the second is an element b of R. When evaluated on R and b, the function returns true if b is a nonzero divisor in R.

Commented Mathematical property (CMP):
if x is a non-zero divisor in the ring R then x is in R and x is different from zero and for all non-zero y in R, x*y is different from zero or y*x is different from zero.
Formal Mathematical property (FMP):
is_nonzero_divisor ⁡ ( R , x ) ⇒ x ∈ carrier ⁡ ( R ) ∧ x ≠ zero ⁡ ( R ) ∧ ∀   y . y ∈ carrier ⁡ ( R ) ∧ y ≠ zero ⁡ ( R ) ⇒ ( ( multiplication ⁡ ( R ) ) ⁡ ( x , y ) ≠ zero ⁡ ( R ) ) ∨ ( ( multiplication ⁡ ( R ) ) ⁡ ( y , x ) ≠ zero ⁡ ( R ) )
Example:
is_nonzero_divisor ⁡ ( Z , 5 )
Signatures:
sts

[Next: is_principal_ideal_domain] [Previous: is_Dedekind] [Top]

is_principal_ideal_domain

Role:
application
Description:

The unary boolean function whose value is true if and only if the argument is a principal ideal domain. R is a principal ideal domain if R is a commutative ring without zero divisors and if every ideal of R is a principal ideal.

Commented Mathematical property (CMP):
is_principal_ideal_domain(R) then for all a, b in R a*b=b*a and a different from zero in R then a is a non-zero divisor in R and I an ideal of R then there exists x in R such that I is the principal ideal generated by x in R.
Formal Mathematical property (FMP):
is_principal_ideal_domain ⁡ ( R ) ⇒ ∀   a , b . a ∈ carrier ⁡ ( R ) ∧ b ∈ carrier ⁡ ( R ) ⇒ ( multiplication ⁡ ( R ) ) ⁡ ( a , b ) = ( multiplication ⁡ ( R ) ) ⁡ ( b , a ) ∧ ( a ∈ carrier ⁡ ( R ) ⇒ is_nonzero_divisor ⁡ ( R , a ) ) ∧ ( is_ideal ⁡ ( carrier ⁡ ( R ) , I ) ⇒ ∃   x . x ∈ carrier ⁡ ( R ) ⇒ I = principal_ideal ⁡ ( R , x ) )
Example:
is_principal_ideal_domain ⁡ ( Z )
Signatures:
sts

[Next: order] [Previous: is_nonzero_divisor] [Top]

order

Role:
application
Description:

This is a binary function, whose first argument is a Dedekind ring R and the second is a polynomial f. When applied to R and f, it returns an order of f over the polynomial ring R: it is a ring A containing R, which is finitely generated R-module with no nilpotent non-zero ideal and as a R-module it is torsion-free. Note that the result is not unique. Also this function allows to compute an order of a polynomial over another polynomial ring. The idea behind this computation is to coerce f into the polynomial ring of R and then compute the order.

Example:
order ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 3 , 0 ) ) ) )
Signatures:
sts

[Next: maximal_order] [Previous: is_principal_ideal_domain] [Top]

maximal_order

Role:
application
Description:

This is a binary function, whose first argument is a Dedekind ring R and the second is a polynomial f. When applied to R and f, it returns the maximal order A among the orders of f (over the polynomial ring of R) in the quotient field of A. Note that the result is unique.

Example:
maximal_order ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 3 , 0 ) ) ) )
Signatures:
sts

[Next: is_maximal_order] [Previous: order] [Top]

is_maximal_order

Role:
application
Description:

The unary boolean function whose value is true if and only if the argument is a maximal order.

Example:
is_maximal_order ⁡ ( maximal_order ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 3 , 0 ) ) ) ) )
Signatures:
sts

[Next: algebraic_integer] [Previous: maximal_order] [Top]

algebraic_integer

Role:
application
Description:

This is a binary function. The first argument is an order O. The second argument should be a list L of elements of the Dedekind ring R, such that O is an order over the polynomial ring of R (cf. order). The length of L should be equal to the degree n of the polynomial generating the order O. When applied to O and L, it represents the element L[0] + L[1] b + L[2] b^2 + ... + L[n-1] b^(n-1) of O, where b stands for a primitive element of O.

Example:
algebraic_integer ⁡ ( order ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 3 , 0 ) ) ) ) , ( 7 , 2 ) )
Signatures:
sts

[Next: number_field] [Previous: is_maximal_order] [Top]

number_field

Role:
application
Description:

This symbol is a constructor for number fields. It takes two arguments in the following order: a ring R and a monic irreducible univariate polynomial f. If the ring R is Z (or Q), it returns the absolute number field. Otherwise it returns the relative number field over the number field whose ring of integers is R. This symbol is intended to be used in upcoming CDs for e.g. describing discriminants of number fields, or Galois groups, unit groups, class groups, regulators, etc.; all useful number theoretical notions.

Example:
number_field ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 2 , 1 ) , term ⁡ ( 0 , 1 ) ) ) )
Example:
number_field ⁡ ( ring_integers ⁡ ( number_field ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 2 , 0 ) ) ) ) ) , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 3 , 0 ) ) ) )
Signatures:
sts

[Next: algebraic_number] [Previous: algebraic_integer] [Top]

algebraic_number

Role:
application
Description:

This is a binary function. The first argument is a number field F. The second argument should be a list L of elements of Q in case of an absolute number field F. Otherwise the second argument is a list L of elements of the number field whose ring of integers is the ring R over which F is defined (cf. number_field). The length of the list L should be equal to the degree n of F. When applied to F and L, it represents the element L[0] + L[1] b + L[2] b^2 + ... + L[n-1] ^(b-1) of F, where b stands for a primitive element of F.

Example:
algebraic_number ⁡ ( order ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 1 , 0 ) ) ) , ( 123 , 0 ) ) )
Signatures:
sts

[Next: ring_integers] [Previous: number_field] [Top]

ring_integers

Role:
application
Description:

This is a unary function, whose argument is a number field K. When applied to K, it returns the ring of integers of K. It is the Dedekind ring of K.

Commented Mathematical property (CMP):
if A is the ring of integers of the number field K then A is a subring of K and A is a Dedekind ring.
Formal Mathematical property (FMP):
A = ring_integers ⁡ ( K ) ⇒ is_subring ⁡ ( K , A ) ∧ is_Dedekind ⁡ ( A )
Example:
ring_integers ⁡ ( number_field ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 2 , 0 ) ) ) ) )
Signatures:
sts

[Next: primitive_element] [Previous: algebraic_number] [Top]

primitive_element

Role:
application
Description:

This is a unary function, whose argument is a number field K. It returns a primitive element of K. Note that the result is not unique.

Example:
primitive_element ⁡ ( number_field ⁡ ( Z , DMP ⁡ ( poly_ring_d ⁡ ( Z , 1 ) , SDMP ⁡ ( term ⁡ ( 1 , 2 ) , term ⁡ ( 2 , 0 ) ) ) ) )
Signatures:
sts

[First: is_Dedekind] [Previous: ring_integers] [Top]