Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 13th 2017

    This MO question seemed interesting to me, and I wondered if anyone here had a reaction.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 13th 2017

    I pointed out our page dependent linear type theory in a comment there.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2017

    We even have a page stable homotopy type.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2017
    • (edited Oct 13th 2017)

    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

    1. there is a pointed type X *X_\ast

    2. the morphism ΣΩX X \Sigma \Omega X_\star \to X_\star 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

    1. the morphism ΣΩ(X S )X S \Sigma \Omega(X_\star^{S_\star}) \to X_\star^{S_\star} is an equivalence, for finite pointed powers.

    If one could add the infinite set of these axioms, that would be Goodwillie’s localization for the tangent \infty-topos (here).

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 13th 2017

    Ok, I’ve passed that on. You may be needed to field questions on it.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2017

    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 \infty-topos (unless I am missing a comment of his).

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2017

    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.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2017
    • (edited Oct 13th 2017)

    I had advertized the tangent \infty-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 \infty-category THT \mathbf{H} of an \infty-topos H\mathbf{H} is itself an \infty-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.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeOct 13th 2017

    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. Although I don’t remember whether Voevodsky was present.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 13th 2017

    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.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeOct 13th 2017
    • (edited Oct 13th 2017)

    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.

  1. 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 (,1)(\infty,1)-topos of the (,1)(\infty,1)-topos of \infty-groupoids?

    • CommentRowNumber13.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 13th 2017
    • (edited Oct 13th 2017)

    Re #6, he wrote

    Although maybe there is something to work on regarding the fact that the category of parametrized spectra is an ∞ -topos.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 13th 2017

    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.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeOct 13th 2017

    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.

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 14th 2017

    The link to an anchor in Example 3.6 is broken.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeOct 14th 2017

    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.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeOct 16th 2017

    Okay, thanks!

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeOct 16th 2017

    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 (,1)(\infty,1)-topos of the (,1)(\infty,1)-topos of \infty-groupoids?

    That’s plain parameterized spectra.

  2. Thanks Urs! I think what I was missing is that the tangent (,1)(\infty,1)-topos consists of the parametrised spectra for all XX, not any fixed XX, if I understand correctly?

    I would like to arrive at some intuition as to why this is an (,1)(\infty,1)-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 (,1)(\infty,1)-category of spectra, and with sets in place of homotopy types? Is the point that one would get a (2,1)(2,1)-topos, not a 1-topos in this case, i.e. is it only because we are working at the \infty-level that things ’stabilise’? Or if we actually get a 1-topos, could someone give some explanation as to why?

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeOct 16th 2017

    I think what I was missing is that the tangent (,1)(\infty,1)-topos consists of the parametrised spectra for all XX, not any fixed XX, if I understand correctly?

    Yes, the \infty-groupoids XX are the “points” in \inftyGrpd and then the parameterized spectra over this fixed XX are the “tangents” at that point.

    I would like to arrive at some intuition as to why this is an (,1)(\infty,1)-topos.

    The proof is really easy and might provide sufficient intuition already: 1) If we don’t fix the base XX, then parameterized pre-spectra form a presheaf category. 2) The operation of spectrification turning these into genuine parameterized spectra is a filtered \infty-colimit, hence commutes with finite \infty-limits, hence is a left exact localization. Now Grothendieck \infty-topoi are precisely the (accessible) left exact localizations of presheaf \infty-categories.

  3. 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 (,1)(\infty,1)-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.

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeOct 16th 2017

    reconcile this story with that of parametrised spectra defined as (,1)(\infty,1)-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?

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 16th 2017

    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”.

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeOct 16th 2017

    It’s for emphasis.

    • CommentRowNumber26.
    • CommentAuthorMike Shulman
    • CommentTimeOct 16th 2017

    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.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeOct 16th 2017

    Richard, why do you think size has anything to do with it? A single parametrized spectrum is a small object, just like a single \infty-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 \infty-case is different.

    • CommentRowNumber28.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 16th 2017
    • (edited Oct 16th 2017)

    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 XX. A first guess might be something like the colimit of the functor Grpd(,1)Cat\infty-\mathsf{Grpd} \rightarrow (\infty,1)-\mathsf{Cat} which sends XX to Fun(X,Spectra)\mathsf{Fun}(X, \mathsf{Spectra}). 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 (,1)(\infty,1)-category of large (,1)(\infty,1)-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 (,1)(\infty,1)-topos in the very large world, it cannot be equivalent to a (,1)(\infty,1)-topos in the large, that is to say usual, world (i.e. small \infty-groupoid of arrows), which would seem to contradict the ’easy’ construction, which is evidently an (,1)(\infty,1)-topos in the latter sense.

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeOct 16th 2017

    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.

    • CommentRowNumber30.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 17th 2017
    • (edited Oct 17th 2017)

    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 Grpd(,1)Cat\infty-\mathsf{Grpd} \rightarrow (\infty,1)-\mathsf{Cat}, the (,1)(\infty,1)-category on the right is that of large (,1)(\infty,1)-categories here (since Spectra\mathsf{Spectra}, and hence Fun(X,Spectra)\mathsf{Fun}(X, \mathsf{Spectra}), is large). That is to say, the (,1)Cat(\infty,1)-\mathsf{Cat} 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 (,1)(\infty,1)-category of very large (,1)(\infty,1)-categories! That means, I think, that the observation you made only shows that we have a very large category that is locally large.

    • CommentRowNumber31.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 17th 2017
    • (edited Oct 17th 2017)

    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.

    • CommentRowNumber32.
    • CommentAuthorMike Shulman
    • CommentTimeOct 17th 2017

    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.

  4. Hmm…maybe you interpreted that sentence differently to how I intended. What I meant was that the arrow Grpd(,1)Cat\infty-\mathsf{Grpd} \rightarrow (\infty,1)-\mathsf{Cat} lives in the very, very large category of very large categories. This point is completely academic, of course…

    • CommentRowNumber34.
    • CommentAuthorMike Shulman
    • CommentTimeOct 18th 2017

    Generally the colimit of a diagram F:CDF : C \to D is said to be “in” the category DD, not in the category of categories in which FF lives.

  5. 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 SetCAT\mathsf{Set} \rightarrow \mathsf{CAT}, sending XX to Fun(X,Ab)\mathsf{Fun}(X, \mathsf{Ab}), viewing XX 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 \infty-setting is that an \infty-groupoid has as many levels of structure as an (,1)(\infty,1)-category, so one doesn’t need to do the ’view XX as a discrete category part’. But I’m not sure whether that is a fundamental part of the story.

    • CommentRowNumber36.
    • CommentAuthorMike Shulman
    • CommentTimeOct 18th 2017

    My intuition, such as it is, is more that an \infty-groupoid already has “algebraic” structure in its higher compositions, unlike a set.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeOct 20th 2017

    I would like to see an explanation for why Fam(Ab)Fam(Ab) fails to be a topos, so we can see why it doesn’t apply to parametrized spectra.

    • CommentRowNumber38.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 20th 2017

    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?

    • CommentRowNumber39.
    • CommentAuthorRichard Williamson
    • CommentTimeOct 21st 2017
    • (edited Oct 21st 2017)

    It might be interesting to see if we can find a limit sketch whose category of models is Fam(Ab)\mathsf{Fam}(\mathsf{Ab}). The objects of the latter can be thought of, if I am not mistaken, as infinite tuples (X,A 1,A 2,)(X, A_{1}, A_{2}, \ldots), where XX is a set and, for every ii, A iA_{i} is an abelian group, with the property that A i=0A_{i} = 0 when i>ni \gt n, where nn is the number of elements of XX. 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 A i=0A_{i} = 0 when i>ni \gt n, where nn is the number of elements of XX, in a limit sketch. It does not seem very natural to me, but maybe there is some trick.

  6. (I was restricting to finite sets in #39, but this case should still be instructive).

    • CommentRowNumber41.
    • CommentAuthorMike Shulman
    • CommentTimeOct 21st 2017

    It’s quite easy to express Fam(Ab)Fam(Ab) 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.).

  7. That’s a nice idea, Mike, thanks!

    So then at least we know that Fam(Ab)\mathsf{Fam}(\mathsf{Ab}) 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 Fam(Set)\mathsf{Fam}(\mathsf{Set}) and abelianise? Is it any more obvious whether Fam(Set)\mathsf{Fam}(\mathsf{Set}) 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.

    • CommentRowNumber43.
    • CommentAuthorMike Shulman
    • CommentTimeOct 25th 2017

    Fam(Set)Fam(Set) is a presheaf category, in fact it’s equivalent to the Sierpinski topos Set Set^{\to}.

    And of course, it wouldn’t help to prove that the localization of Fam(Ab)Fam(Ab) 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.

  8. Somehow it seems to me that since stabilisation has the necessary properties to allow us to demonstrate left exactness in the (,1)(\infty,1)-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.

    • CommentRowNumber45.
    • CommentAuthorMike Shulman
    • CommentTimeOct 26th 2017

    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 \infty-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.