I have split the entry in two. I didn’t see another way out after unsuccessfully trying to safe it for about an whole hour. The paragraph that I had meant to point to above should now be visible here. Not a big deal, that was just meant as a side remark. A side remark that cost me an hour of experimenting.

]]>sorry, that last addition that I mentioned is still not visible. The Lab has been slow all day, but now it takes many *minutes* to save long entries like that on cohesive $\infty$-toposes. A steam engine computer would be faster. And apparently we are now actually at the point where it fails to safe at all. Maybe I need to split the entry. Or migrate to another software…

I have expanded the definition of formal smoothness/unramifiedness/étaleness in the general abstract context of “infinitesimal cohesion” here and added a note highlighting the subtlety about the unramified-condition discussed above.

]]>We still need to go back to the entry de Rham space and fill in all the right technical qualifiers in order to correctly reproduce various traditional notions.

But I am currently taking a general perspective essentially equivalent to that of Kontsevich-Rosenberg’s: since I can define $dR(X)$ abstractly in great generality, I *define* formal smoothness in any context by this epi-condition. But then of course, I agree, one wants to carefully state the conditions under which this reproduces various traditional notions.

Hey Urs, by the way, the determination of smoothness by requiring a map to be epi on the dR space only works with Noetherian hypotheses. This is because the nilradical is only a nilpotent ideal provided that R is noetherian.

]]>So in the 1-categorical context we look at the morphism

$X \to dR(X)$of any space into its de Rham space and consider three cases

it is an epimorphism, then we say $X$ is formally smooth;

it is a monomorphism, then we say $X$ is formally unramified;

or it is both, hence an isomorphism if we are in a balanced category, then we say $X$ is formally étale.

(Or rather, we look at the relative versions of these statements, so that the second two points become useful).

This is equivalent to what Kontsevich-Rosenberg consider, under the dictionary discussed here. Notice that there I write $\mathbf{\Pi}_{inf}(X)$ for $dR(X)$.

Now when we lift this from 1-category theory to $(\infty,1)$-category theory, the notions of epimorphisms and of monomorphisms multiply. The good notion of epimorphism that we seem to want to keep here is effective epimorphism in an (infinity,1)-category. So we say

A (derived) $\infty$-stack $X$ is formally smooth if $X \to dR(X)$ is an effective epimorphism.

A (derived) $\infty$-stack $X$ is formally etale if $X \to dR(X)$ is an effective epimorphism equivalence.

(Or rather, again, the relative versions of these statements.)

But now there is no direct analog of the above mono-condition. We could ask $X \to dR(X)$ to be a k-truncated morphism for all $k$. For $k = -2$ this is an equivalence. So we could say as $k$ decreases from $\infty$ to -2 that we are approaching formal etalness.

]]>I do not understand, what is the problem, could you guys explain it to me ? Is it in $(\infty,1)$-only, or also in $(\infty,2)$-context ? You started talking just vague $\infty$, what is confusing when making statement about different categorical dimensions.

]]>Formal unramifiedness is a condition that is nonsense in the derived setting.

Yes, and for a good reason: in the $\infty$-categorical context the statement “epi plus mono is iso” is nonsense. Formal smoothness has a good $\infty$-version: $X$ is formally smooth if $X \to dR(X)$ (the canonical morphism to the de Rham space) is an effective epimorphism (or similarly for the relative version). And analogously for formal etalness and equivalences. But the mono-condition that gives formally unramified in the 1-categorical context has no good analog.

]]>I don’t believe that either the Kontsevich-Rosenberg or even the EGA version of formal smoothness is actually accepted in the context of derived algebraic geometry.

For instance, formal smoothness fails to be determined stalkwise.

]]>Formal unramifiedness is a condition that is nonsense in the derived setting. It is a first approximation to formal etaleness and a that’s it (that is, in terms of the cotangent complex, it means that its zeroth homotopy vanishes.

]]>Good. In the scheme context somebody should eventually take EGA IV and write various properties and theorems in that context.

]]>I have split off formally unramified morphism from unramified morphism. Then I added the general-abstract topos theoretic characterization, by essentially copy-and-pasting the discussion from formally smooth morphism (and replacing epimorphisms by monomorphisms)

]]>