Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
Monoids
-
Grzegorz Bancerek
-
Polish Academy of Sciences, Institute of Mathematics, Warsaw
Summary.
-
The goal of the article is to define the concept of monoid.
In the preliminary section we introduce the notion of some properties
of binary operations. The second section is concerning with structures
with a set and a binary operation on this set: there is introduced
the notion corresponding to the notion of some properties of binary
operations and there are shown some useful clusters. Next, we are
concerning with the structure with a set, a binary operation on the set
and with an element of the set. Such a structure is called monoid
iff the operation is associative and the element is a unity of the operation.
In the fourth section the concept of subsystems of monoid (group)
is introduced. Subsystems are submonoids (subgroups) or other parts of monoid
(group) with are closed w.r.t. the operation. There are presented facts on
inheritness of some properties by subsystems. Finally, there are
constructed the examples of groups and monoids:
the group $\rangle{\Bbb R},+\langle$ of real numbers with addition,
the group ${\Bbb Z}^+$ of integers as the subsystem of
the group $\rangle{\Bbb R},+\langle$,
the semigroup $\rangle{\Bbb N},+\langle$ of natural numbers as the
subsystem of ${\Bbb Z}^+$, and
the monoid $\rangle{\Bbb N},+,0\langle$ of natural numbers with addition
and zero as monoidal extension of the semigroup $\rangle{\Bbb N},+\langle$.
The semigroups of real and natural numbers with multiplication are also
introduced. The monoid of finite sequences over some set with concatenation
as binary operation and with empty sequence as neutral element is
defined in sixth section. Last section deals with monoids with the composition
of functions as the operation, i.e. with the monoid of partial and
total functions and the monoid of permutations.
The terminology and notation used in this paper have been
introduced in the following articles
[16]
[7]
[21]
[18]
[10]
[17]
[1]
[22]
[8]
[4]
[2]
[23]
[6]
[5]
[3]
[9]
[19]
[11]
[12]
[15]
[14]
[20]
[13]
-
Binary operations preliminary
-
Semigroups
-
Monoids
-
Subsystems
-
The examples of monoids of numbers
-
The monoid of finite sequences over the set
-
Monoids of mappings
Bibliography
- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
- [2]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
- [3]
Czeslaw Bylinski.
Binary operations.
Journal of Formalized Mathematics,
1, 1989.
- [4]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [5]
Czeslaw Bylinski.
Functions from a set to a set.
Journal of Formalized Mathematics,
1, 1989.
- [6]
Czeslaw Bylinski.
Partial functions.
Journal of Formalized Mathematics,
1, 1989.
- [7]
Czeslaw Bylinski.
Some basic properties of sets.
Journal of Formalized Mathematics,
1, 1989.
- [8]
Czeslaw Bylinski.
Binary operations applied to finite sequences.
Journal of Formalized Mathematics,
2, 1990.
- [9]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a non-empty sets.
Journal of Formalized Mathematics,
2, 1990.
- [10]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
- [11]
Eugeniusz Kusak, Wojciech Leonczuk, and Michal Muzalewski.
Abelian groups, fields and vector spaces.
Journal of Formalized Mathematics,
1, 1989.
- [12]
Michal Muzalewski.
Construction of rings and left-, right-, and bi-modules over a ring.
Journal of Formalized Mathematics,
2, 1990.
- [13]
Dariusz Surowik.
Cyclic groups and some of their properties --- part I.
Journal of Formalized Mathematics,
3, 1991.
- [14]
Andrzej Trybulec.
Binary operations applied to functions.
Journal of Formalized Mathematics,
1, 1989.
- [15]
Andrzej Trybulec.
Semilattice operations on finite subsets.
Journal of Formalized Mathematics,
1, 1989.
- [16]
Andrzej Trybulec.
Tarski Grothendieck set theory.
Journal of Formalized Mathematics,
Axiomatics, 1989.
- [17]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
Journal of Formalized Mathematics,
1, 1989.
- [18]
Andrzej Trybulec.
Subsets of real numbers.
Journal of Formalized Mathematics,
Addenda, 2003.
- [19]
Michal J. Trybulec.
Integers.
Journal of Formalized Mathematics,
2, 1990.
- [20]
Wojciech A. Trybulec.
Groups.
Journal of Formalized Mathematics,
2, 1990.
- [21]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
- [22]
Edmund Woronowicz.
Relations and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
- [23]
Edmund Woronowicz.
Relations defined on sets.
Journal of Formalized Mathematics,
1, 1989.
Received December 29, 1992
[
Download a postscript version,
MML identifier index,
Mizar home page]