Concrete Categories

Grzegorz Bancerek

University of Bialystok, Shinshu University, Nagano

Summary.

In the paper, we develop the notation of duality and equivalence of categories and concrete categories based on [22]. The development was motivated by the duality theory for continuous lattices (see [10, p. 189]), where we need to cope with concrete categories of lattices and maps preserving their properties. For example, the category {\it UPS} of complete lattices and directed suprema preserving maps; or the category {\it INF} of complete lattices and infima preserving maps. As the main result of this paper it is shown that every category is isomorphic to its concretization (the concrete category with the same objects). Some useful schemes to construct categories and functors are also presented.

MML Identifier: YELLOW18

Contents (PDF format)

1. Definability of Categories and Functors
2. Isomorphism and Equivalence of Categories
3. Dual Categories
4. Concrete Categories
5. Equivalence Between Concrete Categories
6. Concretization of Categories

Bibliography

[1] Grzegorz Bancerek. Curried and uncurried functions. Journal of Formalized Mathematics, 2, 1990.

[2] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.

[3] Grzegorz Bancerek and Agata Darmochwal. Comma category. Journal of Formalized Mathematics, 4, 1992.

[4] Czeslaw Bylinski. Basic functions and operations on functions. Journal of Formalized Mathematics, 1, 1989.

[5] Czeslaw Bylinski. Binary operations. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[9] Czeslaw Bylinski. Some basic properties of sets. Journal of Formalized Mathematics, 1, 1989.

[10] G. Gierz, K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D.S. Scott. \em A Compendium of Continuous Lattices. Springer-Verlag, Berlin, Heidelberg, New York, 1980.

[11] Artur Kornilowicz. The composition of functors and transformations in alternative categories. Journal of Formalized Mathematics, 10, 1998.

[12] Malgorzata Korolkiewicz. Homomorphisms of many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[13] Beata Madras. Product of family of universal algebras. Journal of Formalized Mathematics, 5, 1993.

[14] Beata Madras-Kobus. Basic properties of objects and morphisms. Journal of Formalized Mathematics, 9, 1997.

[15] Michal Muzalewski and Wojciech Skaba. Three-argument operations and four-argument operations. Journal of Formalized Mathematics, 2, 1990.

[16] Andrzej Nedzusiak. $\sigma$-fields and probability. Journal of Formalized Mathematics, 1, 1989.

[17] Robert Nieszczerzewski. Category of functors between alternative categories. Journal of Formalized Mathematics, 9, 1997.

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

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

[20] Andrzej Trybulec. Many-sorted sets. Journal of Formalized Mathematics, 5, 1993.

[21] Andrzej Trybulec. Many sorted algebras. Journal of Formalized Mathematics, 6, 1994.

[22] Andrzej Trybulec. Categories without uniqueness of \rm cod and \rm dom. Journal of Formalized Mathematics, 7, 1995.

[23] Andrzej Trybulec. Examples of category structures. Journal of Formalized Mathematics, 8, 1996.

[24] Andrzej Trybulec. Functors for alternative categories. Journal of Formalized Mathematics, 8, 1996.

[25] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

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

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

[28] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.