Journal of Formalized Mathematics
Volume 8, 1996
University of Bialystok
Copyright (c) 1996 Association of Mizar Users

## Basic Properties of Functor Structures

Claus Zinn
University of Erlangen--N\"urnberg
Wolfgang Jaksch
University of Erlangen--N\"urnberg

### Summary.

This article presents some theorems about functor structures. We start with some basic lemmata concerning the composition of functor structures. Then, two theorems about the restriction operator are formulated. Later we show two theorems concerning the properties 'full' and 'faithful' of functor structures which are equivalent to the 'onto' and 'one-to-one' properties of their morphmaps, respectively. Furthermore, we prove some theorems about the inversion of functor structures.

#### MML Identifier: FUNCTOR1

The terminology and notation used in this paper have been introduced in the following articles [9] [6] [15] [16] [3] [5] [4] [2] [10] [11] [8] [7] [12] [13] [1] [14]

#### Contents (PDF format)

1. Definitions
2. Theorems about sets and functions
3. Theorems about the composition of functor structures
4. Theorems about the restriction and inclusion operator
5. Theorems about 'full' and 'faithful' functor structures
6. Theorems about the inversion of functor structures

#### Acknowledgments

This article has been written during the four week internship of the authors in Bia{\l}ystok in order to get familiar with the MIZAR system. We would like to thank Andrzej Trybulec and the members of the MIZAR group for their invitation and their instructive support.

#### Bibliography

[1] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.
[2] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.
[3] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[4] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[7] Malgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[8] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.
[9] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[10] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.
[11] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.
[12] Andrzej Trybulec. Categories without uniqueness of \rm cod and \rm dom. Journal of Formalized Mathematics, 7, 1995.
[13] Andrzej Trybulec. Examples of category structures. Journal of Formalized Mathematics, 8, 1996.
[14] Andrzej Trybulec. Functors for alternative categories. Journal of Formalized Mathematics, 8, 1996.
[15] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[16] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.