Etale / Smooth / Unramified etc.

Stream: mathlib4

[Christian Merten]

@Judith Ludwig and I am working on properties of étale (resp. smooth, resp. unramified) morphisms. For this we suggest refactoring the current file setup slightly. Some options:

1. Make three folders RingTheory/Etale/, RingTheory/Unramified/, RingTheory/Smooth/ with a Basic.lean file with the definitions (e.g. the currently existing docs#Algebra.FormallyEtale and after the refactor a new Algebra.Etale, analogously for unramified and smooth). More complicated characterisations and properties could then go in specialized files in the respective folder.
2. Make a new folder RingTheory/Etale/, move the current RingTheory/Etale.lean to RingTheory/Etale/Formally.lean and add the new etale (resp. unramified, resp. smooth) definitions to a new file RingTheory/Etale/Basic.lean.

I am in favour of option one, since it keeps files shorter and hence makes more space for further progress. Since these notions are quite fundamental, a lot of API needs to be built around them.

What do you think? Are you happy with option one? (cc @Andrew Yang, the author of the current RingTheory.Etale.lean)

[Andrew Yang]

I also wanted to split up the file and I think option 1 makes a lot of sense.

[Andrew Yang]

I'm also thinking about developing some of the materials there and is there anything I could collaborate on? I have some drafts lying here and there (#11793, #11843, and one on the Jacobi-Zariski sequence not yet pushed) to see what attempt is best and I think they might be helpful?

[Christian Merten]

Good to know, happy to collaborate on this! I am just reading through your PRs. We were also thinking about characterisation of étale k-algebras, which I see you have already completed in #11793. Some thinkgs that we were planning to do:

• Characterisation of unramified via stalks (i.e. finite separable extensions of residue fields). This should follow rather easily from your characterisation of unramified k-algebras.
• etale = flat + unramified
• open immersion = etale + radicial
• standard etale (resp. smooth) morphisms
• etale = smooth of relative dimension zero (this might have to wait for dimension theory, at least to have a clean statement)

Does this interfere with anything you are planning to do?

[Andrew Yang]

Are you talking about ring homomorphisms or morphisms between schemes? Most of my plans are on the algebraic side, as I'm waiting for the AG workshop for some insights on whether the current approach on morphisms is the right one. But if you have some thoughts on this I'm all ears.

[Judith Ludwig]

We planned to focus on the commutative algebra part, i.e. ring maps for now.

[Andrew Yang]

My current target now is to show that formally smooth iff $\Gamma_{S/R}$(the $H^1$ of the cotangent complex) is zero and $\Omega_{S/R}$ is projective. Then it should be easy to show that formally-unramifed, formally-unramified and smooth are all Zariski-local.

[Andrew Yang]

And maybe we should change up the definition to make it universe polymorphic once that's done.

[Christian Merten]

Christian Merten said:

Judith Ludwig and I am working on properties of étale (resp. smooth, resp. unramified) morphisms. For this we suggest refactoring the current file setup slightly. Some options:

1. Make three folders RingTheory/Etale/, RingTheory/Unramified/, RingTheory/Smooth/ with a Basic.lean file with the definitions (e.g. the currently existing docs#Algebra.FormallyEtale and after the refactor a new Algebra.Etale, analogously for unramified and smooth). More complicated characterisations and properties could then go in specialized files in the respective folder.
2. Make a new folder RingTheory/Etale/, move the current RingTheory/Etale.lean to RingTheory/Etale/Formally.lean and add the new etale (resp. unramified, resp. smooth) definitions to a new file RingTheory/Etale/Basic.lean.

I am in favour of option one, since it keeps files shorter and hence makes more space for further progress. Since these notions are quite fundamental, a lot of API needs to be built around them.

What do you think? Are you happy with option one? (cc Andrew Yang, the author of the current RingTheory.Etale.lean)

The split is #12017

[Matthew Ballard]

Should there be RingTheory.Morphisms for better organization and to reflect AG?

[Christian Merten]

While I like the idea, there might be a better name? Since most things are defined in terms of algebras, not in terms of ring homs. Maybe RingTheory.Relative?

[Andrew Yang]

I think maybe RingTheory/Properties

[Christian Merten]

Andrew Yang said:

I think maybe RingTheory/Properties

Aren't most things in RingTheory/ properties? (e.g. PrincipalIdealDomain should probably not belong to that new folder)

[Matthew Ballard]

I delegated #12017 with a comment.

I still like morphisms since that is how the majority of algebraic geometers would describe these things (my guess).

[Andrew Yang]

Yeah I'd prefer morphisms more as well. We'll need a ringhom definition for each algebra definition anyway so I guess the name is fine?

[Matthew Ballard]

This is more a meta-label than a specific type class one in my mind.

[Christian Merten]

Fine with me.

[Kevin Buzzard]

Sorry, I was in the process of reviewing as well but my daughter has just started a harp lesson and I've been kicked out of the room with the computer I was using! I will be able to finish my review in an hour if you can face hanging on for that long.

[Christian Merten]

I can certainly face hanging on for that long :D

[Kevin Buzzard]

OK, apologies; I'd hoped to get to the end before the lesson started.

[Christian Merten]

No worries :)

[Judith Ludwig]

"Properties of morphisms" is what I would call the corresponding chapter in an algebraic geometry lecture course, if I had to name it (ok I'd be talking about schemes, but even in the ring theoretic context, I think), but I guess this is too long for mathlib? (I'm new to this, so I'll be asking naive questions, sorry for that).

[Kevin Buzzard]

Right now we have RingTheory.FiniteType (property of morphism, just one of many), RingTheory.Fintype (property of object, just one of very many), RingTheory.Discriminant (a definition involving rings), RingTheory.EisensteinCriterion (a theorem about rings), etc etc, so I don't think there's any need to start changing any names or adding any directories in this PR; whilst it arguably needs to be done, it shouldn't be done at the same time as this file split (which is already slightly complicated to review).

[Christian Merten]

There is one more splitting PR #12030 are some definitions in #12044. Stability under base change is next, which needs to be done for finite presentation.

[Christian Merten]

The next goal would be smooth implies flat. @Andrew Yang: is this currently on your roadmap?

[Andrew Yang]

No. What proof do you plan to use?

[Christian Merten]

For the discussion on "essentially of finite type / presentation": This version sounds quite non-standard to me, so I am not sure about deviating here. Does the "essential" part allow arbitrary localisations?

[Christian Merten]

Defining unramified as formally unramified + finite type is fine to me, I think fin. pres. is the EGA definition, but as you say there are quite a few sources which use the finite type version.

[Christian Merten]

IMHO it's better to have standard definitions of smooth, etale, unramified etc. and state theorems in maximal generality, so if a theorem holds under the weaker "essentially of finite type" assumption, then it can (should) be stated under the weaker assumptions. Type class inference will then allow applying the more general versions in the case of having a Ramified R A assumption.

[Christian Merten]

Andrew Yang said:

No. What proof do you plan to use?

First I would like to reduce to the Noetherian case using https://stacks.math.columbia.edu/tag/00TP and then argue along the lines of Bourbaki (chapter 10 of commutative algebra) or https://arxiv.org/pdf/1504.05709.pdf.

[Judith Ludwig]

The stacks project also has finite presentation as a condition for etale morphisms https://stacks.math.columbia.edu/tag/00U1
and I think I've always used this definition. Same for smooth morphisms: https://stacks.math.columbia.edu/tag/00T2 .

[Andrew Yang]

First of all: Yeah finite type is not enough for etale or smooth morphisms, but finite type should be enough for unramified. Among other reasons, unramified morphisms are morally (etale-)locally closed immersions but closed immersions aren't necessarily of finite presentation.

[Andrew Yang]

I think I've seen ess. of finite presentaiton instead of finite presentation at various places (for example the paper on smooth => flat you linked) but I have yet to find another book using this definition.

[Andrew Yang]

If $f : R \to S$ is of finite type, then $f$ is unramifed at $q \in \operatorname{Spec}(S)$ iff $R \to S_q$ is unramified. But this only works if you allow ess. finite type maps. Or you would like to check on stalks $R_p \to S_q$, which is also not finite type as well. Of course you may define a separate class of unramified morphisms on local rings (as in stacks#024L) that allows ess. finite type local ring homs but I'd argue we just use the definition unramifed = formally unramified + ess. finite type globally.

[Christian Merten]

Andrew Yang said:

I think I've seen ess. of finite presentaiton instead of finite presentation at various places (for example the paper on smooth => flat you linked) but I have yet to find another book using this definition.

Bourbaki actually also uses the "essentially" definition.

[Christian Merten]

If $f : R \to S$ is essentially of finite presentation and formally smooth, then by definition $f$ is a composition $R \to A \to S$ where $R \to A$ is of finite presentation and $A \to S$ is a localization. Does it follow that $R \to A$ is formally smooth?

[Andrew Yang]

No but smooth at every $q \in \operatorname{Spec} A$ contained in $\operatorname{Spec} S$.

[Christian Merten]

Well, so using stacks#00TP to reduce to the Noetherian situation does not work which rules out relying on Bourbaki (defines smooth only for Noetherian base ring). Hence with the "essentially" definition, the only source on these topics are the notes by Iversen?

[Andrew Yang]

A way to reduce the ess. finite presentation case to the fp case is to show that $R \to A_q$ smooth then $R \to A_g$ smooth for some $g \not\in q$.

[Andrew Yang]

So if $R \to S$ is ess. fp and formally smooth, you can always find $R \to A \to S$ with $R \to A$ f.p. and smooth and $A \to S$ a localization.

[Christian Merten]

Ahh! That way it sounds reasonable to me.

[Joël Riou]

I think it is better to follow standard definitions, and assume finite presentation, similarly as in EGA IV 17.3.1, a morphism of schemes is smooth (resp. étale, unramified) if it is (locally) of finite presentation and formally smooth (resp...), so that a morphism of algebra is smooth (resp...) iff the corresponding morphism of affine schemes is.
Of course, at some point, we shall have to formalize the limit arguments of EGA IV 8 (one of my favourite references...).

[Andrew Yang]

As mentioned above, I don't think the literature has a consensus on what is "standard"? As for "a morphism of algebra is smooth (resp...) iff the corresponding morphism of affine schemes is", I agree that this is a valid point but we will need to (and be able to) relax most of the assumptions to ess. of finite presentation to describe the map on stalks anyways.

[Christian Merten]

As I said earlier: We can have both, standard definitions (e.g. smooth = formally smooth + fin.pres.) and general theorems (only assuming essentially fin. pres + formally smooth for instance). As soon as Algebra.FinitePresentation is a class, typeclass inference will fill in assumptions automatically and we can seamlessly apply the more general theorems if Smooth R S is given.

[Christian Merten]

Alternatively we could define Smooth and EssentiallySmooth where the former is the fin.pres. definition and the latter is the former up to composition with a localization.

[Antoine Chambert-Loir]

About what is standard and what is not, mathlib may have interest in making bold decisions, because standard definitions were sometimes made at a time were objects used nowadays were not looked as relevant. (I'm thinking of associated ideals, eg, whose “standard” definition does not work outside of noetherian hypotheses.)

[Christian Merten]

Christian Merten said:

As I said earlier: We can have both, standard definitions (e.g. smooth = formally smooth + fin.pres.) and general theorems (only assuming essentially fin. pres + formally smooth for instance). As soon as Algebra.FinitePresentation is a class, typeclass inference will fill in assumptions automatically and we can seamlessly apply the more general theorems if Smooth R S is given.

Is this a compromise, that you are happy with @Andrew Yang ?

[Judith Ludwig]

Etale morphisms were my starting point in all of this.
And IMO a good definition for etale is "etale = form. etale + fin.pres". Then I would want to have "etale = smooth + unramified".
Now as was mentioned above, unramified should have a weaker finiteness assumption, i.e. fin.type not fin.pres .
So to get the equivalence "etale = smooth + unramified", I would define smoothness with the same finiteness condition as etale, i.e. "smooth = form.smooth + fin.pres" and not the essential condition.
And then I feel it's cleaner to also have unramified = form. unramified + fin.type.
And as Christian Merten suggested we could make an essential version of smoothness and a definition essentially unramified. This language then seems fairly intuitive to me.

[Andrew Yang]

I'm fine with either definition as long as the theory is developed in sufficient generality.

[Christian Merten]

To record this here: Smooth implies flat is done in summary (draft) PR #12695. I took a slight detour via flatness of adic completions and models for smooth algebras over Noetherian rings, but essentially the proof is the one from https://arxiv.org/pdf/1504.05709.pdf. As said in the PR description, I'll slowly split it into multiple parts.

[Christian Merten]

@Andrew Yang I would like to prove the "converse" now. Namely, etale = flat + unramified. Probably via showing that "smooth = flat + smooth fibres", but for the latter I have not yet looked at a proof. Are you working on anything related?

[Andrew Yang]

I think the Jacobian criterion will follow from my work:
If $R \to S$ is a local ring homomorphism ess. of f.p. and $k$ the residue field of $S$, then $S/R$ is smooth iff $NL_{S/R} \otimes_S k$ is injective.
($NL$ is the (truncated) cotangent complex stacks#00S0)

This then imply flat + smooth fibres => smooth:
Let $S/R$ be flat and (ess of) f.p., and $q$ a prime of $S$ over $p$.
Then $\kappa(p) \to S_q \otimes_R \kappa(p)$ is (formally) smooth iff $NL_{S_q \otimes_R \kappa(p)/\kappa(p)} \otimes_{S} \kappa(q)$ is injective (jacobian criterion).
Since $S_q/R$ is flat, $NL_{S_q \otimes_R \kappa(p)/\kappa(p)} = NL_{S_q/R} \otimes_R \kappa(p)$.
So $\kappa(p) \to S \otimes_R \kappa(p)$ smooth iff $NL_{S \otimes_R \kappa(p)/\kappa(p)} \otimes_{S} \kappa(q) = NL_{S_q/R} \otimes_{S_q} \kappa(q) = NL_{S_q/R_p} \otimes_{S_q} \kappa(q)$ injective iff $R_p \to S_q$ smooth (jacobian criterion again).
So flat + smooth fibres imply $S_q/R_p$ smooth for all $q$ imply $S/R$ smooth.

[Christian Merten]

Why can you apply the Jacobian criterion in these two steps? Neither $S \otimes_R \kappa(p)$ is local in the first step, nor is $R$ in the second.

[Andrew Yang]

Apply that on $\kappa(p) \to S_q \otimes_R \kappa(p)$ and $R_p \to S_p$.

[Andrew Yang]

Okay fixed the proof above. We can reduce to the case where $R \to S$ is a local ring hom anyway and that was messing with my brain.

[Christian Merten]

Ah that now makes sense to me. And you prove separately that $R_{\mathfrak{p}} \to S_{\mathfrak{q}}$ smooth for all $\mathfrak{p}$ and $\mathfrak{q}$ over $\mathfrak{p}$ implies $R \to S$ smooth?

[Andrew Yang]

Yeah. $R_p \to S_q$ is smooth iff $NL_{S_q/R_p} = NL_{S_q/R} = NL_{S/R} \otimes_S S_q$ is split injective. But since $H^0(NL_{S/R}) = \Omega_{S/R}$ is finitely presented when $S/R$ is ess. of fp, being split injective is local on stalks.