Thanks for the pointer! Dave had told me he was about to put this on the arXiv, but now I would have missed it.

Regarding your question: the general idea of étale gluing is certainly always the same, yes. The technical implementation may differ.

]]>When David Carchedi in Higher Orbifolds and Deligne-Mumford Stacks as Structured Infinity Topoi writes

we will make precise what is means to glue structured $(\infty, 1)$-topoi along local homeomorphisms (i.e. etale maps) starting from a collection of local models…

can we see this in terms of #12 and #13 above? Or is it that these local models come from a richer context than the types of a universe?

By the way, Carchedi has another paper just out, On The Homotopy Type of Higher Orbifolds and Haefliger Classifying Spaces, which begins

]]>In this paper, we explain how to functorially associated to an orbifold, or more generally to a higher ´etale differentiable stack, a canonical weak homotopy type. This builds on work of Dugger and Schreiber, who address this question for arbitrary higher stacks in [10] and [25], and also of Moerdijk who addresses this question in terms of ´etale Lie groupoids in [21]

All right.

I suppose what we should still add is a comment on motives as being linearized higher spaces. Much of noncommutative geometry finds a decent home there, and maybe the difficulties with making NCG a standalone theory of higher geometry are related to it “really” being more of an aspect of motivic geometry.

]]>Thanks! I made some more changes again. After thinking about it, I think this is a nice way of summarizing the derived NC AG story: 1) noncommutative schemes are dg-algebras glued together *along bimodules*; 2) dg-categories are a good setting for gluing along bimodules. I wrote the following on the page:

The above frameworks for higher geometry are not suitable for describing noncommutative algebraic geometry, because of the more complicated notions of localization, gluing and descent in the latter setting. Indeed, noncommutative spaces are supposed to be obtained from affine ones (formal duals of associative algebras or dg-algebras) by gluing along

bimodules. A good setting for such gluing is that of pretriangulated dg-categories (or stable (∞,1)-categories). Thus in derived noncommutative algebraic geometry, a noncommutative space is defined to be a stable (∞,1)-category.

I therefore removed the stable infinity-category subsection from the formalizations section, because I think it is more of an example than a formalization. A formalization would be a framework for geometry where the local models are associative algebras in a symmetric monoidal infinity-category, and gluing is along bimodules. For example, a special case of that would be “spectral noncommutative geometry” (associative ring spectra glued along bimodules). Does that make any sense?

Probably I should update the derived noncommutative algebraic geometry page as well, to link it back with higher geometry.

]]>I have further edited a little the Idea-section. Please check it out. Moved the paragraph on Connes-style NCG to a dedicated subsection of the Examples-section

]]>One little further edit:

where it said:

Following Jacob Lurie

I have expanded to

]]>Following Jacob Lurie (based on the theory of geometry via ringed toposes by Alexander Grothendieck and Monique Hakim)

Thanks for all this, Adeel.

I have to apologize for being weird, as it was indeed myself, long ago, who wrote the comment regarding the Giraud theorem.

In any case, I have edited the section Higher geometry – Formalizations – Via Stable infinity-categories further to better reflect what we said in #28 and #29. Please look over it to see if you agree. And please add what you just wrote in #30! I think that would fit nicely right at the point where this subsection presently ends.

I have also given the Higher geometry – Formalizations-section a lead-in that says again what the three different perspective that follow are like.

Then I have edited the subsection Higher geometry – Formalizations – Cohesive infinity-toposes a little more to make it clearer how this connects back to the “petit” previous perspective.

Please look at all this critically and please disagree or expand where you see the need.

]]>Here is some more speculation (nothing new to you, I think, but just to write it down). In any kind of geometry, one starts with some notion of local models. In NC algebraic geometry these are dg-algebras up to Morita equivalence. Then the various frameworks for higher geometry give a way to glue these local models together. Of course, the problem in NC AG is that there is no suitable Grothendieck topology to put on dg-algebras, so that the usual frameworks using infinity-topos theory do not work. Somehow, dg-categories solve this problem by apparently doing a good job of representing glued together dg-algebras. The hierarchy

- commutative algebras $\subset$ schemes $\subset$ stacks

has the rough analogue

- dg-algebras $\subset$ dg-categories of perfect complexes over dg-algebras $\subset$ dg-categories

with each of the levels above mapping into the respective level below. According to some of the literature, the middle level below is supposed to be thought of as “noncommutative schemes”, or, I guess, glued together dg-algebras. This setup therefore also has the property that glued together commutative algebras are mapped into glued together noncommutative ones. Somehow, this dg-category framework is supposed to be encoding some kind of descent, but it is not the notion of descent from topos theory. I don’t really know how to explain this.

]]>Hmm, interesting question. I am not sure if I know a convincing raison d’être for derived noncommutative algebraic geometry, that does not come from concrete considerations in the noncommutative world (such as what I wrote in this MO answer). To be honest, I am not fully convinced by the stable Giraud theorem story (I am not the original author of that paragraph, by the way, I just rephrased what was written there already in a way that made a bit more sense to me).

It seems to me that the noncommutative picture simply doesn’t fit into the frameworks of either structured or cohesive toposes. One interesting thing to note is that, rather than there being several different noncommutative geometries, there is just one noncommutative geometry encompassing everything. Hence, for any given “geometry” that has a notion of “quasi-coherent complex” (and hence perfect complex), there is a functor to noncommutative geometry (i.e. stable infinity-categories up to Morita equivalence).

As to the question of requiring the monoidal structure, I think that this is simply the observation that in noncommutative geometry, spaces are supposed to be considered up to Morita equivalence, nothing more and nothing less. Taking stable monoidal infinity-categories, one simply gets a fully faithful enlargement of commutative algebraic geometry. Hence these stories are basically completely unrelated, I would say. (Though I have not read DAG VIII yet, which means I don’t really know anything about the “tensor-triangulated geometry” story.)

]]>I have a question regarding the stable story:

I used to think that the “right” perspective here is that stable *monoidal* $\infty$-categories (of quasicoherent sheaves) play the role of “2-rings” and as such provide an $(\infty,2)$-higher version of algebraic geometry. And that it just so happens that Kontsevich et al used to consider essentially that, but without actually requiring the monoidal structure, which is possible to some extent but maybe more exotic than it needs to be.

But you seem to be saying now that via the stable Giraud theorem the non-monoidal stable higher geoemtry has its stand-alone *raison d’être*.

Is that the right way to summarize it? Maybe this distinction could be commented on a bit more in the entry.

]]>Thanks!

]]>Thanks! Nice.

Regarding that sentence, I have edited it to read now as follows, please let me know if that version now is intelligible:

]]>Notice that the proceess of forming groupoid convolution algebras is a (2,1)-functor from suitable differentiable stacks to C*-algebras with Hilbert bimodules between them. Much of Connes-style noncommutative geometry turns out to deal with objects in the image of this functor, and in this way also Connes-style noncommutative geometry may be regarded as being a way of speaking about the higher differential geometry of differentiable stacks.

I tried to rewrite some parts of the page higher geometry. However I admit I don’t know anything about the cohesive infinity-topos story, so if I have written something stupid, please feel free to revert.

(I don’t understand the sentence

Under forming groupoid convolution algebras and their higher analog, at least parts of higher geometry translate to noncommutative geometry.

so I just left it as is, but I think it would be helpful to expand a bit on whatever is meant.)

]]>Oh right, sorry. And hence why you said that internally we need the sharp before we can even define the flat.

]]>That would be the shape modality. For (just) the flat modality we need the inverse image of the terminal geometric morphism to be fully faithful, which is connectedness.

]]>Don’t you mean “locally connected topos”?

]]>Externally, a topos having a flat modality would just mean that the inverse image of its geometric morphism to the base topos is fully faithful, hence that it is a *connected topos*.

Internally the various modalities are more interrelated, because internally we first need to say what the base topos actually is supposed to be. The solution to that which Mike gave in our article was to first define the sharp modality, and then use that to define all the others.

And generally it’s a good idea to consider the flat modality and the sharp modality jointly. After all, they form the adjoint modality whose existence got Lawvere started in “On the future of category theory” and which he called “category of being”. For a topos, externally that makes a *local topos*.

So there’s something I haven’t considered before, is there some neat relationship between the conditions added so that a site is a cohesive site (connectedness, local connectedness,…) or to a topos or $\infty$-topos to be cohesive, and the modalities which take us from type theory to cohesive type theory? In other words, can I characterise the kinds of topos which instantiate, say, just a flat modality?

]]>Right, so given any model of bare homotopy type theory, i.e. given an $\infty$-topos, one may want to ask which further axioms it verifies. This is something quite general, not specific to cohesion.

For instance it seems to me that for what some people are trying to do it would be an urgent question to find axioms that sufficiently characterize the $\infty$-topos over the Nisnevich site. I suppose in this case one should go for an axiom that amounts to saying that algebraic K-theory (first of all makes sense and second) satisfies descent.

On the other hand, as I tried to amplify above, one does not need the full axiomatics of cohesion to speak of geometry. The main ingredient that most people will be content with is the the infinitesimal shape modality and its implied concept of formall étale morphisms. This are essentially what in Structured Spaces are the “admissible morphisms” and as implied there and in precursor’s such as Hakim’s old thesis, this alone induces much of algebraic geometry.

Roughly, the more of the other modalities of cohesion are added, the more does this geometry exhibit aspects of *differential* geometry.

And I think some time in the future people will stop building models in an ambient set theory and then ask if they are models for some homotopy type theory with possibly some extra axioms added, and instead proceed entirely within the homotopy type theory. The way things are currently progressing this will be far ahead in the future, but I suppose the time will come.

]]>Then we might add the story of how to turn kinds of space into something which obeys the chosen axioms, e.g., given the choice of the full cohesive axiom package and the choice of a certain kind of space, how to see whether there’s a cohesive site around on the category of those spaces.

]]>Regarding the first question:

Yes, all these extra properties of $X$ that I mentioned will also be extra properties of the $U_i$. I didn’t mean to make a distinction here.

Indeed, in that hierarchy I mentioned, in the first layer we’d specify these *modes of being* (modalities) that any type whatsoever in the type system may have, and then then we pick model spaces, and then we glue them.

By the way, given the first layer, then there may be some canonical model spaces singled out. For instance given a shape modality, one may ask if it happens to be equivalent to $\mathbb{A}^1$-localization for some model space $\mathbb{A}^1$. If so, that singles out this model space (as the “continuum”). This happens for instance in smooth cohesion with the real line. In this sense manifolds are a “canonical” type of space in smooth cohesion.

Regarding your second question:

If we follow the discussion at *higher Klein geometry* and declare that a higher Klein model space is the homotopy fiber of a function of pointed connected types $\mathbf{B}H \to \mathbf{B}G$, then that is something one will eventually consider in any homotopy type theory, regardless of whether it carries geometric modalities or not. But only if it carries geometric modalities will we be able to demand, if we want, that $H$ and $G$ here should be suitably geometric group objects, instead of very general and possibly very “wild” group objects.

Can’t some part of ensuring that

for $X$ to be a reasonable kind of space, then there ought to be a decent concept of differential forms on it

be already present in the choice of model spaces? I.e., why not have differential forms on the $U_i$?

More generally, how does the role of homotopy type theory in forming the model spaces (as mentioned above in #12 in the case of higher Klein geometry) mesh with the roles you’ve just outlined?

]]>Right, that’s exactly the question to ask.

In an arbitrary infinity-topos / homotopy type theory, you could just choose a bunch of types $\{U_i\}$ and then consider types $X$ such that there are 1-epimorphisms of the form $\coprod_j U_{i(j)} \to X$.

That would be the very first condition for $X$ to qualify as a “geometric infinity-stack”. But in applications one will find that this is a very weak concept of a space modeled on the $\{U_j\}$s, and so one will want to add more axioms to the ambient homotopy type theory in order to be able to express more accurate concepts of space.

From the point of view of scheme theory / manifold theory, the crucial ingredient is that one needs to know which maps qualify as being formally étale. This is in order for $X$ not just to be covered by the $\{U_j\}$, but to actually be locally equivalent to them. The modality that axiomatizes formal étalness is the infinitesimal shape modality and so here one would tend to want to assume this.

Then you might go on.

You might say that for $X$ to be a reasonable kind of space, then there ought to be a decent concept of differential forms on it “measuring its extension”. That effectively amounts to assuming that there is also a flat modality.

You might say that for $X$ to be a reasonable kind of space, then it ought to have a “shape” that is an actual homotopy type. This is not guaranteed in bare homotopy type theory, and so to guarantee it one would add the axiom to the ambient system that there exists a shape modality.

You might say that for $X$ to be a reasonable kind of space, then it ought to have a decent formal neighbourhood around each of its points. To guarantee this, assume an infinitesimal flat modality.

And so forth. So there is a minimum ambient context in which a very loose concept of space exists, and then there are modal strengthenings of the context which make the concepts of space which may be axiomatized have more and more of the properties (modes of being) that one might want a space to have.

As with all axioms, which axioms exactly one chooses to add to the ambient homotopy type theory will depend on which application one is looking into.

]]>Thanks! I’m fond of the idea that an indication of an important development in science and maths is that it allows for the telling of a simpler and more coherent history of the subject. It sounds like we may have that here.

So to be clear about what precisely (1) provides, we may have dreamt up our test spaces (2), and look to glue something resembling them together (3). But really we need (1) to provide what it is to resemble the test spaces? Or is it playing a role in the gluing too?

Perhaps that’s the same as asking, if we only had resources to produce things like $\coprod_j U_j$, what would we lack?

]]>