Basic Properties of Functor Structures

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)

Definitions
Theorems about sets and functions
Theorems about the composition of functor structures
Theorems about the restriction and inclusion operator
Theorems about 'full' and 'faithful' functor structures
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.