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

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.