You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Patrick Nicodemus (Apr 30 2023 at 01:46):Recently researchers have formalized various cool things in Isabelle/HOL, such as schemes https://arxiv.org/abs/2104.09366 and strict omega categories https://devel.isa-afp.org/entries/StrictOmegaCategories.html#
The internal logic of Isabelle is that of a classical topos. Well, it is slightly stronger than that because it has polymorphism, so one can define various endofunctors on this topos, like the endofunctor X -> X^A for some fixed object A. Intuitively I would expect that any construction in topos theory which is parametric in a fixed number of arbitrary objects could be formalized as an "endofunctor" in Isabelle.
I would like to ask for resources on doing mathematics internal to a topos. I am familiar with Sheaves in Geometry and Logic and other classic books but I want stuff that scales more realistically than that. In particular I would like to do category theory in Isabelle and I am wondering how topos theorists have generally axiomatized stuff like this.
I do not want to just do category theory per se but category theory which is actually applicable to the rest of mathematics in this topos, so that results from category theory can be applied to the category of groups, rings, fields, etc. internally in this topos. How would you define something like the category of groups in a topos? How would you say that this has all small limits? Especially, how would you state and prove Yoneda, what is the category of presheaves relative to an internal category, etc. What are weighted colimits?
One thing you could do is assume additional axioms stating that some fixed object is a model of ZFC in the internal language of topos theory, and then you would have an internal category of sets, groups, etc. and that would presumably take you pretty far. Has this approach been studied? What do you call "topos theory over an internal topos?"
At the time being I am thinking Jean Benabou's work on category theory internal to a fibration is most relevant.
David Michael Roberts (Apr 30 2023 at 03:42):Defining the category of models of a finite-product (aka Lawvere) theory like groups, or more generally a finite-limit theory (aka essentially algebraic theory) in a topos is actually rather easy, since it only uses the finite limits that exist in the topos, and so one might as well assume the much more general case. It's when one has a geometric theory, like that of local rings, for instance, that dealing with the internal logic of a topos with all its bells and whistles starts to get interesting.
David Michael Roberts (Apr 30 2023 at 03:44):If you want to say a given fixed object is a model of ZFC (or, more charitably, a structural version of set theory), you might want to consider Algebraic Set Theory, which works with a pretopos with axioms that give a category of classes, inside which is an object that is V, familiar from traditional set theory, albeit flexible enough to deal with things like IZF and CZF as well.
Graham Manuell (Apr 30 2023 at 13:08):It's not difficult to handle these things constructively, but is question behind the question about how to deal with proper classes in a topos? You might want to look at the nlab page for [[locally internal category]], as well as Shulman's paper on stack semantics. The latter also discusses the link to material set theories such as ZFC.
Matteo Capucci (he/him) (May 03 2023 at 13:48):Obligatory plug of Ingo Blechschmidt's PhD thesis (you find it on google). He does a bunch of algebraic geometry in the topos of sheaves over a space.
Patrick Nicodemus (May 07 2023 at 20:45):@Mike Shulman Hi Mike. I am currently reviewing your paper on Set Theory for Category Theory and I do not fully understand what is meant formally when you discuss indexed categories and fibrations over a topos.
What is the intended formalism? Presumably these large categories cannot be purely discussed within the internal language of topos theory. So if one is intending to take fibrations or indexed categories over a topos as a foundation for mathematics, including the discussion of large categories, what is the formal language that one associates to this? How do I say "Let J be an indexed category" in such a formalism?
Patrick Nicodemus (May 07 2023 at 20:56):I am interested in developing mathematics in a topos without reference to an external category of sets and I am trying to understand how I can speak about indexed categories and fibrations without assuming a background set theory in which to work.
I understand the idea that we do not want to rely on an external notion of limit, which is why we are working with the family fibrations, so that we can discuss limits and colimits via quantifiers (adjoints). But sometimes I read (in various sources) paragraphs that say something along the lines of "Instead of working with a category, we associate to each object in our topos a category" and I do not understand what is meant by the word "category" here.
I understand how one defines various concrete categories (family fibrations) like the category of groups - you start with S/X and then consider the group objects in that category. But are we restricted to these concrete categories like groups, topological spaces and so on? I don't see how to generalize this to give a general definition of a "category" (i.e. a fibration with potentially large fibers)
Mike Shulman (May 08 2023 at 02:41):Good question. One approach is to treat large categories in the same way that one does in ZFC, as proper classes that are determined by a logical formula, which can then be interpreted in any slice. In ZFC it is also not possible to state a single theorem of the sort "for any large category" -- any statement of that form is technically a theorem-schema, with one instance for every logical formula that could define a large category.
Mike Shulman (May 08 2023 at 02:42):However, if you want something more like NBG or ZFC+U, then I think the way to go is what I sketched in this talk. I haven't managed to write that up formally yet.
Patrick Nicodemus (May 28 2023 at 15:57):Mike Shulman said:
However, if you want something more like NBG or ZFC+U, then I think the way to go is what I sketched in this talk. I haven't managed to write that up formally yet.
I am interested (in this thread at least) in formalizing category theory in Isabelle/HOL, which is essentially a classical Boolean topos with some additional features like type polymorphism I'm not sure how to describe well categorically. On the other hand it has some painful features which disqualify it from being a topos. There are no empty types and subset comprehension is restricted to predicates which you can prove hold at at least one point.
I think the most likely bet here is using the notion of universes in a topos. https://ncatlab.org/nlab/show/universe+in+a+topos
What is the current status of developing large scale mathematics (like category theory) in a topos with a universe? Can this be done in a way that it integrates well with normal topos theory without a universe, or would most of the work have to be done with terms of universe type?
I think you would want to work, practically speaking, in the family fibration associated to the universe.
Mike Shulman (May 28 2023 at 16:49):I don't know whether anything like that has been done formally. It should be straightforward, especially if you work in an internal dependent type theory, but I don't know if it's been written down.
Ryan Wisnesky (May 28 2023 at 16:52):One precise way to do HOL in CoC is here: https://www.researchgate.net/publication/2641362_The_Calculus_of_Constructions_and_Higher_Order_Logic
Patrick Nicodemus (May 28 2023 at 17:28):I think this is an important practical question. Because HOL is a simpler logic than CoC, automation for HOL will likely always be 10-15 years ahead of that of CoC, it seems doubtful to me that the gap will ever close - I am not saying CoC will never have good automation, I'm speaking in purely relative terms. Most researchers at the intersection of formal methods and category theory have been interested in MLTT/CoC but if real, genuine category theory can be done in a faithful elegant way inside HOL in such a way that it's actually applicable to prove general results of topology and algebra, I think it is worth doing. Essentially I am saying, you have a topos, you can assume whatever axioms you want in the internal logic, universes, etc. (but not small cocompleteness!) Somebody asks you "Can you state and prove that the category of small topological spaces is small-cocomplete?" Do we have a good answer? Kevin Buzzard has speculated that the answer is no. Schemes and some stuff on infinity categories have recently been formalized in HOL but I'm not yet convinced that those definitions are "right" in the sense that they actually allow interesting mathematics to accumulate on top of them, i.e. you can hack together a reasonable definition of a presheaf in a weak logic but if you can't state and prove the Yoneda lemma, is there really a point?
There's also a substantial amount of category theory in Isabelle/HOL formalized inside a type which is axiomatized to satisfy the ZFC axioms, which is definitely expressive enough to do all your math, but you are not really taking advantage of the HOL at that point. How can we do large-scale category theory in a way which actually takes advantage of HOL?
I wonder how practical it would be (for formalizing) to work in an internal language of dependent type theory inside HOL.
Mike Shulman (May 28 2023 at 18:22):I'm doubtful that there is a very elegant way to do serious category theory inside HOL, due to the lack of a congenial way to represent families of types. However, it should certainly be possible. What is Kevin worried about? Obviously one needs to assume that the universe is closed under small products and coproducts, but given that there shouldn't be any problem proving small-(co)completeness of small topological spaces or anything similar.