Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
you can define to be the 2-category of all -small categories, where is some Grothendieck universe containing . That way, you have without contradiction.
Do you agree with changing this to
” you can define to be the 2-category of all -small categories, where is some Grothendieck universe containing . That way, for every small category , you have the category an object of without contradiction. This way, e.g. the diagram in Cat used in this definition of comma categories is defined. “
?
Reason: motivation is to have the pullback-definition of a comma category in (For others, it’s about the diagram here) defined, or rather, having Cat provide a way to make it precise. Currently, the diagrammatic definition can either be read formally, as a device to encode the usual definition of comma categories, or a reader can try to consult Cat in order to make it precise. Then they will first find only the usual definition of Cat having small objects only, which does not take care of the large category
used in the pullback-definition. Then perhaps they will read all the way up to Grothendieck universes, but find that option not quite sufficient either since it only mentions Set, but not . It seems to me that large small-presheaf-categories such as can be accomodated, too, though.
(Incidentally, tried to find a “canonical” thread for the article “Cat”, by using the search, but to no avail. Therefore started this one.)
Actually, you can do even better: you don’t need to be ()-small there. The point is that if consists of -small categories such as , and is cartesian closed, you can even discuss things like without fear of contradiction.
So as a sample replacement, you could have
you can define to be the 2-category of all -small categories, where is some Grothendieck universe containing . That way, you have without contradiction, as well as constructs such as since is cartesian closed. Note however that will generally not be locally -small unless is itself (essentially) -small.
Thanks for the explanation. So this would be one way to make the two articles more consistent.
However, on second thought it seems to me that
my edit from “1-category Cat” to “2-category Cat” here was not wrong, but beside the point,
to tell readers how to use the diagram in here](https://ncatlab.org/nlab/show/comma+category#AsAFiberProduct) one should,
either
(0) even go one step back from conceiving of Cat as a 1-category and find some precise and appropriate way of telling them “read that diagram formally, as mnemonic, or formal encoding of the axioms of comma categories”,
or
(1) even go one step beyond conceiving of Cat as (some sort of) 2-category, and tell readers to take the diagram as a diagram in CAT.
The point of (0) and (1) is of course that the essence is not what categorical structure Cat could support, but rather some bare minimum of categorical structure that it always has. Therefore, emphasizing viewing it as a 2-category is some sort of “false emphasis”. Again, this is the “how-to-tell-readers-to-read-the-diagram-formally-issue”. This is likely to be a very well-known issue. The terms “metacategory” and “protocategory” (in the sense of Freyd and Scedrov) come to mind, but again, mentioning such concepts under the diagram seems beside the intent of the diagram, which is very useful, by the way.
The essence is probably “what is a standard term for model-of-the-first-order-theory-of-categorie-which-also-has-pullbacks”.
(It seems to me that one cannot do without choosing some model which has some sort of limits, for otherwise (f/g) would not be uniquely defined, and the need for some feature of limit seems to get one some step away from what Mac Lane called metacategories. It seems to me that the first-order-definitions of cones alone are more or less enough to use this diagram to encode the definition of comma categories, the fact that the pullback is the terminal cone seems somewhat secondary here.)
Just a quick observation: the idea of being a 2-category (which is to say a -enriched category) comes from being a special kind of 1-category, namely a cartesian closed category. As with any symmetric monoidal closed category , such structure enables one to see as being -enriched.
I do think the change from “1-category” to “2-category” was actually wrong, or at least misleading, and I’ve reverted it. On the nLab, “2-category” usually means “weak 2-category” and thus a pullback would mean a weak 2-limit, whereas in that definition we really do want the strict limit in the 1-category (or equivalently the strict 2-limit in the strict 2-category , but that is needless complication).
I also don’t understand what you are worried about. Any version of at all includes the interval category, has finite limits, and is cartesian closed, so that that diagram makes sense without any worries about universes.
Cat did not yet mention explicitly that it is cartesian closed. Added that statement, with two references. Added these two references to cartesian closed, too.
Could we briefly summarize in some sort of list what methods have been used so far in the literature to prove that the 1-category Cat is cartesian-closed?
One entry I woud give in this respect is
The cartesian-closedness of Cat is a corollary of this.
Incidentally: does the above embedding imply notable categorical properties of Cat that one cannot get otherwise?
Yeah, I don’t think it’s Stephen Lack who should be credited for that. The construction itself called taking the nerve of a category, and it’s been known for a very long time (since 1958, I would guess – Dan Kan wrote a famous paper).
And in such an approach, it’s not so much the full embedding as it is the fact that this has a left adjoint that preserves products, that one can use to derive cartesian closure of from that of .
So sure, that’d be one approach. But I think it’s more complicated than just proving it directly. It’s not exactly a mystery how this goes. You could see for instance chapter 7 here.
A “list” of proofs for such a basic result seems a little ponderous to me.
(Incidentally, the current description of the nerve of a 1-category at nerve seems a little heavy to me. It is after all very easily described. Edit: Oh, I see that definition 3.4 gives the simple abstract description. I think what comes before, while “concrete”, makes it IMO look harder than it is.)
Thinking over it a little more: we have
The direct method (which according to Cat is in Mac Lane, and I gave another reference above). This is probably simplest. Highly recommended!
The method that proceeds by characterizing the (essential) image of the nerve , as those simplicial sets which takes certain pushouts in to pullbacks in . I think that’s due to Grothendieck, although they are called Segal conditions. Then use this characterization to show that is an exponential ideal in . This has as a corollary that is cartesian closed.
Prove by some method or other that the reflector preserves products. But this looks very close to (if not the exact same as) the prior method, since there is the general result that the reflector preserves finite products iff the inclusion is an exponential ideal inclusion.
That’s all I got so far.
Very useful answer, thanks.
The direct method (which according to Cat is in Mac Lane, and I gave another reference above). This is probably simplest. Highly recommended!
The references given in Cat so far were to places in books where no detailed exposition of cartesian closedness of Cat appears to be given.
I therefore added, for tidiness now confined to a footnote, the reference you gave, to Cat. I also wrote some summarizing remarks along with the reference, into the footnote; maybe it will be better if someone has a quick look at the footnote and perhaps redacts it. In particular, I shied away from calling the functor a presheaf, for reasons I cannot verbalize, although calling it by this name may add further structure.
I redacted the footnote, moving the references into the main text (and adding a mention of the other method from #10 above). This page is not the place for rehashing various ways to express the meaning of “cartesian closed”; if we feel that more explanation of that is merited then it should go at the page cartesian closed category. In general I think footnotes are rarely the best formatting choice: if something is important and relevant enough to say on a page, then say it directly; otherwise put it on some other page with a hyperlink.
added cross-link with elementary theory of the category of categories and pointers to
William Lawvere, The Category of Categories as a Foundation for Mathematics, pp.1-20 in Eilenberg, Harrison, MacLane, Röhrl (eds.), Proceedings of the Conference on Categorical Algebra - La Jolla 1965, Springer Heidelberg 1966 (doi:10.1007/978-3-642-99902-4_1)
John Gray, Formal category theory: adjointness for 2-categories, Lecture Notes in Mathematics, Vol. 391. Springer 1974 (doi:10.1007/BFb0061280)
added pointer to:
added pointer to
added pointer to:
Added a remark (here) on ordinary limits and colimits in the 1-category , for the colimits with pointer to Section 4 in:
1 to 17 of 17