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.

MML Identifier: MONOID_0

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]

Contents (PDF format)

1. Binary operations preliminary
2. Semigroups
3. Monoids
4. Subsystems
5. The examples of monoids of numbers
6. The monoid of finite sequences over the set
7. 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