Exponential Objects

Marco Riccardi

Formalized Mathematics (2015)

  • Volume: 23, Issue: 4, page 351-369
  • ISSN: 1426-2630

Abstract

top
In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].

How to cite

top

Marco Riccardi. "Exponential Objects." Formalized Mathematics 23.4 (2015): 351-369. <http://eudml.org/doc/276848>.

@article{MarcoRiccardi2015,
abstract = {In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].},
author = {Marco Riccardi},
journal = {Formalized Mathematics},
keywords = {exponential objects; functor category; natural transformation},
language = {eng},
number = {4},
pages = {351-369},
title = {Exponential Objects},
url = {http://eudml.org/doc/276848},
volume = {23},
year = {2015},
}

TY - JOUR
AU - Marco Riccardi
TI - Exponential Objects
JO - Formalized Mathematics
PY - 2015
VL - 23
IS - 4
SP - 351
EP - 369
AB - In the first part of this article we formalize the concepts of terminal and initial object, categorical product [4] and natural transformation within a free-object category [1]. In particular, we show that this definition of natural transformation is equivalent to the standard definition [13]. Then we introduce the exponential object using its universal property and we show the isomorphism between the exponential object of categories and the functor category [12].
LA - eng
KW - exponential objects; functor category; natural transformation
UR - http://eudml.org/doc/276848
ER -

References

top
  1. [1] Jiri Adamek, Horst Herrlich, and George E. Strecker. Abstract and Concrete Categories: The Joy of Cats. Dover Publication, New York, 2009. Zbl0695.18001
  2. [2] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377–382, 1990. 
  3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91–96, 1990. 
  4. [4] Francis Borceaux. Handbook of Categorical Algebra I. Basic Category Theory, volume 50 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, 1994. 
  5. [5] Czesław Byliński. Introduction to categories and functors. Formalized Mathematics, 1 (2):409–420, 1990. 
  6. [6] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1): 55–65, 1990. 
  7. [7] Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. 
  8. [8] Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357–367, 1990. 
  9. [9] Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. 
  10. [10] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. 
  11. [11] Krzysztof Hryniewiecki. Graphs. Formalized Mathematics, 2(3):365–370, 1991. 
  12. [12] F. William Lawvere. Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories. Reprints in Theory and Applications of Categories, 5:1–121, 2004. Zbl1062.18004
  13. [13] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer Verlag, New York, Heidelberg, Berlin, 1971. Zbl0232.18001
  14. [14] Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147–152, 1990. 
  15. [15] Marco Riccardi. Object-free definition of categories. Formalized Mathematics, 21(3): 193–205, 2013. doi:10.2478/forma-2013-0021.[Crossref] Zbl1298.18001
  16. [16] Marco Riccardi. Categorical pullbacks. Formalized Mathematics, 23(1):1–14, 2015. doi:10.2478/forma-2015-0001.[Crossref] Zbl1317.18006
  17. [17] Andrzej Trybulec. Enumerated sets. Formalized Mathematics, 1(1):25–34, 1990. 
  18. [18] Andrzej Trybulec. Isomorphisms of categories. Formalized Mathematics, 2(5):629–634, 1991. 
  19. [19] Andrzej Trybulec. Natural transformations. Discrete categories. Formalized Mathematics, 2(4):467–474, 1991. 
  20. [20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. 
  21. [21] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1 (1):73–83, 1990. 
  22. [22] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.