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.
added a second equivalent definition at quasi-category , one that may be easier to motivate
Added pointer to Rezk 16
Removed the following query box, as this has been dealt with under related concepts:
+– {: .query} Stephen Gaito: If we want to weaken this even further to provide a simplicial model of, for example, a (∞,2)-category, how would we do this?
Would we apply the lifting condition on all but three of the indices… and if so which three? (The first, last and ????)
Mike Shulman: You may be looking for something along the lines of a weak complicial set.
=–
I certainly would not regard what is referred to as the fundamental theorem of category theory in the notes linked to (namely that a fully faithful and essentially surjective functor defines an equivalence of categories) as a fundamental theorem of category theory; indeed, I always avoid it.
While I don’t disagree with Richard, I didn’t spot mention of this “fundamental theorem” either in this thread or in the article quasi-category. What’s the reference?
I use the term (partly in jest) in my quasicategory notes. But only partly in jest: it’s a powerful tool, and is somewhat non-trivial. In the setting, it’s even more non-trivial, and is very much in the spirit of Whitehead’s theorem (on homotopy equivs of CW complexes = weak equivs), which is kind of a fundamental theorem of classical homotopy.
Thanks for clearing that up, Charles. I’m guessing Richard avoids it partly because of its non-constructive nature (e.g., the axiom of choice is needed for it), but maybe he’d like to amplify.
IMHO, it’s only non-constructive if you insist on using wrong definitions. (-: In a set theoretic foundation without choice, “functor” should mean “anafunctor”; whereas in HoTT we have univalent categories that also satisfy the theorem constructively. I can see regarding it as fundamental – it’s essentially a category-theoretic manifestation of the axiom of unique choice, i.e. a “functor comprehension principle”, and the analogous function comprehension principle is certainly fundamental to set theory.
Word. :-)
My objections to it are principally twofold: firstly, as Todd guessed, because of the non-constructivity, and secondly because it does not feel to me like pure category theory (it makes use of a set-theoretic view of a category, so is not obviously able to be expressed internally to the 2-category (or similar) of categories).
No doubt both of these points can be disputed. Mike has already disputed the first one, and no doubt someone will point out that one can formulate the notion of a fully faithful and essentially surjective functor internally to something like the 2-category of categories, and probably prove the result in that setting using some kind of category-theoretic variant of the axiom of choice.
I don’t really wish to discuss these two points. I’ve never been very keen on anafunctors, and my firm opinion that there is no way to get around the use of the axiom of choice here. If one changes something so that one doesn’t need it, one is probably losing something elsewhere (simplicity, if nothing else). Mostly, I just find that arguments that avoid the use of this fact are almost ’better category theory’ according to my aesthetic taste, and I’ve always found that one can avoid it if one understands whatever one needs it for deeply enough. But this is subjective, so we’re not going to get very far with trying to convince one another :-)!
Thanks, interesting.
Somebody here might know who first stated the “fundamental theorem of category theory” (p. 104).
My guess is that one should check Tôhoku, where equivalences were introduced.
Hmm, on checking, it doesn’t seem so. Grothendieck remarks that an equivalence of categories (i.e. an adjoint equivalence) means the functors involved are fully faithful, but without using that phrase. He doesn’t make the explicit observation about essential surjectivity, merely pointing out the (invertible) unit and counit, as we call them today. So I guess one needs to find when was the first usage of “fully faithful” and “essentially surjective”. It seems like the sort of thing that was folklore, and written down in CWM (similar to the Yoneda lemma). Maybe Kan’s early work on adjunctions is a good place to check…
hyperlinked the title of
added pointer to:
added links to these references:
Michael Boardman, Rainer Vogt, Homotopy invariant algebraic structures on topological spaces, Lecture Notes in Mathematics 347 Springer (1973) [doi:10.1007/BFb0068547]
Rainer Vogt, Homotopy limits and colimits, Math. Z., 134 (1973) 11-52 [doi:10.1007/BF01219090, eudml:171965]
here and elsewhere
and for this one:
1 to 19 of 19