Category of categories as a foundation of mathematics - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-22T10:52:18Z http://mathoverflow.net/feeds/question/9269 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/9269/category-of-categories-as-a-foundation-of-mathematics Category of categories as a foundation of mathematics Marc Nieper-Wißkirchen 2009-12-18T13:08:20Z 2011-02-15T21:07:54Z <p>In</p> <blockquote> <p>Lawvere, F. W., 1966, “The Category of Categories as a Foundation for Mathematics”, Proceedings of the Conference on Categorical Algebra, La Jolla, New York: Springer-Verlag, 1–21.</p> </blockquote> <p>Lawvere proposed an elementary theory of the category of categories which can serve as a foundation for mathematics.</p> <p>So far I have heard from several sources that there are some flaws with this theory so that it does not completely work as proposed.</p> <p>So my question is whether there is currently any (accepted) elementary theory of the category of categories that is rich enough so that one can formulate, say, the following things in the theory:</p> <ul> <li>The category of sets.</li> <li>Basic notions of category theory (functor categories, adjoints, Kan extensions, etc.).</li> <li>Other important categories (like the category of rings or the category of schemes).</li> </ul> <p>The elementary theory I am looking for should allow me to identify what should be called a category of commutative rings (at best I would like to see this category defined by a universal 2-categorical property) or how to work with this category. I am not interested in defining groups, rings, etc. as special categories as this seems to be better done in an elementary theory of sets.</p> <p>P.S.: The same question has an analogue one level higher. Assume that we have constructed an object in the category of categories (=: CAT) which can serve as a, say, category C of spaces. Classically, we can associate to each space X in C the sheaf topos over it. In the picture I have in mind, one should ask whether there is a similar elementary theory of the category of 2-categories (=: 2-CAT). Then one should be able to lift the object C from CAT to 2-CAT (as one is able to form the discrete category from a set), define an object T in 2-CAT that serves as the 2-category of toposes, and a functor C -> T in 2-CAT.</p> http://mathoverflow.net/questions/9269/category-of-categories-as-a-foundation-of-mathematics/9270#9270 Answer by Andrew Stacey for Category of categories as a foundation of mathematics Andrew Stacey 2009-12-18T13:33:44Z 2009-12-18T18:25:50Z <p>There's some discussion of this at the nlab:</p> <p><a href="http://ncatlab.org/nlab/show/foundations#categorial_foundations_of_category_theory_5" rel="nofollow">http://ncatlab.org/nlab/show/foundations#categorial_foundations_of_category_theory_5</a></p> <p>That page is one of the, er-hem, least encyclopaedic pages in the n-lab, but it still has quite a lot of discussion on this issue. You are, of course, welcome to join in the discussion there. </p> <p>Is that any help?</p> <p>(<strong>Edit</strong>: link corrected to relevant part of n-lab page as per Mike Shulman's comment)</p> http://mathoverflow.net/questions/9269/category-of-categories-as-a-foundation-of-mathematics/9412#9412 Answer by Mike Shulman for Category of categories as a foundation of mathematics Mike Shulman 2009-12-20T07:25:30Z 2009-12-20T07:25:30Z <p>My personal opinion is that one should consider the <em>2-category</em> of categories, rather than the 1-category of categories. I think the axioms one wants for such an "ET2CC" will be something like:</p> <ul> <li>Firstly, some exactness axioms amounting to its being a "2-pretopos" in the sense I described here: <a href="http://ncatlab.org/michaelshulman/show/2-categorical+logic" rel="nofollow">http://ncatlab.org/michaelshulman/show/2-categorical+logic</a> . This gives you an "internal logic" like that of an ordinary (pre)topos.</li> <li>Secondly, the existence of certain exponentials (this is optional).</li> <li>Thirdly, the existence of a "classifying discrete opfibration" $el\to set$ in the sense introduced by Mark Weber ("Yoneda structures from 2-toposes") which serves as "the category of sets," and internally satisfies some suitable axioms.</li> <li>Finally, a "well-pointedness" axiom saying that the terminal object is a generator, as is the case one level down with in ETCS. This is what says you have a 2-category of categories, rather than (for instance) a 2-category of stacks.</li> </ul> <p>Once you have all this, you can use finite 2-categorical limits and the "internal logic" to construct all the usual concrete categories out of the object "set". For instance, "set" has finite products internally, which means that the morphisms $set \to 1$ and $set \to set \times set$ have right adjoints in our 2-category Cat (i.e. "set" is a "cartesian object" in Cat). The composite $set \to set\times set \to set$ of the diagonal with the "binary products" morphism is the "functor" which, intuitively, takes a set $A$ to the set $A\times A$. Now the 2-categorical limit called an "inserter" applied to this composite and the identity of "set" can be considered "the category of sets $A$ equipped with a function $A\times A\to A$," i.e. the category of magmas.</p> <p>Now we have a forgetful functor $magma \to set$, and also a functor $magma \to set$ which takes a magma to the triple product $A\times A \times A$, and there are two 2-cells relating these constructed from two different composites of the inserter 2-cell defining the category of magmas. The "equifier" (another 2-categorical limit) of these 2-cells it makes sense to call "the category of semigroups" (sets with an associative binary operation). Proceeding in this way we can construct the categories of monoids, groups, abelian groups, and eventually rings.</p> <p>A more direct way to describe the category of rings with a universal property is as follows. Since $set$ is a cartesian object, each hom-category $Cat(X,set)$ has finite products, so we can define the category $ring(Cat(X,set))$ of rings internal to it. Then the category $ring$ is equipped with a forgetful functor $ring \to set$ which has the structure of a ring in $Cat(ring,set)$, and which is universal in the sense that we have a natural equivalence $ring(Cat(X,set)) \simeq Cat(X,ring)$. The above construction then just shows that such a representing object exists whenever Cat has suitable finitary structure.</p> <p>One can hope for a similar elementary theory of the 3-category of 2-categories, and so on up the ladder, but it's not as clear to me yet what the appropriate exactness properties will be.</p> http://mathoverflow.net/questions/9269/category-of-categories-as-a-foundation-of-mathematics/55552#55552 Answer by godelian for Category of categories as a foundation of mathematics godelian 2011-02-15T21:07:54Z 2011-02-15T21:07:54Z <p>I've just run into your question now. I realized it's over a year since it was asked, but since the question is not closed and I happen to have at hand some references (as I'd been interested in such developments for a while), perhaps you should take a look at the following proposals.</p> <p>Lawvere's original paper was indeed flawed, as reviewed by Prof. Isbell. Something later known as "category description theorem", a way to generating objects in the theory (i.e. categories) from some description of its intuitive structure, happened to be non provable in the original theory. A thorough review of the paper including ways to fix this and save a considerable portion can be found in: Blanc G., Preller A., Lawvere’s basic theory of the category of categories. Journal of Symbolic Logic 40 (1975, no. 1), 14–18.</p> <p>Subsequent proposals also try to address the point of the "category description theorem" by taking a variant of it as an axiom. This is done in Blanc G., Donnadieu M. R., Axiomatisation de la catégorie des catégories. Cahiers de topologie et géométrie différentielle 77 (1976, no. 2), 1–35.</p> <p>Finally, McLarty proposed a clean, elegant and well presented axiomatization where proofs of independence and relative consistency are given. This can be found in McLarty, C., Axiomatizing a category of categories. Journal of Symbolic Logic 56 (1991, no. 4), 1243–1260. McLarty theory was meant to be taken in conjunction with certain axioms for specific categories or functors needed for specific purposes.</p> <p>But I believe that all these three proposals are able to formulate the three bullets you mentioned in the first part of your question. For some other purposes one should take a closer look at them.</p>