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 beauty bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology definitions deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality education elliptic-cohomology enriched fibration foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory infinity integration integration-theory k-theory kan lie lie-theory limit limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monad monoidal monoidal-category-theory morphism motives motivic-cohomology nonassociative noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pasting philosophy physics planar 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 simplicial space spin-geometry stable-homotopy-theory stack string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory 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.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 15th 2018

    I added the reference

    diff, v26, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 15th 2018

    Rasekh speaks of a future goal

    Blakers-Massey: One of the classical results of algebraic topology is the Blakers-Massey theorem. We already know it holds in a higher topos [Re05]. Thus the next natural question is to show it also holds in an EHT, using the fact that the proof mainly relies on the descent condition

    But we know this about the Blakers-Massey theorem already, no? It says thre about the HoTT proof that

    This translates to an internal language proof of Blakers-Massey valid in all (∞,1)-toposes (including elementary (∞,1)-toposes). Unwinding of the fully formal HoTT proof to ordinary mathematical language is, for the special case of the Freudenthal suspension theorem, in (Rezk 14).

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 16th 2018

    We may as well carry on discussion of this topic here, rather than the parallel thread, since the nLab software sends updates to elementary (infinity,1)-topos here.

    With the definition settling down :), perhaps this is a good moment to revisit Joyal-Kripke semantics for HoTT. It was raised back here as something needing some loving attention with regard to n-types cover.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMay 16th 2018

    I’m still trying to finish up the semester, haven’t had a chance to really read Rasekh’s paper yet. Re #2, I guess the point is that Rezk’s manual unwinding should apply essentially verbatim in the elementary case, presuming that it only uses descent rather than any Grothendiecky stuff? (Otherwise, the claim would depend on the conjecture that HoTT is an internal language for (elementary) (,1)(\infty,1)-toposes.)

    • CommentRowNumber5.
    • CommentAuthornimarasekh
    • CommentTimeMay 16th 2018
    I might be able to explain where the Blakers-Massey came from. There is a good chance that I am over-complicating things and everything has already been done, but here is my perspective: There is already a proof in HoTT. That proof was translated to spaces by Charles Rezk. He also proves that it holds for a higher topos (using model categories). Ideally this means that the proof will also hold for an elementary higher topos, however, I don't know if that directly follows. In particular the arguments by Rezk are focused on spaces. As Mike pointed out the underlying idea should be that everything just depends on descent and other topos theoretic properties, but I personally think this is worth analyzing.

    There is also a second motivation I had in mind, which might be less clear from the HoTT perspective. I am hoping to convince more "traditional" algebraic topologists to consider topos theory/higher cats/HoTT. That is also why I called the section algebraic topology. It's interesting how results that are obvious to the HoTT community are surprising to many algebraic topologists. From that perspective having concrete proofs in the language of higher categories seems to be a benefit.
    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 17th 2018

    Thanks for joining in the conversation, Nima. Of course, do feel free to add to the entry elementary (infinity,1)-topos.

    results that are obvious to the HoTT community are surprising to many algebraic topologists.

    I’d be interested to hear of anything specific that can be said along these lines. Will HoTT insights be expressible as understandable maxims, or will they remain difficult to comprehend.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMay 17th 2018

    There are two proofs by Rezk cited at Blakers-Massey theorem. The first, in Toposes and homotopy toposes, does indeed use model categories. But the second is the one that’s a translation of the HoTT proof and thus uses only elementary topos-theoretic properties, no model categories in sight. The latter writeup does talk about “spaces”, but he says at the beginning

    I expect that things go through in an arbitrary ∞-topos.

    I think one can just read his note essentially verbatim with “space” translated to “object”. I suppose maybe it would have been better if he’d written it in that language to start with and not trusted the reader to do the translation in their head?

    • CommentRowNumber8.
    • CommentAuthornimarasekh
    • CommentTimeMay 19th 2018

    OK, I am new to the forum and so my comments are more ambiguous than I expected. I will try to clarify.

    I’d be interested to hear of anything specific that can be said along these lines. Will HoTT insights be expressible as understandable maxims, or will they remain difficult to comprehend.

    When I was talking about the surprise among algebraic topologists I had the following in mind. There are many results that are well-known for spaces, such as truncations, factorizations, Blakers-Massey, … . Many of those results can be generalized, but very often the proof has to be changed. That’s exactly what resulted in the new proof of Blakers-Massey or truncations. In algebraic topology a standard way to construct truncations is the small object argument. That obviously doesn’t work in every setting, which is exactly why a new proof was necessary. As a result of this general fact algebraic topologists can react surprised that certain results about spaces can hold in other settings and I would like to change that.

    There are two proofs by Rezk cited at Blakers-Massey theorem. The first, in Toposes and homotopy toposes, does indeed use model categories. But the second is the one that’s a translation of the HoTT proof and thus uses only elementary topos-theoretic properties, no model categories in sight. The latter writeup does talk about “spaces”, but he says at the beginning.

    Yes, I had exactly those two proofs in mind in my previous post. I think you are right and the proof can be adjusted to a topos. The one thing that worries me are fiber-wise statements (like Lemma 1.4). By my understanding of the word fiber this only holds for spaces.

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeMay 20th 2018

    Ah, I didn’t realize Rezk was lazy in his translation that way. Statements like that, of course, should be interpreted in the HoTT sense of “fiberwise”, as a dependent product internal to the topos. You’re right that there would be some additional work to be done in writing that in true \infty-categorical language. On the other hand, maybe that work was already done by ABFJ? Their generalized Blakers-Massey theorem is explicitly “valid in an arbitrary higher topos” (as well as “with respect to an arbitrary modality”) and it looks like their proof is written in \infty-categorical language.

    • CommentRowNumber10.
    • CommentAuthornimarasekh
    • CommentTimeMay 20th 2018

    I think ABFJ might be a more promising path forward. At least one issue is that some of their results on modalities rely on presentability conditions (for example Proposition 3.1.8 and Proposition 3.3.8). In particular it seems to be needed for the parts where you have to show that we get a factorization system. So, those parts need to be adjusted somehow.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 20th 2018

    Right, you do need to be in something like a locally presentable setting in order to generate modalities by an arbitrary set of maps. But the classical Blakers-Massey is, I believe, the special case of their theorem applied to the truncation modalities, and those should exist in the elementary case. Indeed, the fact that truncations can be constructed from finite colimits and an NNO is a big part of what motivated me to suggest that we were ready for a tentative definition of elementary (,1)(\infty,1)-topos. However, as far as I know, that proof hasn’t been written out in categorical language yet.

    But that problem is already mentioned as (III) in your “Algebraic topology” section, so if that’s the only obstacle to applying ABFJ in the elementary case then it doesn’t seem like your problem (II) is really open any more. (Also, I think even in (III) you should say explicitly that the theorem has already been proven in HoTT, and all that remains to do is translate it into categorical language.)

    • CommentRowNumber12.
    • CommentAuthornimarasekh
    • CommentTimeMay 27th 2018

    I agree I should mention the HoTT work on NNO and truncations in the problem section. Thank you for reminding me.

    On the ABFJ I am still uncertain. It’s seems promising (and it should be true that descent is enough) but I still need to check in detail to make sure presentability hasn’t snuck into any of the later results.

    • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeMay 27th 2018

    That’s fair, but even before the checking has been done, their work (and Rezk’s) should still be mentioned in any discussion of this possibly-still-open problem.

    • CommentRowNumber14.
    • CommentAuthorspitters
    • CommentTimeJun 2nd 2018
    • (edited Jun 2nd 2018)

    Do we have a precise (classical) connection between Shulman/Rasekh and the work by Joyal, who uses model structures? Constructively, we would first need to develop a theory of \infty-categories, probably following Riehl/Shulman, perhaps along the lines of directed type theory and the work by Licata and Weaver slides.

    • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeJun 2nd 2018

    Which work by Joyal are you referring to?

    • CommentRowNumber16.
    • CommentAuthorspitters
    • CommentTimeJun 3rd 2018

    This one, the one linked to at that elementary+(infinity%2C1)-topos using tribes.

    • CommentRowNumber17.
    • CommentAuthorMike Shulman
    • CommentTimeJun 3rd 2018

    Hmm. Well, I haven’t worked out the details, but I expect that one of his presents one of ours, whereas it’s an open question whether every one of ours could be presented by one of his. Some of his axioms (like fibrancy of \mathbb{N}) are very strict, so strict that I don’t even know whether every Grothendieck (,1)(\infty,1)-topos has a model satisfying them. Other than that issue, it looks like the main difference is that he assumes one fixed universe as part of the structure rather than the mere existence of as many universes as necessary, plus the effectiveness of groupoid objects (which is not “elementary” in the sense of “finite”).

    • CommentRowNumber18.
    • CommentAuthorspitters
    • CommentTimeJun 3rd 2018

    He seems to restrict to Grothendieck toposes over Reedy categories, I don’t know why he wants NN to be fibrant.

    It would be good to record this in any case, currently, the page read like the two notions are equivalent.

    • CommentRowNumber19.
    • CommentAuthornimarasekh
    • CommentTimeJun 3rd 2018

    Mike as a follow up to our previous discussion, do you have (or are aware of) a write up of a proof for how to build an NNO in an EHT? I’ve seen you mention this based on the fact that it holds in HoTT, but was wondering if there is an actual higher categorical argument out there.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    I don’t think anyone has compiled the HoTT proof out into a topos-theoretic one. It’s kind of involved.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    My guess would be that he wants N to be fibrant for the same reason the 2LTT people do, so that he can do things like define a fibrant type of semisimplicial types by induction over it.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJun 4th 2018

    Added remarks on how Joyal’s definition differs from the one here.

    diff, v27, current

    • CommentRowNumber23.
    • CommentAuthornimarasekh
    • CommentTimeJun 4th 2018

    Yeah, that is what I was worried about. I think one important step in translating many of the results into an EHT is to have a concrete proof that we can construct an NNO. Well then let me rephrase my question. Do you know of a HoTT proof that would be more amenable to a translation to higher categorical language?

    • CommentRowNumber24.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 5th 2018

    Fixed a markdown-formatted link whose opening < was replaced by &lt;, so it had rendered looking like raw markdown.

    diff, v28, current

    • CommentRowNumber25.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    I think constructing an NNO out of the rest of the structure is more of a curiosity than an impediment to using the definition of EHT. Just like the question of whether we can construct colimits: the important thing is that colimits and the NNO are there; if we can remove them from the definition without changing the fact that they’re there, that’s nice, but it doesn’t make much of a difference in practice.

    • CommentRowNumber26.
    • CommentAuthornimarasekh
    • CommentTimeJun 5th 2018

    I thought we need an NNO to make the definition of an EHT work. Specifically the constructions by Egbert Rijke need colimits over countably infinite set. So we either have to assume it (which would be a non-finite assumption and so not elementary?) or we have to prove it.

    In particular in your blog post you suggest that one reason why we should not assume NNOs in a topos is exactly because we can prove it’s existence and then use that to recover the results of Rijke in the setting of an EHT.

    I think in that sense it is different from finite colimits. It am perfectly willing to assuming we have finite colimits (but it would be cool to know you can recover them), but I think it is important that we can build NNO to avoid assuming it.

    Based on your post are you suggesting we should just add the existence of an NNO to the definition of an EHT?

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJun 5th 2018

    An NNO is perfectly finite and elementary. I don’t think it is any different from finite colimits. The only difference between them is that in the 1-categorical case an NNO is not usually included in the definition and doesn’t follow from it — but probably more theorems about elementary 1-toposes than not add the assumption of an NNO, and there aren’t many interesting examples that lack one; so arguably it could just as well have been included.

    I think in a paper proving (say) the Blakers-Massey theorem in an EHT it would be perfectly in order to state the definition including an NNO and then say “it is expected that the existence of an NNO can be proven from the other axioms; this has been shown in homotopy type theory, which is conjecturally the internal language of EHTs, but the general internal language theorem has not yet been proven and the construction of an NNO has not yet been manually compiled out into categorical language.”

    • CommentRowNumber28.
    • CommentAuthorDavidRoberts
    • CommentTimeJun 5th 2018

    OT: about toposes without NNO… I guess sheaves of finite sets on a finite site, but are there finite versions of realisability topses? Lurie’s recent course on categorical logic ended up with \infty-pretoposes of finite homotopy types, which aren’t \infty-toposes, so that’s kind of an indication of the boundary between EHT and higher pretoposes as far as possessing NNO/W-types goes.