3
$\begingroup$

I mean, I know that a category consists a class of objects and a class of morphisms, satisfying some axioms. What confuses me is that, in set theory, we define a group to be a tuple $\langle G,\cdot\rangle$ where G is a set and · is an operation. One can rewrite the sentence "$\langle G,\cdot\rangle$ is a tuple, $G$ is a set and $\cdot$ is an operation" in extremely formal language, if necessary. But——if we build up the category theory based on the language of set theory——what exactly is a category? A conglomerate that contains a class of objects and a class of morphisms?

If we build the category theory completely independent of set theory, then how would the axioms be like? Are they based on first-order language? Could they be wrote down in some way as formal as those axioms of ZFC or NBG? So far I haven't seen such a formal definition on my textbooks.

By the way, since I knew the word "conglomerate", I've been wondering if we could define some sense "larger and larger" after set, class and conglomerate, and even use something like "transfinite definition". But I guess this question may be too stupid to ask separately so I just wrote it here.

$\endgroup$
  • 1
    $\begingroup$ If we build the category theory completely independent of set theory then how would the axioms be like? this is done in the first chapters of Categories for the Working Mathematician by Mac Lane. You should check it out. The first sentence of chapter 1 is: First we describe categories directly by means of axioms, without using any set theory, and call them "metacategories". The spirit of the axioms is graph-based, actually. $\endgroup$ – rschwieb Apr 25 '17 at 13:21
  • 1
    $\begingroup$ @1830rbc03 Symbols should only be used to abbreviate once their usage has been well established, or the author can safely assume the reader understands them. Starting a ground-up exposition of a discipline with a lot of symbols would be a very obtuse thing for an author to do. I don't know why seeing words in a mathematical text would be confusing... words are just very information-heavy symbols. Of course, a text can have too many words but this is not the case for CftWM. $\endgroup$ – rschwieb Apr 25 '17 at 13:44
  • 1
    $\begingroup$ You can see Lawvere, Conceptual Mathematics. $\endgroup$ – Mauro ALLEGRANZA Apr 25 '17 at 14:09
  • 1
    $\begingroup$ Also Rodin, Axiomatic Method and Category Theory. $\endgroup$ – Mauro ALLEGRANZA Apr 25 '17 at 14:09
  • 1
    $\begingroup$ And, as suggested, MacLane, Categories for the Working Mathematician. $\endgroup$ – Mauro ALLEGRANZA Apr 25 '17 at 14:10
3
$\begingroup$

1) We can define thing which have name "metacategory" in purely formal way, using only first-order logic. To do this you just need to write axioms of reflexive graph and append one more predicate to signature $\operatorname{comp}(f,g,h)$ which says that $f = g \circ h$. Fully formal axioms you can find in Mac Lane book "Category for working mathematician".

1.1) It's not pretty comfortable to think about composition like about predicate, not like about operation. So, it's seems more natural to define category theory not in regular first-order logic but in first-order logic with depended sorts (FOLDS) which is more in type-theoretic style. See nLab and related links.

2) When you define it you can interpret your theory in $\mathbf{ZFC}$, $\mathbf{NBG}$ or even in another categories of special types (like toposes or finite complete categories). But such interpretations gives us only, in some sense, "small" categories. For example in $\mathbf{NBG}$ you can't define "$\mathbf{Class}$ category" because of Russel paradox. So it doesn't cover all categories which we want to consider.

3) I know only one way to, in some sense, avoid this Russel-Paradox-type problem. It's, like you say, just to build infinite series of "embedded universes" and when we want to extend our possibilities we just need to do step on higher universe. In set-theoretic style we can do this using Grothendieck universes and in type-theoretic style we can use type universes (see HoTT book 1.3) but it's just the same construction. On my point of view this is terrible and unaesthetic solution, it's just dirty hack which repeats infinitely many times. And it's actually doesn't really avoid the problem, because in $\mathbf{ZFC}$ with Grothendieck axiom you still can't define $\mathbf{Set}$ category (which contain all universes). But it's seems like no one knows another. 3:

$\endgroup$
  • $\begingroup$ Excuse me but I still have trouble with some basic matters. Do we need extra predicates to say that something is an object or something is a morphism from something to something? $\endgroup$ – 1830rbc03 Apr 25 '17 at 14:32
  • 1
    $\begingroup$ Yes, you can do it in such way. Another way: identify objects with identity arrows and then you can talk only about arrows in your theory. So, you need predicate symbol "IsIdentityMorphism(f)" functional symbols "Dom(f)" and "Codom(f)" and predicate symbol "Composition(f,g,h)". You can write axioms by yourself. $\endgroup$ – kp9r4d Apr 25 '17 at 14:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.