Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
Opposite Rings, Modules and Their Morphisms
-
Michal Muzalewski
-
Warsaw University, Bialystok
Summary.
-
Let $\Bbb K = \langle S; K, 0, 1, +, \cdot \rangle$ be a ring.
The structure ${}^{\rm op}\Bbb K = \langle S; K, 0, 1, +, \bullet \rangle$
is called anti-ring, if $\alpha \bullet \beta = \beta \cdot \alpha$
for elements $\alpha$, $\beta$ of $K$
[8, pages 5-7].
It is easily seen that ${}^{\rm op}\Bbb K$ is also a ring. If $V$ is a
left module over $\Bbb K$, then $V$ is a right module over ${}^{\rm op}\Bbb K$.
If $W$ is a right module over $\Bbb K$, then $W$ is a left module over
${}^{\rm op}\Bbb K$.
Let $K, L$ be rings. A morphism $J: K \longrightarrow L$
is called anti-homomorphism,
if $J(\alpha\cdot\beta) = J(\beta)\cdot J(\alpha)$
for elements $\alpha$, $\beta$ of $K$. If $J:K \longrightarrow L$ is a
homomorphism, then $J:K \longrightarrow {}^{\rm op}L$ is an anti-homomorphism.
Let $K, L$ be rings, $V, W$ left modules over $K, L$ respectively and
$J:K \longrightarrow L$ an anti-monomorphism. A map
$f:V \longrightarrow W$ is called
$J$ - semilinear, if $f(x+y) = f(x)+f(y)$ and
$f(\alpha\cdot x) = J(\alpha)\cdot f(x)$
for vectors $x, y$ of $V$ and a scalar $\alpha$ of $K$.
MML Identifier:
MOD_4
The terminology and notation used in this paper have been
introduced in the following articles
[4]
[12]
[13]
[2]
[3]
[1]
[11]
[6]
[7]
[9]
[5]
[10]
-
Opposite functions
-
Opposite rings
-
Opposite modules
-
Morphisms of rings
-
Opposite morphisms to morphisms of rings
-
Morphisms of groups
-
Semilinear morphisms
Bibliography
- [1]
Czeslaw Bylinski.
Binary operations.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [3]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
- [4]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Czeslaw Bylinski.
The modification of a function by a function and the iteration of the composition of a function.
Journal of Formalized Mathematics,
2, 1990.
- [6]
Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.
Abelian groups, fields and vector spaces.
Journal of Formalized Mathematics,
1, 1989.
- [7]
Michal Muzalewski.
Construction of rings and left-, right-, and bi-modules over a ring.
Journal of Formalized Mathematics,
2, 1990.
- [8]
Michal Muzalewski.
\em Foundations of Metric-Affine Geometry.
Dzial Wydawnictw Filii UW w Bialymstoku, Filia UW w
Bialymstoku, 1990.
- [9]
Michal Muzalewski.
Categories of groups.
Journal of Formalized Mathematics,
3, 1991.
- [10]
Michal Muzalewski.
Category of rings.
Journal of Formalized Mathematics,
3, 1991.
- [11]
Wojciech A. Trybulec.
Vectors in real linear space.
Journal of Formalized Mathematics,
1, 1989.
- [12]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [13]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
Received June 22, 1992
[
Download a postscript version,
MML identifier index,
Mizar home page]