ring2
http://www.openmath.org/cd/ring2.ocd
2006-06-01
2004-06-01
1
1
experimental
Basic functions for homomorphisms in ring theory
Initiated by Arjeh M. Cohen 2004-02-25
is_homomorphism
This symbol is a boolean function with three arguments.
The first and arguments are rings M, N,
the third is a map f from the element set of M to the element set of N.
When applied to M, N, and f, it denotes that f is a ring homomorphism from M
to N.
If is_homomorphism(M,N,f) then, for each pair of elements x, y of M, we have
f(x * y) = f(x) * f(y).
is_isomorphism
This symbol is a boolean function with three arguments.
The first and arguments are rings M, N,
the third is a map f from the element set of M to the element set of N.
When applied to M, N, and f, it denotes that f is a ring isomorphism from M
to N.
This means that f is a homomorphism from M to N,
that f is bijective, and that its inverse is a homomorphism from N to M.
is_endomorphism
This symbol is a boolean function with two arguments.
The first argument is a ring M,
the second is a map f from the element set of M to the element set of M.
When applied to M and f, it denotes that f is a ring endomorphism from M
to M.
If is_endomorphism(M,f) then is_homomorphism(M,M,f)
is_automorphism
This symbol is a boolean function with two arguments.
The first is a ring M,
the second is a map f from the element set of M to the element set of M.
When applied to M and f, it denotes a ring automorphism f of M.
If is_automorphism(M,f) then is_isomorphism(M,M,f)
left_multiplication
This symbol is a function with two arguments, which should be a ring M
and an element x of M.
When applied to M and x, it denotes left multiplication on M by x.
left_multiplication(M,x) (y) = x * y.
right_multiplication
This symbol is a function with two arguments, which should be a ring M
and an element x of M.
When applied to M and x, it denotes right multiplication on M by x.
right_multiplication(M,x) (y) = y * x.
isomorphic
This symbol is a Boolean function with n arguments, n at least 2, which are rings.
When applied to M_1, ..., M_n, it denotes the fact that there is an
isomorphism from each M_i to each M_j.