Natural transformations. Discrete categories

Andrzej Trybulec

Warsaw University, Bialystok

Summary.

We present well known concepts of category theory: natural transformations and functor categories, and prove propositions related to. Because of the formalization it proved to be convenient to introduce some auxiliary notions, for instance: transformations. We mean by a transformation of a functor $F$ to a functor $G$, both covariant functors from $A$ to $B$, a function mapping the objects of $A$ to the morphisms of $B$ and assigning to an object $a$ of $A$ an element of $\mathop{\rm Hom}(F(a),G(a))$. The material included roughly corresponds to that presented on pages 18,129-130,137-138 of the monography ([9]). We also introduce discrete categories and prove some propositions to illustrate the concepts introduced.

MML Identifier: NATTRA_1

Contents (PDF format)

1. Preliminaries
2. Application of a functor to a morphism
3. Transformations
4. Natural transformations
5. Functor category
6. Discrete categories

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. 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. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.

[7] Czeslaw Bylinski. Subcategories and products of categories. Journal of Formalized Mathematics, 2, 1990.

[8] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[9] Zbigniew Semadeni and Antoni Wiweger. \em Wst\c ep do teorii kategorii i funktorow, volume 45 of \em Biblioteka Matematyczna. PWN, Warszawa, 1978.

[10] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[11] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[12] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[13] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.