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.
Fawzi Hreiki (Feb 04 2021 at 16:53):I've heard that many kinds of categories with extra structure can be defined internal to a category with finite limits, usually by equipping internal categories with appropriate adjoints. I can see how this works for finite limits, finite colimits, and NNOs. But how can this be done for toposes? I can't see how you can even express the notion of monomorphism without having the universal quantifier.
John Baez (Feb 04 2021 at 17:09):@David Michael Roberts (and probably plenty of other people, but unfortunately not me) should be able to answer this question, since he wrote:
It has been known for some time that one can define a topos as a model of a (finitary) essentially algebraic theory (or in other words, can be defined internal to any category with finite limits).
Nathanael Arkor (Feb 04 2021 at 17:11):It's in Dubac–Kelly's A Presentation of Topoi as Algebraic Relative to Categories or Graphs.
John Baez (Feb 04 2021 at 17:12):Thanks.
Fawzi Hreiki (Feb 04 2021 at 17:13):Perfect! Thanks
Nathanael Arkor (Feb 04 2021 at 17:14):(One may have to combine this result with the fact that categories of algebras for finitary monads on locally finitely presentable categories are themselves locally finitely presentable; that Cat is locally finitely presentable; and that locally finitely presentable categories are the categories of models of finite limit theories.)
David Michael Roberts (Feb 05 2021 at 01:41):I really should write up my notes on this.
David Michael Roberts (Feb 05 2021 at 06:52):I should add that monomorphisms have a finite-limit characterisation, they pull back along themselves to give the identity map.
Fawzi Hreiki (Feb 05 2021 at 09:10):I had totally forgotten about this. Of course.
Fawzi Hreiki (Feb 05 2021 at 09:17):Also, Freyd’s Aspects of Topoi has an essentially algebraic definition of cartesian closure
David Michael Roberts (Feb 05 2021 at 09:45):So one can define the subcategory of the arrow category with objects the monomorphisms, and with arrows the pullback squares, and then demand that this has a terminal object. In fact it's rather nice to write down an algebraic definition of an internal topos all in terms of internal adjunctions (cartesian closure is a little more tricky, in that it happens in a slice category, IIRC). Then I believe that writing down the same thing in the bicategory of internal cats and anafunctors (need to maybe have a regular category here, or something a little weaker) gives a definition of internal topos that doesn't demand that we've specified actual pullbacks or internal homs. A terminal object and a subobject classifier is likewise only demanded to exist up to isomorphism, though depending on the ambient regular category one is working with (maybe every regular epi to the terminal object splits), one might be able to specify these exactly.
However, the main point of introducing anafunctors is not to just define internal toposes, it means we can write down logical morphisms between internal toposes that do not necessarily preserve the internal homs or subobject classifier on the nose, only up to isomorphism.
What would be really cool is if there was some kind of definition of internal topos that used formal category theory (basically: the 2-category structure on Cat plus extra things like maybe a Yoneda structure). I wish I knew how to do this!
Fawzi Hreiki (Feb 05 2021 at 10:41):Well one thing I’ve wondered about is how 1-topos theory can emerge from 2-topos theory. Because in a 1-topos, the subobject classifier is a Heyting algebra but this follows from the other axioms and is not postulated a priori.
Fawzi Hreiki (Feb 05 2021 at 10:42):So the corresponding truth value object in a 2-topos should morally be a 1-topos in virtue of the other axioms
David Michael Roberts (Feb 05 2021 at 11:49):In the 2-category of groupoids the forgetful functor from pointed sets and bijections to sets and bijections acts a bit like (and ditto the 2-category of categories, cf the Grothendieck construction) Added in the latter case, it's pointed sets and functions, and Set itself (realised what I wrote was super ambiguous)
David Michael Roberts (Feb 05 2021 at 11:51):But this really is brushing up against universes of types of a fixed h-level à la HoTT. I'm not so sure about 2-toposes in the (2,2)-world, in the sense of @Mike Shulman .
Mike Shulman (Feb 05 2021 at 14:08):Well, there's Theorem 10.1.12 in the HoTT Book, which can be interpreted semantically as saying that in the "internal type theory of a (2,1)-topos" one can prove that the discrete-fibration-classifier is a 1-topos.
Nathanael Arkor (Feb 05 2021 at 17:11):What would be really cool is if there was some kind of definition of internal topos that used formal category theory (basically: the 2-category structure on Cat plus extra things like maybe a Yoneda structure). I wish I knew how to do this!
One can formulate the definition of cartesian-closed object in a cartesian 2-category, and also objects that are complete with respect to a class of weights (equivalently algebras for a coKZ pseudomonad), so I imagine "finitely complete cartesian-closed object" should not cause significant difficulties. The subobject classifier seems more difficult: perhaps equipping the object with a suitable generalised universal bundle (provided that the 2-category is finitely complete) would give something along the right lines? (A Grothendieck topos in a 2-category with a Yoneda structure should be much more straightforward.)
Fawzi Hreiki (Feb 05 2021 at 18:21):How do you define a Cartesian closed object in a 2-category?
Nathanael Arkor (Feb 05 2021 at 18:33):Assuming that has finite products, a cartesian-closed object is one for which the 1-cells have right adjoints, and for which has a right adjoint for all .
Mike Shulman (Feb 05 2021 at 22:01):That's not a real great definition, though, since it refers to global points. A better definition requires some notion of "opposite" with a duality than can be applied to some notion of profunctor, such as in a Weber 2-topos or a compact closed equipment.
Nathanael Arkor (Feb 05 2021 at 22:05):Yes, I also found that aspect dissatifying (though it is the definition given by Weber in his paper on 2-toposes).
Nathanael Arkor (Feb 05 2021 at 22:06):Do you have a precise definition in mind, or simply some idea of what an ideal definition should look like?
Nathanael Arkor (Feb 05 2021 at 22:10):Perhaps it would be better to axiomatise the closed structure using a 2-variable adjunction.
Mike Shulman (Feb 05 2021 at 22:29):Day-Street in "Monoidal bicategories and Hopf algebroids" give a definition of "closed map pseudomonoid" in any monoidal bicategory with duals. So if your 2-category has the structure to define such a bicategory of its objects and "profunctors" between them (like the 2-sided fibrations that Weber uses), you can interpret that therein (and also require the pseudomonoid structure to be cartesian). But I think if you compile it out, it should make sense in a Weber 2-topos: you have , from that you construct a representable fibration from to , then transpose that to a fibration from to , and require that the latter be corepresentable by some hom-map .
Nathanael Arkor (Feb 05 2021 at 22:40):Ah, interesting, thanks. That is much more satifsying.
Fawzi Hreiki (Feb 06 2021 at 00:04):m is the product map right?
Fawzi Hreiki (Feb 06 2021 at 00:04):If we’re interpreting this in CAT
John Baez (Feb 06 2021 at 19:28):Yes, I think it's the product map.
Fawzi Hreiki (Feb 14 2021 at 11:18):I know it’s a bit late coming back to this now, but I was reading Toposes, Triples, and Theories and in chapter 4 on sketches they construct the finite limit sketch of elementary toposes. So that’s also an answer to this.
David Michael Roberts (Feb 14 2021 at 12:01):For anyone else looking, it's section 4.11, starting on page 142 of the TAC Reprint version.
David Michael Roberts (Feb 14 2021 at 12:06):In particular, they use the definition of a topos as a category with terminal objects, pullbacks, and power objects.
Leopold Schlicht (Dec 15 2021 at 19:20):In this video Joyal states a theorem he announced as the "main theorem of elementary topos theory from my point of view" a few minutes earlier: if is an elementary topos, then the category of (Grothendieck?) toposes over is equivalent to the category of (Grothendieck?) toposes internal to . Where can I read about that theorem?
Mike Shulman (Dec 15 2021 at 20:05):A few minutes later in the video he says that all his "toposes", including , are Grothendieck. (One could allow to be elementary, in which case the "toposes over " would also be elementary but the geometric morphisms would have to be required to be "bounded".) And he also says that by a "topos internal to " he actually means a site internal to , which I think is a rather confusing terminological choice. There are therefore various subtleties here if you want to make this an equivalence of categories (or even, more sensibly, 2-categories) because in general not every geometric morphism between toposes (even over Set) is represented by a morphism between two arbitrary sites chosen to present them. However, with those caveats I think the result is discussed in section B3.3 of Sketches of an Elephant, which attributes it to a paper by Diaconescu called "Change of base for toposes with generators" (which I have not read).
David Michael Roberts (Dec 15 2021 at 20:49):Another term would be "internal sheaves", as a bounded geometric morphism is equivalent data to a category of internal sheaves on an internal site.
Leopold Schlicht (Dec 16 2021 at 16:10):Thanks! What's the motivation for describing how some internal concepts look in a topos? Another question: what's the motivation for examining internal categories? Does this "internal" stuff has applications?
Mike Shulman (Dec 16 2021 at 17:05):Well, this theorem that Joyal quoted is one motivation! If you care about toposes over a base -- which, for instance, includes all algebraic geometers, since a variety defined "over" a field in the algebraic sense is in particular a topos over in this categorical sense -- then it's often handy to study them in terms of internal sites. And since a site is a kind of category, that's a reason to study internal categories.
Leopold Schlicht (Dec 16 2021 at 17:13):Thanks! By "to study them in terms of internal sites" you mean to constructively prove a theorem about sites so that it is true in the internal language of the topos at interest, and when one then looks at what the theorem means "externally" one automatically gets a theorem about toposes over a base, right?
Leopold Schlicht (Dec 16 2021 at 17:14):What are other typical motivations for studying internal categories?
Mike Shulman (Dec 16 2021 at 17:56):Yes.
Mike Shulman (Dec 16 2021 at 17:58):For other motivations, it not infrequently happens that a category arising "in nature" actually has the structure of an internal category, or some structure on an object of some category is naturally represented by an internal category. For instance, orbifolds are naturally represented as certain internal groupoids in the category of manifolds, and similarly for orbispaces. Stacks can be presented by certain internal categories in spaces/schemes/etc.
John Baez (Dec 17 2021 at 02:46):Yeah, it's pretty common that the set of objects and the set of morphisms of a small category has more structure than mere sets; then you're often dealing with an internal category. For example, differential geometers are often dealing with groupoids in some category of smooth spaces - like orbifolds, or Lie groupoids.
Other times familiar things turn out to be internal categories and this gives you a new outlook on them. For example, a 2-term chain complex of abelian groups is the same as a category internal to AbGp... and an (n+1)-term chain complex of abelian groups is the same as a strict n-category in AbGp. This reveals that the theory of chain complexes can be seen as a small branch of higher category theory.
Tim Hosgood (Dec 17 2021 at 07:10):how does this example of a 2-term chain complex work? how do you get a source and a target morphism out of just one differential?
Spencer Breiner (Dec 17 2021 at 13:49):Zero for source?
John Baez (Dec 18 2021 at 05:14):Yes. For the whole story see e.g. Section 3 of
Here we consider categories internal to Vect, but the idea works the same.
John Baez (Dec 18 2021 at 05:17):Until I learned that chain complexes were "infinitely categorified abelian groups" - that is, an elegant distillation of strict -categories internal to AbGp - they seemed like some kind of random thing that just mysteriously happened to be extremely important, and all the things people did with them seemed a bit magical.
Mike Shulman (Dec 18 2021 at 05:39):There's also another sense in which chain complexes are "infinitely categorified abelian groups" -- they're equivalent to -module spectra. But I suppose that's probably a bit much for this discussion... (-:O
John Baez (Dec 18 2021 at 14:16):The two facts fit together in a bigger picture. But yes, we were talking about internal categories.
Another nice example of why internal categories are interesting. Categories internal to Gp, also known as 2-groups, are useful in homotopy theory. Just as a pointed space has a fundamental group, it has a fundamental 2-group, which captures more information.
Tim Hosgood (Dec 18 2021 at 14:18):what does the H mean in ?
Ian Coley (Dec 18 2021 at 15:35):Eilenberg-Maclane Spectrum, i.e. is the spectrum which represents (co)homology with coefficients. https://ncatlab.org/nlab/show/Eilenberg-Mac+Lane+spectrum
John Baez (Dec 18 2021 at 15:40):turns an abelian group into a spectrum, so it expresses how spectra generalize abelian groups.
David Michael Roberts (Dec 18 2021 at 21:17):Just to put an answer here to @Tim Hosgood 's question, you get an internal groupoid in Vect, or Ab, etc, from a 2-term chain complex d:A-> B by taking obj=B, morphisms=AxB, source = projection, target of (a,b) is d(a)+b
Leopold Schlicht (Dec 27 2021 at 16:41):Thanks!
Leopold Schlicht (Feb 19 2022 at 19:24):Leopold Schlicht said:
Another question: what's the motivation for examining internal categories? Does this "internal" stuff has applications?
In Johnstone's first book on topos theory, internal categories are discussed at the very beginning: in chapter 2. In the introduction he mentions that he used internal categories in his construction of the associated sheaf functor for elementary topoi. If someone of you has read the book: are there other places in the book in which he uses internal categories? And how are internal categories applied, why are they useful in the book? They have to be very important if the author discusses them as early as in chapter 2.
John Baez (Feb 20 2022 at 00:49):One reason why Johnstone might talk about internal categories is that people who like topos theory like 'doing mathematics in a topos', and if you do category theory in a topos you're studying categories internal to a topos.
(Some size issues show up here, but not so much if you're studying small categories.)
Zhen Lin Low (Feb 20 2022 at 01:01):There is a theorem that says that for every bounded geometric morphism E → S there is an internal site in S and an equivalence (over S) between E and sheaves on that site. (Maybe S needs to have an NNO, I forget. But it does not need to be a Grothendieck topos.)
Zhen Lin Low (Feb 20 2022 at 01:03):A lot of the basic theory of Grothendieck toposes can be relativised by introducing a base topos S like this, but the price is that you have to use the machinery of internal categories and locally internal categories.
Morgan Rogers (he/him) (Feb 20 2022 at 09:13):This was standard for a long time (and I have an ongoing project about these). A few years ago, Olivia Caramello made the reasonable judgement that the price was too high: actually computing the internal sites and working with them is horrible. We have an abstract site-theoretic construction of a pullback of toposes over a base topos, but good luck actually computing it!
Instead, she had a look (or got one of her PhD students to look) at what could be done with stacks; note, though, that her research programme is mostly concerned with Grothendieck toposes. Many results are contained in the thesis of @Riccardo Zanfa, although I have to admit I haven't read much of it.
Zhen Lin Low (Feb 20 2022 at 09:16):Hmmm. Is that what those papers about stacks is about... interesting. Are you sure it's not just them reinventing locally internal category theory?
Morgan Rogers (he/him) (Feb 20 2022 at 09:42):I can't be sure since I haven't read enough, and I also am not familiar enough with locally internal category theory to recognize if someone were reinventing it.
Zhen Lin Low (Feb 20 2022 at 09:45):OK. I ask because a locally internal category is (among other things) a stack satisfying certain conditions.
Zhen Lin Low (Feb 20 2022 at 10:00):Maybe I should add that I mean "is" in the sense "should be" there. The conventional definition does not require or imply the stack condition, which I believe results in unintuitive situations like "there exists a terminal object" being true for some internal category even if there is no functor from the terminal internal category picking it out. (The axiom of unique choice is not applicable because terminal objects are not strictly unique!)
Reid Barton (Feb 20 2022 at 10:24):Ah I never understood that we are meant to interpret statements about internal categories as statements in the internal logic (since "internal category" makes sense also in other categories like Cat or Top where "internal logic" does not).
Reid Barton (Feb 20 2022 at 10:24):But isn't there still a separate issue around things like what it means to have say binary products, since the internal axiom of choice may fail?
Morgan Rogers (he/him) (Feb 20 2022 at 10:41):Yes, you have the difference between category with products and category with chosen products coming up. This is pointed out in a few constructions in the Elephant.
Zhen Lin Low (Feb 20 2022 at 11:36):In any topos – even any cartesian category really – we have the axiom of _unique_ choice, which tells us that any functional relation is realised by a function. Morally, a category with a terminal object, or binary products, or such that some object has a representable functor with a left adjoint, or whatever gadgets that are unique up to unique isomorphism, should be the same thing as a category with chosen gadgets, because the choice is essentially unique! The failure of this is more down to the foundations we choose to work in and the definitions we choose to work with than anything deep. In classical foundations where categories have a _set_ of objects we can (ab)use the axiom of choice to work around this flaw. In HoTT where categories have a _classifying space_ of objects we can use the axiom of unique choice. But in a general 1-topos we have neither the axiom of choice nor classifying spaces.
Leopold Schlicht (Feb 20 2022 at 15:41):Thanks for the discussion!
Reid Barton said:
(since "internal category" makes sense also in other categories like Cat or Top where "internal logic" does not).
That's not true. Each finitely complete category has an internal language which is a theory in so-called [[cartesian logic]].
Leopold Schlicht (Feb 20 2022 at 15:47):Each finitely complete category can interpret cartesian logic. And the theory of categories is a cartesian theory.
Reid Barton (Feb 20 2022 at 15:58):For sufficiently flexible meanings of "logic", sure.
Jon Sterling (Feb 20 2022 at 16:06):Zhen Lin Low said:
In any topos – even any cartesian category really – we have the axiom of _unique_ choice, which tells us that any functional relation is realised by a function. Morally, a category with a terminal object, or binary products, or such that some object has a representable functor with a left adjoint, or whatever gadgets that are unique up to unique isomorphism, should be the same thing as a category with chosen gadgets, because the choice is essentially unique! The failure of this is more down to the foundations we choose to work in and the definitions we choose to work with than anything deep. In classical foundations where categories have a _set_ of objects we can (ab)use the axiom of choice to work around this flaw. In HoTT where categories have a _classifying space_ of objects we can use the axiom of unique choice. But in a general 1-topos we have neither the axiom of choice nor classifying spaces.
Indeed, dealing with the differences between internal categories that (e.g.) "have products" vs "have chosen products" is one of the main subtleties --- and it is also a nice motivation for stacks (as opposed to arbitrary fibrations).
Jon Sterling (Feb 20 2022 at 16:12):Reid Barton said:
For sufficiently flexible meanings of "logic", sure.
I think the appropriate meaning of "internal logic" is "whatever structure the subobject preorders are stably closed under". So every kind of category surely has an internal logic, but it may be more or less degenerate depending on how nice the structure of that category is. Or else we would have to come up with some bizarre explanation of why (e.g.) "coherent logic" is a kind of logic but "cartesian logic" and "equational logic" are not!
Reid Barton (Feb 20 2022 at 16:14):All I really meant is that considering internal categories in C doesn't suggest in general that we are also thinking about the internal logic of C, whatever that might mean. For example people who think about double categories aren't thinking about the internal logic of Cat.
Reid Barton (Feb 20 2022 at 16:35):But in fact I was mostly misremembering which thing I was confused about--having a terminal object vs having products.
Reid Barton (Feb 20 2022 at 16:36):Is a stack automatically locally representable (up to equivalence of stacks) by an internal category?
Leopold Schlicht (Feb 20 2022 at 17:27):Zhen Lin Low said:
There is a theorem that says that for every bounded geometric morphism E → S there is an internal site in S and an equivalence (over S) between E and sheaves on that site. (Maybe S needs to have an NNO, I forget. But it does not need to be a Grothendieck topos.)
Thanks, I think that's the theorem discussed at the beginning of this thread! Is there also another motivation in the book for studying internal categories except the applications in relative topos theory? It doesn't look like the book discusses toposes over a base too much.
Jon Sterling (Feb 20 2022 at 17:30):Reid Barton said:
Is a stack automatically locally representable (up to equivalence of stacks) by an internal category?
I don't think so. Stacks in general are the relative version of large categories, and internal categories are the relative version of small categories.
Reid Barton (Feb 20 2022 at 17:32):Ah right, I guess I meant a stack of small categories.
Jon Sterling (Feb 20 2022 at 22:16):So one has to define what a "stack of small categories is", but with the correct definition one does indeed find that the original small stack is equivalent to the externalization of an internal category. You may find it useful to check out the corresponding section of my mini-book on relative category theory: https://www.jonmsterling.com/math/nodes/000N.html
Zhen Lin Low (Feb 20 2022 at 22:18):I don't think that's true. (If it were then I wouldn't have had to write "should be" earlier.) The naïve externalisation of an internal category may fail to be a stack.
Jon Sterling (Feb 20 2022 at 22:19):ohh, that's true... I was thinking only of general fibrations.
Jon Sterling (Feb 20 2022 at 22:21):In this case, the full internal subcategory determined by the stack's generic object is equivalent to the stack but I suppose it need not itself be a stack, unless I am missing something. So this is very close to Reid's request --- it shows that every small stack is weakly equivalent (as a fibration) to the externalization of an internal category.
Jon Sterling (Feb 20 2022 at 22:23):If the base category is a Grothendieck topos, you can take the stack completion of the generic object to obtain a (weakly) equivalent internal category whose externalization is a stack.
Jon Sterling (Feb 20 2022 at 22:25):But let me come back to this another time, I am too sleepy right now and likely to make mistakes. But before I go to bed, let me remark that there is a nice "descent axiom" that you can formulate for the generic object of a small fibration, and it would be nice to check that when this axiom holds, the externalization of the resulting internal category is a stack.
Jon Sterling (Feb 20 2022 at 22:31):Zhen Lin Low said:
In any topos – even any cartesian category really – we have the axiom of _unique_ choice, which tells us that any functional relation is realised by a function. Morally, a category with a terminal object, or binary products, or such that some object has a representable functor with a left adjoint, or whatever gadgets that are unique up to unique isomorphism, should be the same thing as a category with chosen gadgets, because the choice is essentially unique! The failure of this is more down to the foundations we choose to work in and the definitions we choose to work with than anything deep. In classical foundations where categories have a _set_ of objects we can (ab)use the axiom of choice to work around this flaw. In HoTT where categories have a _classifying space_ of objects we can use the axiom of unique choice. But in a general 1-topos we have neither the axiom of choice nor classifying spaces.
By the way, it is not the case that in any cartesian category we have the axiom of unique choice. It is very easy to find examples of cartesian categories in which unique choice fails --- in particular, I believe that any quasitopos that is not a topos would be a counterexample (e.g. a category of assemblies).
Zhen Lin Low (Feb 20 2022 at 22:37):It depends on how you interpret the quantifier. If your interpretation does not make it a theorem that every cartesian category has unique choice then it's probably not a good interpretation.
Jon Sterling (Feb 20 2022 at 23:25):@Zhen Lin Low I am sorry, but this is just not reasonable. It is true that in cartesian logic, $\exists!$ is a quantifier on its own and means the thing you say --- but that is reasonable in the specific case because cartesian logic doesn't have an ordinary existential quantifier. In a logic that has an existential quantifier, it is necessary for $\exists!$ to mean the expanded statement "there exists x such that for all y, x = y" etc.
Why do I insist on this? Because the failure of unique choice in MY sense is an important measure of how bad a category is... There are plenty of "alternative foundations of mathematics" in which unique choice fails, and this failure has very important implications. To trivialize this by just saying "unique choice holds because I defined it to be a tautology" is really not a good idea.
Zhen Lin Low (Feb 20 2022 at 23:27):Are you telling me you can give a total interpretation of in an arbitrary cartesian category?
Jon Sterling (Feb 20 2022 at 23:27):This is rather like saying "Function extensionality holds in every model of intensional type theory, because if I interpret Id(A-> B, f, g) to be anything other than Pi(x:A). Id(B, f(x), f(y)) it is "probably not a good interpretation".
Jon Sterling (Feb 20 2022 at 23:27):Zhen Lin Low said:
Are you telling me you can give a total interpretation of in an arbitrary cartesian category?
No I am saying precisely the opposite.
Jon Sterling (Feb 20 2022 at 23:28):The fact that cartesian categories do not have existential quantifiers means that it is not appropriate to speak of "unique choice" in that context --- unique choice is an important property of the interaction between the actual existential quantifier, exponentials, and equality, which might hold and might fail in a given category. It is similar to balancedness.
Jon Sterling (Feb 20 2022 at 23:29):In general, when a property holds of nearly every category in which it can be stated, you can be sure that you do not have a good definition. That is why I object to speaking of the property you describe as "unique choice".
Zhen Lin Low (Feb 20 2022 at 23:30):If you say it is not appropriate to speak of unique choice in a cartesian category then you are not really in a position to say it fails in a cartesian category either.
Jon Sterling (Feb 20 2022 at 23:30):Good, because I am not saying it fails in a cartesian category.
Zhen Lin Low (Feb 20 2022 at 23:30):"find examples of cartesian categories in which unique choice fails "
Jon Sterling (Feb 20 2022 at 23:31):I meant, "I can find examples of categories that have finite limits AND for which unique choice is a meaningful concept, in which unique choice fails".
Zhen Lin Low (Feb 20 2022 at 23:33):I am not familiar with categories in which can be interpreted and in which the axiom of unique choice does not hold. It holds in any regular category.
Reid Barton (Feb 20 2022 at 23:36):I think there is another variable here, namely whether /images are interpreted as being about subobjects or regular subobjects in categories where those differ.
Jon Sterling (Feb 20 2022 at 23:36):Yes, precisely. Thank you @Reid Barton
Jon Sterling (Feb 20 2022 at 23:37):That is EXACTLY the point of unique choice, and why in a given logic it may succeed or fail.
Reid Barton (Feb 20 2022 at 23:37):For me, just thinking about geometric examples like Top, the regular subobject definition seems more sensible and I think it's the one you have in mind (if I'm not mixed up).
Reid Barton (Feb 20 2022 at 23:39):So I can have a map id : (X, discrete) -> (X, not discrete) which is injective and whose regular image is everything, but it is not an isomorphism.
Zhen Lin Low (Feb 20 2022 at 23:40):I don't think so. I don't know of any serious attempt to interpret using plain epimorphisms. If is a regular or strong epimorphism then the choice of subobjects does not matter, because regular/strong epi + plain mono is already iso.
Jon Sterling (Feb 20 2022 at 23:46):Considring as an example the category of PERs or assemblies on some pca, the correct formulation of unique choice would employ the regular existential quantifier. But I believe we can show that unique choice in this sense doesn't hold.
Zhen Lin Low (Feb 20 2022 at 23:47):I am informed the category of assemblies is regular. So how could it fail? (I'm not talking about the tripos.)
Jon Sterling (Feb 20 2022 at 23:47):Let me come back to this tomorrow when I have slept more. This is subtle and I dont' want to write something down that's wrong.
Zhen Lin Low (Feb 20 2022 at 23:49):I know you can construct hyperdoctrines where the axiom of unique choice fails. I even presented a talk about it once. I'm not talking about them.
Jon Sterling (Feb 21 2022 at 11:23):A reference for my claims is https://ncatlab.org/nlab/show/quasitopos, which mentions the failure of the function comprehension principle (a.k.a. unique choice) in quasitopoi that aren't topoi. However I suspect that what is actually going on here is that we are working from subtle differences in terminology. Roughly the issue is that propositions in a quasitopos must be represented as _strong_ monomorphisms (and I believe in the case of assemblies, you can show that these are exactly the fiberwise codiscrete subobjects, i.e. ones whose realizers carry no useful data). As a result, there is not enough realizability data in the subobject to turn a functional relation into a function. I hope this helps clarify matters, or at least isolate where I am confused.
Zhen Lin Low (Feb 21 2022 at 12:24):I see. In that hyperdoctrine is interpreted by ordinary epimorphisms, and the failure of the axiom of unique choice is indeed down to non-balancedness.Incidentally, for the hyperdoctrine of subspaces (over the category of topological spaces), the functional relations are arbitrary not-necessarily-continuous functions, which I find rather disturbing.
Zhen Lin Low (Feb 21 2022 at 12:33):Ah, I think I remember why I made a fuss about topological quotients in that talk about cartesian hyperdoctrines now...
Leopold Schlicht (Feb 21 2022 at 17:57):Mike Shulman said:
If you care about toposes over a base -- which, for instance, includes all algebraic geometers, since a variety defined "over" a field in the algebraic sense is in particular a topos over in this categorical sense -- then it's often handy to study them in terms of internal sites.
Does that have applications in algebraic geometry, which justify the claim that algebraic geometers are, or should be, interested in topoi over a base?
To me algebraic geometers don't seem to be very interested in topoi:
This I promise: if I use the word “topoi”, you can shoot me.
In SGA 4, p299, it is argued that toposes are the natural objects of study rather than sites. However, I shall not use the word again in these notes.
Morgan Rogers (he/him) (Feb 21 2022 at 18:15):Grothendieck wasn't popular with everyone... but the current generation of algebraic geometers is not predisposed to be against using topos theory explicitly (rather than just working in and over toposes while ignoring them)
Ian Coley (Feb 21 2022 at 18:51):Seems like a pretty obvious case of hyperbole on Vakil's part. I think the spirit of these sentences is that you don't need an exhaustive topos theory to talk thoroughly about sheaves on a (Zariski/Nisnevich/etale) site to an algebraic geometer. They don't need to go into further abstraction just for the sake of it.
Jon Sterling (Feb 21 2022 at 18:59):Nonetheless, I think people who write such things would do well to think a bit about the source of such strong emotions on their part...
I can't imagine saying something like "If you catch me dirtying my hands with an actual prime ideal, you can shoot me!"
Mike Shulman (Feb 21 2022 at 19:32):Jonathan Sterling said:
A reference for my claims is https://ncatlab.org/nlab/show/quasitopos, which mentions the failure of the function comprehension principle (a.k.a. unique choice) in quasitopoi that aren't topoi. However I suspect that what is actually going on here is that we are working from subtle differences in terminology. Roughly the issue is that propositions in a quasitopos must be represented as _strong_ monomorphisms
I agree with all of this except with the "must". I would say that a quasitopos has two different "internal logics" -- a logic of strong monomorphisms and a logic of arbitrary monomorphisms. The logic of arbitrary monos has the advantage of satisfying unique choice, while the logic of strong monos has the advantage of having a subobject classifier.
Mike Shulman (Feb 21 2022 at 19:34):The best thing to do, in my opinion, is embed the quasitopos in a topos, such as [[subsequential spaces]] sitting inside [[Johnstone's topological topos]]. Then the standard internal logic of the topos (using arbitrary monos) has unique choice and a subobject classifier, plus there is generally a lex modality allowing you to recover the original quasitopos and its strong monos as the separated objects -- it's just that the classifier of arbitrary subobjects is not separated.
Mike Shulman (Feb 21 2022 at 19:35):Unfortunately, IIRC it is an open question whether every elementary quasitopos can be so embedded, but every Grothendieck one certainly can be.
Reid Barton (Feb 21 2022 at 19:56):Ian Coley said:
I think the spirit of these sentences is that you don't need an exhaustive topos theory to talk thoroughly about sheaves on a (Zariski/Nisnevich/etale) site to an algebraic geometer.
Also "sheaf" in this context probably means a sheaf of abelian groups (or rings or modules or ...) so, at least in the classical theory, one never really thinks about the topos itself.
Reid Barton (Feb 21 2022 at 19:57):(Also, algebraic geometry is a vast and diverse subject and it's hard to make general statements about it of this type.)
Morgan Rogers (he/him) (Feb 21 2022 at 21:05):That perspective has always seemed strange to me. We deduce so much about categories of groups and various other algebras by considering the underlying set functor; the natural corresponding construction for sheaves of groups is the forgetful functor to the topos of sheaves of sets. Why would people think it's a good idea to ignore that?
John Baez (Feb 21 2022 at 21:15):I don't think lowbrow algebraic geometers exactly "ignore" that a sheaf of R-modules has an underlying sheaf of sets, or "think it's good a idea to ignore that". I think they consider it obvious. I think they find topos theory complicated and don't see enough payoff to want to learn it.
John Baez (Feb 21 2022 at 21:18):For example why does Milne, in his 200-page Lectures on etale cohomology, say
In SGA 4, p299, it is argued that toposes are the natural objects of study rather than sites. However, I shall not use the word again in these notes.
It's a somewhat grumpy sentence! But I imagine he thinks that teaching the students topos theory would mainly slow down the business of getting to the topics he's interested in.
John Baez (Feb 21 2022 at 21:19):Since I like categories, I think it would be great if he were wrong, and that his lectures would be much clearer and more efficient if he used topos theory. But I'm not sure that's true.
Jon Sterling (Feb 21 2022 at 21:22):I think it is quite understandable to not want to take a detour through topoi if you are trying to teach algebraic geometry to students! The situation could be different if students were taught locales and topoi rather than topological spaces in their prerequisites, but that's not the world we live in.
With that said, I think we can do without the "grumpiness". Some of the statements sound like they are holding back an avalanche of malice mixed with feelings of inadequacy --- surely these feelings are ones that we should not externalize onto our students. Far from making the topic more inviting to students who might be worried that they need to learn about topoi, I think it just sounds discouraging to students and fosters disunity. Maybe some old professor had a beef with Grothendieck, but I don't think it is reasonable to pass that on to the youth.
John Baez (Feb 21 2022 at 21:41):I agree that the grumpiness is pointless and silly. I don't ever feel compelled to say stuff like "I shall not use the word again". It's weird.
Jens Hemelaer (Feb 21 2022 at 21:47):John Baez said:
Since I like categories, I think it would be great if he were wrong, and that his lectures would be much clearer and more efficient if he used topos theory. But I'm not sure that's true.
I would find it interesting to know when concepts from algebraic geometry depend only on the underlying (petit étale) toposes. For example, the structure sheaf is probably relevant when classifying line bundles, but not when computing cohomology of a constant group.
This is a bit similar to how some theorems about smooth manifolds are really about the underlying topological space, while for others the choice of smooth structure is relevant.
Reid Barton (Feb 21 2022 at 21:53):for example, the property of being quasiseparated!
Jens Hemelaer (Feb 21 2022 at 21:56):Ah, does that only depend on the underlying petit étale toposes? I didn't know that.
Zhen Lin Low (Feb 21 2022 at 22:14):I'm not sure I believe that. But here's something that definitely only depends on the underlying topos: the étale homotopy type!
Reid Barton (Feb 21 2022 at 22:34):It is usually stated as "intersection of two affine opens is a finite union of affine opens", which appears to depend on the structure sheaf. But a finite union of affine opens is the same as a quasicompact open, and that is the same as a subterminal object that's (quasi)compact in the topos sense.
Zhen Lin Low (Feb 21 2022 at 22:39):Ah, that's nice. I guess that's quasiseparatedness over ? I was thinking more generally of quasiseparated morphisms, which would depend not only on the structure sheaf but also the base scheme.
Reid Barton (Feb 21 2022 at 22:48):Ah yes, I think that's right. Don't know what happens for quasiseparated morphisms, in general.
Reid Barton (Feb 21 2022 at 22:53):Perhaps we would need some way of relativizing notions like "quasicompact" to a base topos... but that seems dangerously close to the original topic of this thread.
Zhen Lin Low (Feb 21 2022 at 22:55):Oh, that can be done, of course.
Jens Hemelaer (Feb 22 2022 at 11:21):A reference is SGA4, Exposé VI, Exemple 1.22.1: there it is remarked that the petit étale topos is quasi-compact (resp. quasi-separated) if and only if the scheme is quasi-compact (resp. quasi-separated). Similarly the induced geometric morphism is quasi-compact (resp. quasi-separated) if and only if the original morphism of schemes is quasi-compact (resp. quasi-separated).
The definitions are as follows:
Leopold Schlicht (Feb 22 2022 at 17:38):John Baez said:
Since I like categories, I think it would be great if he were wrong, and that his lectures would be much clearer and more efficient if he used topos theory. But I'm not sure that's true.
Lurie's opinion is quite interesting:
The theory of (Grothendieck) topoi was originally developed by the Grothendieck school motivated by applications in algebraic geometry. In practice, algebraic geometers who want to understand things like etale cohomology only need a small fraction of the theory that was developed by Grothendieck, such as the notion of a Grothendieck topology and the associated notion of sheaf. Many do not see the need to learn the version topos theory presented in SGA, and I suspect that the number who are interested in the subsequently developed theory of elementary topoi is vanishingly small. I do not see this as a failing of the algebraic geometry community: the notion of Grothendieck topology was quite useful to them, so they internalized it. Related ideas may be interesting for other reasons, but have had limited relevance to algebraic geometry.
So I don't think topos theory has any real applications in algebraic geometry, at least until somebody gives me one.
Reid Barton (Feb 22 2022 at 18:34):I would be very surprised if there was any application of elementary topos theory to algebraic geometry. (I don't really think of an elementary topos and a Grothendieck topos as the same sort of thing at all--the morphisms are different!)
Morgan Rogers (he/him) (Feb 22 2022 at 18:35):Since I like categories, I think it would be great if he were wrong, and that his lectures would be much clearer and more efficient if he used topos theory. But I'm not sure that's true.
If I ever have to teach algebraic geometry, I'll have a shot at writing the course without avoiding toposes and let you know how it goes!
Reid Barton (Feb 22 2022 at 18:38):Really I think the best "application" of topos theory to algebraic geometry is to understand it "from the outside"--to understand what makes it work, and to transfer ideas to and from other subjects. Where are all these strange definitions coming from: Zariski spectrum, quasicoherent sheaf, sheaf cohomology, ...?
The first and best example is the construction of the spectrum of a ring--why should it be a topological space whose points are prime ideals, and where does this sheaf of functions come from? How come we have to define the sheaf first on a base of distinguished open sets and then use some other construction to extend to arbitrary ones?
But the ringed locale can be written down in one line: its objects are determined by localizations of the form and the structure sheaf assigns to the ring... drumroll... !
Reid Barton (Feb 22 2022 at 18:40):But obviously it's sensible that in a course on algebraic geometry you want to see the definition of scheme without having to explain first what a locale (or topos, ...) is. And algebraic geometry uses a bunch of things just once like this, so that if you're only interested in learning algebraic geometry, you don't derive any particular extra power from seeing the general picture.
Jens Hemelaer (Feb 22 2022 at 19:09):Topos theory was originally developed to introduce étale cohomology, but it seems that nowadays étale cohomology or even sheaf cohomology is no longer seen as part of topos theory by algebraic geometers. As soon as you ignore étale cohomology (and the étale fundamental group), I think it becomes harder to come up with applications of toposes in algebraic geometry.
Jens Hemelaer (Feb 22 2022 at 19:10):Maybe the other way around condensed sets can be seen as an application of algebraic geometry to topos theory.
John Baez (Feb 22 2022 at 19:31):it seems that nowadays étale cohomology or even sheaf cohomology is no longer seen as part of topos theory by algebraic geometers...
What do topos theorists think about this? I'm not sure I care what algebraic geometers consider to be part of topos theory, since most of them don't care much about topos theory.
John Baez (Feb 22 2022 at 19:32):(They may just feel that anything they do is not part of topos theory.)
Jens Hemelaer (Feb 22 2022 at 20:02):I'm not sure, but my guess is that many topos theorists view sheaf cohomology as being a part of topos theory. For example, Caramello organized a course joint with Lafforgue on cohomology of toposes, and this included the typical settings from algebraic geometry. In Johnstone's "Sketches of an Elephant", cohomology isn't mentioned so much, but this is only because it is postponed to a yet-to-appear volume (there is a chapter on cohomology in his earlier book "Topos Theory"). On the other hand, there is no chapter on cohomology in the book by Mac Lane and Moerdijk.
Leopold Schlicht (Feb 22 2022 at 20:10):Jens Hemelaer said:
On the other hand, there is no chapter on cohomology in the book by Mac Lane and Moerdijk.
In the "Epilogue" they write "we have omitted sheaf cohomology - but with great regrets". :grinning_face_with_smiling_eyes:
Jens Hemelaer (Feb 22 2022 at 20:11):I didn't notice that :big_smile:
David Michael Roberts (Feb 22 2022 at 20:30):Leopold Schlicht said:
So I don't think topos theory has any real applications in algebraic geometry, at least until somebody gives me one.
Ingo Blechschmidt proved Grothendieck's generic freeness lemma in a very short way using topos-theoretic techniques. I'm not sure that counts as a real application, but I would be surprised if there weren't more proofs like his of known results.
John Baez (Feb 22 2022 at 20:34):I want to see more topos theorists re-enter algebraic geometry and try to make progress on some of the huge questions left open by Grothendieck, like the standard conjectures, or maybe something altogether new, like ideas surrounding "the field with one element". Of course some people are trying to study the latter using topos theory. And of course it's easy for me to want this, not so easy to actually do it! :upside_down:
John Baez (Feb 22 2022 at 20:36):I'm not really expecting miracles; I just like it when different branches of math stay interacting.
Fawzi Hreiki (Feb 22 2022 at 21:37):Speaking of applications of topos theory to AG, I've recently come across a scan of A. Kock's 'Topos Theoretic Methods in Geometry'.
John Baez (Feb 22 2022 at 21:42):Interesting! Knowing him, that could be about synthetic differential geometry... which of course has some overlap with algebraic geometry, but has a different focus.
Fawzi Hreiki (Feb 22 2022 at 22:00):It's a collection of papers from different authors (Lawvere, Wraith, etc..). There are some SDG papers by Kock in there, but there are also papers on AG such as one on subtoposes of the classifying topos of rings, or on Grothendieck topologies for real algebraic geometry.
Zhen Lin Low (Feb 22 2022 at 22:30):I don't think even Grothendieck envisioned solving the standard conjectures using topos theory. They are about quite concrete objects, even in the context of schemes rather than locally ringed toposes or whatever.
Fawzi Hreiki (Feb 22 2022 at 22:36):Of course, topos theory is far too general to actually 'solve' problems in algebraic geometry, the same way category theory does not 'solve' any concrete problems in algebraic topology. That doesn't mean that its not a useful language and meta-framework for thinking about the subject.
Zhen Lin Low (Feb 22 2022 at 22:41):OK. But if that's the bar then algebraic geometers have already adopted topos theory. Some – very few – have even found applications of the theorem that every Grothendieck topos can be covered by a localic boolean one.
Morgan Rogers (he/him) (Feb 22 2022 at 22:45):If someone were to solve the Hodge Conjecture using topos theory, would that be sufficient to prove its relevance?
Morgan Rogers (he/him) (Feb 22 2022 at 22:46):(Asking for a friend)
John Baez (Feb 22 2022 at 22:47):Someone might have fun arguing about whether category theory 'solves' problems in algebraic topology, but maybe it's better to say that a lot of algebraic topology would be harder to do without results about abelian categories, model categories and the like.
John Baez (Feb 22 2022 at 22:48):Morgan Rogers (he/him) said:
If someone were to solve the Hodge Conjecture using topos theory, would that be sufficient to prove its relevance?
It depends on whether I could figure out how to rewrite the solution in a way that never mentioned topos theory. :upside_down:
John Baez (Feb 22 2022 at 22:48):(Just kidding, but this seems to be one standard attitude.)
Zhen Lin Low (Feb 22 2022 at 22:48):Considering that Wiles's proof of FLT involved high powered stuff and ended up inviting scepticism because of it... Or Mochizuki now, for that matter.
Leopold Schlicht (Feb 23 2022 at 12:18):Reid Barton said:
Really I think the best "application" of topos theory to algebraic geometry is to understand it "from the outside"--to understand what makes it work, and to transfer ideas to and from other subjects. Where are all these strange definitions coming from: Zariski spectrum, quasicoherent sheaf, sheaf cohomology, ...?
Where can I read more about how topos theory motivates some of the definitions in algebraic geometry?
Reid Barton (Feb 23 2022 at 13:34):Leopold Schlicht said:
Reid Barton said:
Really I think the best "application" of topos theory to algebraic geometry is to understand it "from the outside"--to understand what makes it work, and to transfer ideas to and from other subjects. Where are all these strange definitions coming from: Zariski spectrum, quasicoherent sheaf, sheaf cohomology, ...?
Where can I read more about how topos theory motivates some of the definitions in algebraic geometry?
Good question and I don't have a good answer for you. I learned this stuff mainly from Lurie's DAG V and in bits and pieces from the nLab.
Morgan Rogers (he/him) (Feb 23 2022 at 13:45):Leopold Schlicht said:
Reid Barton said:
Really I think the best "application" of topos theory to algebraic geometry is to understand it "from the outside"--to understand what makes it work, and to transfer ideas to and from other subjects. Where are all these strange definitions coming from: Zariski spectrum, quasicoherent sheaf, sheaf cohomology, ...?
Where can I read more about how topos theory motivates some of the definitions in algebraic geometry?
I'll say SGA IV before someone else does.
Leopold Schlicht (Feb 23 2022 at 14:39):Thanks! By the way, is everything in DAG n contained in the book "Spectral algebraic geometry" by Lurie?
Reid Barton (Feb 23 2022 at 15:49):I think that is the eventual plan but I don't know whether it is the case currently
Leopold Schlicht (Feb 23 2022 at 15:56):Thanks!
Leopold Schlicht (Feb 23 2022 at 18:59):Morgan Rogers (he/him) said:
Leopold Schlicht said:
Reid Barton said:
Really I think the best "application" of topos theory to algebraic geometry is to understand it "from the outside"--to understand what makes it work, and to transfer ideas to and from other subjects. Where are all these strange definitions coming from: Zariski spectrum, quasicoherent sheaf, sheaf cohomology, ...?
Where can I read more about how topos theory motivates some of the definitions in algebraic geometry?
I'll say SGA IV before someone else does.
Which parts of SGA 4 in particular? Exposé 4 and 5 don't talk about schemes much. Exposé 7 defines the étale site, but I can't find there many motivating explanations of the kind I asked about.
Morgan Rogers (he/him) (Feb 23 2022 at 19:18):I would have to have read it recently to answer that. Perhaps @Mateo Carmona can refer you to something that Grothendieck wrote that can provide more insight than SGA4 into the interplay between definitions of toposes and of structures in algebraic geometry?
Fawzi Hreiki (Feb 23 2022 at 22:23):The pure topos theory is mostly part 1 of SGA4. Part 2 deals with descent theory and the etale topology for schemes, while part 3 deals with etale cohomology for schemes.
Mateo Carmona (Feb 23 2022 at 23:02):Thanks, a lot of interesting questions have been asked before on this thread. Let me focus on the interplay.
First, we need to clarify that this interplay is far from being simple. There are various sections of Recoltes et Semailles that intend to answer that.
There is nevertheless a particular reference that tries to answer it
UTILISATION DES CATÉGORIES EN GÉOMÉTRIE ALGÉBRIQUE par Jean GIRAUD scan (you can see also Chapter VII. "Examples tirés de la Géométrie Algébrique" of Giraud's thesis)
You can see also How Grothendieck Simplified
Algebraic Geometry
"Toposes are less popular than schemes or sites in geometry today. Deligne expresses his view with care: “The tool of topos theory permitted the construction of étale cohomology” [10, p. 15]. Yet, once constructed, this cohomology is “so close to classical intuition” that for most purposes one needs only some ordinary topology plus “a little faith/un peu de foi” [9, p. 5]. Grothendieck would “advise the reader nonetheless to learn the topos language which furnishes an extremely convenient unifying principle” [5, p. VII]."
And this is the point I would like to emphasize. Instead of the question of how we can use them in algebraic geometry, we should ask what is topos theory trying to unify (as developed by Grothendieck).
"Parmi ces thèmes, le plus vaste par sa portée me paraît être celui des topos, qui fournit l’idée d’une synthèse de la géométrie algébrique, de la topologie et de l’arithmétique."
Of course, an answer about this interplay would need a lot more detail, even the interplay between sheaves and algebraic geometry is already a very rich one, but nevertheless... you can see, for example, the thesis of Mme M Reynaud or Jouanolou, SGA 7...
Grothendieck used "the notion of a topos and a map of topoi, as an ideal means and guide to put geometrical and topological significance into purely algebraic situations." Remember how all those theories began. At the beginning (Weil conjectures), what was needed was a language that would eventually unify the methods used with continuous coefficients in discrete ones.
The fact, for example, that one can associate a topos (and topological invariants) to an arbitrary category was exploited in various directions by him. And also, the fact that topos constitute a 2-category and not an ordinary category (like topological spaces) would open new doors in topology (remember, this was at the beginning of the 60s).
One can ask, for example, higher category theory is better suited than topos theory in the things algebraic geometers like..? I think this is not the right question to ask. It is enough to try to understand.
"Ce qui fait la qualité de l’inventivité et de l’imagination du chercheur, c’est la qualité de son attention, à l’écoute de la voix des choses."
Sorry if this goes in another direction than simply citing some references. But maybe helps someone in something.