Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

Isomorphisms of Categories


Andrzej Trybulec
Warsaw University, Bialystok

Summary.

We continue the development of the category theory basically following [8] (compare also [7]). We define the concept of isomorphic categories and prove basic facts related, e.g. that the Cartesian product of categories is associative up to the isomorphism. We introduce the composition of a functor and a transformation, and of transformation and a functor, and afterwards we define again those concepts for natural transformations. Let us observe, that we have to duplicate those concepts because of the permissiveness: if a functor $F$ is not naturally transformable to $G$, then natural transformation from $F$ to $G$ has no fixed meaning, hence we cannot claim that the composition of it with a functor as a transformation results in a natural transformation. We define also the so called horizontal composition of transformations ([8], p.~140, exercise {\bf 4}.{\bf 2},{\bf 5}(C)) and prove {\em interchange law} ([7], p.44). We conclude with the definition of equivalent categories.

MML Identifier: ISOCAT_1

The terminology and notation used in this paper have been introduced in the following articles [9] [5] [11] [2] [3] [1] [4] [6] [10]

Contents (PDF format)

Bibliography

[1] Czeslaw Bylinski. Basic functions and operations on functions. 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. Introduction to categories and functors. Journal of Formalized Mathematics, 1, 1989.
[5] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Subcategories and products of categories. Journal of Formalized Mathematics, 2, 1990.
[7] Saunders Mac Lane. \em Categories for the Working Mathematician, volume 5 of \em Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin, 1971.
[8] Zbigniew Semadeni and Antoni Wiweger. \em Wst\c ep do teorii kategorii i funktorow, volume 45 of \em Biblioteka Matematyczna. PWN, Warszawa, 1978.
[9] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[10] Andrzej Trybulec. Natural transformations. Discrete categories. Journal of Formalized Mathematics, 3, 1991.
[11] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.

Received November 22, 1991


[ Download a postscript version, MML identifier index, Mizar home page]