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.
This MO question seemed interesting to me, and I wondered if anyone here had a reaction.
I pointed out our page dependent linear type theory in a comment there.
We even have a page stable homotopy type.
I am busy in a talk now. But if anyone has a second, Simon Henry’s comments should be replied to by pointing out that while the category of spectra is not univalent, that of parameteritzed spectra is. In other words, an idea to go about “stable HoTT” is to try to add an axiom that makes it the internal language for tangent (infinity,1)-toposes. That axiom should be
there is a pointed type
the morphism is an equivalence
So far this makes the ambient category “linear” in the terminology of Schwede’s old article on parameterized spectra. One could now continue to add the axioms
If one could add the infinite set of these axioms, that would be Goodwillie’s localization for the tangent -topos (here).
Ok, I’ve passed that on. You may be needed to field questions on it.
Thanks!
Maybe you could change the line
As Simon pointed out in his comment, the category of parametrized spectra is an ∞-topos
because it seems instead that this is the information that Simon was lacking. What he pointed out is just that non-parameterized spectra is not an -topos (unless I am missing a comment of his).
By the way, “Schwede’s old paper on parameterized spectra” which I mentioned is this here, where the concept of “linear” (as opposed to fully stable) is def. 2.2.1.
I had advertized the tangent -topos as the route for HoTT to go stable in May 2014 at the IHP trimester on Semantics of proofs and certified mathematics –Workshop 1: Formalization of Mathematics, in my talk Differential generalized cohomology in Cohesive homotopy type theory (schreiber).
Unfortunately, when I came to state, about 15 minutes into the talk, what is prop. 2.5 in the talk notes (pdf), namely the statement that the tangent -category of an -topos is itself an -topos, Vladimir Voevodsky started to interrupt and to question this statement. Nobody would stop him – it turned out that he himself was the chair and it seemed everyone except me was scared to argue with him. Had I not known that he was a famous homotopy theorists, I would not have gathered from this event.
Already at the IAS HoTT special year in 2012-2013, Joyal gave a talk in which he mentioned that parametrized spectra form an -topos. Although I don’t remember whether Voevodsky was present.
Actually, now that I look at dependent linear type theory, I think that sections 3 and 4 of it are on the wrong page. They are not about any kind of type theory, but about the categories that are conjectured to be semantics for DLTT. They should be moved to a page like indexed monoidal (∞,1)-category, and the page dependent linear type theory should just link to that page as the conjectural semantics for DLTT.
Already at the IAS HoTT special year in 2012-2013, Joyal gave a talk in which he mentioned that parametrized spectra form an ∞\infty-topos.
Yes, that’s where I got it from. I was citing that in the talk.
They are not about any kind of type theory, but about the categories that are conjectured to be semantics for DLTT.
Yes!
They should be moved
If you insist on that, then it might be easier to just rename the entry, and either have “dependent linear type theory” be a redirect, or else make it a stub entry pointing to the other one.
A simple question in passing, which I could not find an answer to after a quick glance at tangent (infinity,1)-toposes: what is the tangent -topos of the -topos of -groupoids?
Re #6, he wrote
Although maybe there is something to work on regarding the fact that the category of parametrized spectra is an ∞ -topos.
I do insist, and I’ll do the move when I have time. Pages on type theory should be about type theory. It wouldn’t make sense for the page string diagram to have a long discussion about structures that can be defined in a monoidal category, on the basis that theorems about such structures could be proven using string diagrams; the proper place for the that would be at monoidal category or at individual pages on the individual structures. It’s a little different because the syntax of type theory is powerful enough that you can actually define things entirely inside it (unlike the syntax of string diagrams), but unless such definitions are actually being written in type theory, they don’t belong on a page about type theory. Moreover, having such an extensive page called “dependent linear type theory” could create the wrong impression in the reader that such a type theory exists and is well-studied.
Okay, I have split the page into indexed monoidal (infinity,1)-category, with all the purely category-theoretic stuff, and dependent linear type theory with the little that is actually known about the type theory itself. From the former I also added the Beck-Chevalley condition to the definition, since it seems to be satisfied and needed in all cases, and removed the disparagement of nonlinear examples.
The link to an anchor in Example 3.6 is broken.
Thanks, fixed. That was because I changed some anchor names to remove references to linear type theory from statements that are only about indexed monoidal categories and missed changing that link. I would have desisted from changing anchors to avoid link-breakage, but unfortunately anchored links from other pages are going to break anyway because of the move from dependent linear type theory to indexed monoidal (infinity,1)-category, so I figured I might as well make the anchor names correct too.
Okay, thanks!
A simple question in passing, which I could not find an answer to after a quick glance at tangent (infinity,1)-toposes: what is the tangent -topos of the -topos of -groupoids?
That’s plain parameterized spectra.
Thanks Urs! I think what I was missing is that the tangent -topos consists of the parametrised spectra for all , not any fixed , if I understand correctly?
I would like to arrive at some intuition as to why this is an -topos. Firstly, there is a minor question of size. I suppose by some tricks (e.g. not using in fact all homotopy types) one can get it to live in the same universe as one started with, or else one can accept that it lives in a different universe and adjust other things accordingly, but it seems to me that some care is needed one way or the other here.
More significantly, what happens if I work in ordinary category theory, i.e. with the category of abelian groups instead of the -category of spectra, and with sets in place of homotopy types? Is the point that one would get a -topos, not a 1-topos in this case, i.e. is it only because we are working at the -level that things ’stabilise’? Or if we actually get a 1-topos, could someone give some explanation as to why?
I think what I was missing is that the tangent -topos consists of the parametrised spectra for all , not any fixed , if I understand correctly?
Yes, the -groupoids are the “points” in Grpd and then the parameterized spectra over this fixed are the “tangents” at that point.
I would like to arrive at some intuition as to why this is an -topos.
The proof is really easy and might provide sufficient intuition already: 1) If we don’t fix the base , then parameterized pre-spectra form a presheaf category. 2) The operation of spectrification turning these into genuine parameterized spectra is a filtered -colimit, hence commutes with finite -limits, hence is a left exact localization. Now Grothendieck -topoi are precisely the (accessible) left exact localizations of presheaf -categories.
Thank you! I follow that argument certainly, but it is not completely clear to me how to reconcile this story with that of parametrised spectra defined as -functors from a homotopy type to spectra.
If somone would be able to address my two questions from #20 directly, I think that would help me a lot.
reconcile this story with that of parametrised spectra defined as -functors from a homotopy type to spectra.
That equivalence was proven in Ando-Blumberg-Gepner 11
If someone would be able to address my two questions from #20 directly, I think that would help me a lot.
Hopefully somebody else here with more time will look into this, but I am thinking that at least it should be easy to see why the easy proof for parameterized spectra outlined in #21 does not generalize to parameterized abelian groups: these are not given by applying a filtered colimit to some kind or presheaf representation of “pre-groups”. Are they?
At the new entry dependent linear type theory, isn’t the ’dependent’ in
Dependent linear homotopy type theory
redundant? We don’t say “dependent homotopy type theory”.
It’s for emphasis.
I.e. to make it clear that “homotopy” is something being added to the previously mentioned “dependent linear type theory”, not a replacement for some part of it.
Richard, why do you think size has anything to do with it? A single parametrized spectrum is a small object, just like a single -groupoid, so the category of such is large and locally small just like any other.
As for your second question, I’m still looking for a good answer to that one. I mean, Urs’s answer is technically correct, but it doesn’t really provide me with a good intuition for why the -case is different.
Thanks to you both for your replies! I look forward to any further thoughts.
It could be that I’ve got something mixed up with regard to size, but I was thinking along the following lines. Suppose that we wish to formally express the idea that we are varying over . A first guess might be something like the colimit of the functor which sends to . Possibly there should be an ’oplax’ thrown in here somewhere, so that we have something like the Grothendieck construction. This colimit lives in the very large -category of large -categories, and I was thinking that it surely would only be locally small in the very large world, not in the large world, And if it is an -topos in the very large world, it cannot be equivalent to a -topos in the large, that is to say usual, world (i.e. small -groupoid of arrows), which would seem to contradict the ’easy’ construction, which is evidently an -topos in the latter sense.
Ah, I see what you were thinking. In general, yes, a colimit of a large diagram of large locally-small categories will no longer be locally-small. However, the oplaxness saves us in this case: the oplax colimit / Grothendieck construction of a large locally-small diagram of large locally-small categories is again locally-small, because of the explicit description of the homs in the Grothendieck construction in terms of homs in the base and the fibers. That’s kind of interesting, I hadn’t noticed that explicitly before; we should add a note about it to Grothendieck construction.
Thanks for this and for adding the note!
Just one more thing on this. I hope that I’m not muddling things up, just let me know if so. I think that I got the sizes involved slightly wrong the first time around. In the functor , the -category on the right is that of large -categories here (since , and hence , is large). That is to say, the itself that we are working with here is already very large. That means that the oplax colimit is actually taking place in the very, very large -category of very large -categories! That means, I think, that the observation you made only shows that we have a very large category that is locally large.
Upon further thought, I think the sizes in #30 are correct, but that the last sentence is incorrect; I think your observation does indeed show that we have a locally small category in this case.
I think the penultimate sentence of #30 is also wrong: the colimit is taking place in the very large category of large ones, hence is automatically itself large; the only question is about local smallness.
Hmm…maybe you interpreted that sentence differently to how I intended. What I meant was that the arrow lives in the very, very large category of very large categories. This point is completely academic, of course…
Generally the colimit of a diagram is said to be “in” the category , not in the category of categories in which lives.
Yes, no criticism was intended, I just wished to clarify what I meant. Sorry the confusion, and thanks for your answers!
I remain interested in the question about what happens in the non-infinity setting, should anybody reach any enlightenment upon that. I am actually not completely sure how to formulate things precisely for sets and abelian groups. The analogous functor would probably be , sending to , viewing as a discrete category. If we apply the Grothendieck construction to this, is it clear that we do not have a topos?
I guess what is special about the -setting is that an -groupoid has as many levels of structure as an -category, so one doesn’t need to do the ’view as a discrete category part’. But I’m not sure whether that is a fundamental part of the story.
My intuition, such as it is, is more that an -groupoid already has “algebraic” structure in its higher compositions, unlike a set.
I would like to see an explanation for why fails to be a topos, so we can see why it doesn’t apply to parametrized spectra.
Is there an AT category-like structure on Fam(Ab) such that the exactness properties force the A side (or an analogue) to be dominant?
It might be interesting to see if we can find a limit sketch whose category of models is . The objects of the latter can be thought of, if I am not mistaken, as infinite tuples , where is a set and, for every , is an abelian group, with the property that when , where is the number of elements of . The arrows are then just levelwise, I believe. This kind of description looks quite promising, but the question is whether we can express the condition when , where is the number of elements of , in a limit sketch. It does not seem very natural to me, but maybe there is some trick.
(I was restricting to finite sets in #39, but this case should still be instructive).
It’s quite easy to express as the models of a limit sketch: write down the sketch for abelian groups, but with a terminal object adjoined and included as part of all the limit cones (so that products become pullbacks over it, etc.).
That’s a nice idea, Mike, thanks!
So then at least we know that is a localisation of a presheaf category, we just do not know if that reflection is left exact. The obvious question is whether we can identify this presheaf category, and describe the localisation more explicitly?
Can we simply look at and abelianise? Is it any more obvious whether is a presheaf category or a localisation of one?
Don’t have time to think about this properly myself just now, am just throwing out the questions in case they suggest some way to proceed to someone.
is a presheaf category, in fact it’s equivalent to the Sierpinski topos .
And of course, it wouldn’t help to prove that the localization of as models of that sketch isn’t left exact (which is what I would expect to be the case), since a non-left-exact localization of a topos can still happen to be a topos.
Somehow it seems to me that since stabilisation has the necessary properties to allow us to demonstrate left exactness in the -setting, so should abelianisation have the necessary properties to allow us to demonstrate left exactness in the 1-categorical setting. Again, I have not thought properly about this statement at all due to lack of time, but I would expect something along these lines to hold.
The difference between abelianization and stabilization does seem to be the crux of the matter. In the stable situation, we can stabilize by localizing a prespectrum object so as to become a spectrum; this works because of the “internal algebraic structure” of an -groupoid that is lacked by a set, so that to abelianize a set we have to instead add the addition operation and so on. The resulting localizations of presheaf categories are very different, so it makes sense to me that one of them would be left exact and not the other.
1 to 45 of 45