sheafifying Kaehler differentials

Stream: maths

[Kevin Buzzard]

Fix a base ring R. To an R-algebra A one can attach the A-module of Kaehler differentials, and given a commutative square comprising of a morphism from an R-algebra A to an S-algebra B, there's a corresponding A-linear map docs#KaehlerDifferential.map from the differentials of A/R to the differentials of B/S.

What theorems about KaehlerDifferential.map do I need in order to wave a magic glue wand and get the construction of a sheaf of O_X-modules associated to a morphism of schemes X->S ?

[Christian Merten]

This might not be what you are looking for, but the stacks project defines derivations for morphisms of schemes by defining it for morphisms of sheaves of rings from scratch (i.e. without gluing, but by defining a sheafy version of derivations and by showing the derivations functor is representable). See: https://stacks.math.columbia.edu/tag/08RL

[Joël Riou]

Actually, it is not clear how to define $\Omega^1_{X/S}$ as a presheaf, because even if $U$ is an affine open subset of $X$, it may not lie over an affine open subset of $S$... However, it may be possible to define the "absolute" $\Omega^1$ by sheafifying modules of $\Omega^1_{R/\mathbf{Z}}$, and then define the relative version as a cokernel (killing the differentials coming from the base, see Hartshorne II 8.11 for the general cokernel sequence of differentials).

Otherwise, the standard definition of $\Omega^1_{X/S}$ would be like in Hartshorne as $I/I^2$ where $I$ is the Ideal of the diagonal embedding of $X$ in the fibre product of two copies of $X$ over $S$. (This is also the definition in EGA IV 16.3.1.)

For mathlib, I may favour the first definition I suggest above. From any of these two definitions, it should be possible to prove the universal property that @Christian Merten is referring to.

[Christian Merten]

Is it advisable to define a IsDifferential f F class where f is a morphism $X \to S$ and F is an $\mathcal{O}_X$-module? In this case one has to formulate the universal property anyway, so I think at least a definition of derivations in the sheafy sense is needed.

[Joël Riou]

I agree that we need to phrase the universal property! But, in order to prove some of the properties, we need a construction! The advantage of the construction I suggest is that it should allow the use of the existing API for rings.

[Christian Merten]

Joël Riou said:

Actually, it is not clear how to define $\Omega^1_{X/S}$ as a presheaf, because even if $U$ is an affine open subset of $X$, it may not lie over an affine open subset of $S$... However, it may be possible to define the "absolute" $\Omega^1$ by sheafifying modules of $\Omega^1_{R/\mathbf{Z}}$, and then define the relative version as a cokernel (killing the differentials coming from the base, see Hartshorne II 8.11 for the general cokernel sequence of differentials).

Otherwise, the standard definition of $\Omega^1_{X/S}$ would be like in Hartshorne as $I/I^2$ where $I$ is the Ideal of the diagonal embedding of $X$ in the fibre product of two copies of $X$ over $S$. (This is also the definition in EGA IV 16.3.1.)

For mathlib, I may favour the first definition I suggest above. From any of these two definitions, it should be possible to prove the universal property that Christian Merten is referring to.

Can't I take an open affine covering $V_i = \mathrm{Spec}(R_i)$ of $S$ and then affine open coverings $U_{ij} = \mathrm{Spec}(A_{ij}) = U_{ij}$ of the preimages of the $V_i$ and then glue the $\widetilde{\Omega^1_{A_{ij} / R_i}}$?

[Christian Merten]

(I have no idea if that matters, because I have never used the sheafy differentials module for other things than schemes, but an advantage of the stacks project approach might be that it allows to define the sheaf of differentials for an arbitrary morphism of sheaves of rings)

[Joël Riou]

Of course, the glueing approach must work, in principle, but I would rather show general properties of a more global construction, and then deduce that it is compatible with restriction to open subsets.
(Note that the construction I have given may also work for a morphism of comm. ringed sites.)

[Kevin Buzzard]

If $R_1\to R_2$ is an open embedding on Specs. and $A$ is an $R_2$-algebra, is the induced morphism $\Omega_{A/R_1}\to \Omega_{A/R_2}$ an isomorphism?

[Christian Merten]

If $R_2$ is a localization at some multiplicative set of $R_1$, then yes, I think.

[Kevin Buzzard]

if it isn't then how is your sheaf above well-defined? There can be more than one $R_i$ for a given $A_{i,j}$ (but it could well be. Open immersions are etale if that helps)

[Joël Riou]

Kevin Buzzard said:

If $R_1\to R_2$ is an open embedding on Specs. and $A$ is an $R_2$-algebra, is the induced morphism $\Omega_{A/R_1}\to \Omega_{A/R_2}$ an isomorphism?

Yes, because it suffices to check it is an iso after localizing at any prime ideal of $R_2$, and after localizing an open immersion we get an isomorphism of local rings.

[Joël Riou]

A slightly different way to formulate the construction I have suggested above is that if $f : X → S$ is a morphism of schemes (or more generally comm. ringed sites), then, we may consider $O_X$ as a module over the sheaf of rings $f^{-1}O_S$ and construct $\Omega^1_{X/S}$ by sheafifying the presheaf of the $\Omega$ of the sections of $O_X$ relative to the sections of $f^{-1}O_S$. What I suggested was to do this in two steps: define the absolute $\Omega^1_{X}$ (over the integers) for any $X$, and then define the relative $\Omega^1_{X/S}$ as the cokernel of $f^* \Omega^1_{S} \to \Omega^1_{X}$.

[Antoine Chambert-Loir]

Maybe it is worthy to spell out the general construction of a sheaf on the big relative Zariski site (with objects $(f\colon X \to S)$) from a construction of something on algebras $(j\colon R \to S)$.

[Christian Merten]

Antoine Chambert-Loir said:

Maybe it is worthy to spell out the general construction of a sheaf on the big relative Zariski site (with objects $(f\colon X \to S)$) from a construction of something on algebras $(j\colon R \to S)$.

I think the construction of $\Omega^1_{X/S}$ is really not about schemes or morphisms of schemes, but rather a construction on a morphism of sheaves of rings on some top. space (or site).

[Andrew Yang]

One of the reasons I choose the definition of docs#KaehlerDifferential was to connect to the EGA definition of $\Omega_{X/S}^1$ better. I think it wouldn't be that hard to identify them locally? Are there any major disadvantages to this approach?

[Joël Riou]

Andrew Yang said:

One of the reasons I choose the definition of docs#KaehlerDifferential was to connect to the EGA definition of $\Omega_{X/S}^1$ better. I think it wouldn't be that hard to identify them locally? Are there any major disadvantages to this approach?

In case of rings, we have both the definition as a "cotangent" and a universal property, so that once $\Omega_{X/S}^1$ is defined, this original approach for the case of rings should help compare the definition with that of EGA.

[Joël Riou]

In the very draft PR #11570, I construct the absolute differentials of a presheaf of modules. It should not be too hard to state and obtain the universal property it satisfies, as well as deducing the relative notion.
I have also made an attempt at constructing the sheafification of a presheaf of modules #11555 (this is a very pedestrian approach, but it is the most efficient way I could think of).
The only annoying thing I see working with (pre)sheaves of modules in Lean is that it seems difficult to setup things so that dsimp/simp do what we would expect: I am using erw absolutely everywhere. If anybody knows how to ease automation, that would be great.

[Adam Topaz]

Joël Riou said:

The only annoying thing I see working with (pre)sheaves of modules in Lean is that it seems difficult to setup things so that dsimp/simp do what we would expect: I am using erw absolutely everywhere. If anybody knows how to ease automation, that would be great.

This is a bit concerning, and will likely mean that sheaves of modules won't scale very nicely. We should think about how to solve this ASAP.

[Joël Riou]

Among the things to do, I think that the definitional properties of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.html#ModuleCat.restrictScalarsComp' could be improved so that restrictScalarsComp'_hom_apply becomes rfl (and similarly for restrictScalarsId'). Then, find the suitable way to make a good (d)simp lemma of restrictScalarsComp'_hom_apply (currently the simpNF linter complains).

[Christian Merten]

Why does docs#ModuleCat.restrictScalarsComp' exist? It seems to be used only to define docs#ModuleCat.restrictScalarsComp. So why the extra argument hgf : gf = g.comp f which causes the need for subst?

[Joël Riou]

It has to exist because when we have a presheaf of rings R, the equality R.map (f ≫ g) = R.map f ≫ R.map g is usually not a definitional equality.

[Antoine Chambert-Loir]

Christian Merten said:

Why does docs#ModuleCat.restrictScalarsComp' exist? It seems to be used only to define docs#ModuleCat.restrictScalarsComp. So why the extra argument hgf : gf = g.comp f which causes the need for subst?

I don't believe there is LinearMap.restrictScalarsComp neither…

[Antoine Chambert-Loir]

(At least, I couldn't find it yesterday when I needed it!)

[Christian Merten]

Joël Riou said:

Among the things to do, I think that the definitional properties of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.html#ModuleCat.restrictScalarsComp' could be improved so that restrictScalarsComp'_hom_apply becomes rfl (and similarly for restrictScalarsId'). Then, find the suitable way to make a good (d)simp lemma of restrictScalarsComp'_hom_apply (currently the simpNF linter complains).

If I understand correctly, this should make it better:

/-- The restriction of scalars by a composition of ring morphisms identify to the
composition of the restriction of scalars functors. -/
def restrictScalarsComp' :
    ModuleCat.restrictScalars.{v} gf ≅
      ModuleCat.restrictScalars g ⋙ ModuleCat.restrictScalars f := NatIso.ofComponents <| by
  intro M
  fapply Iso.mk
  exact ⟨⟨fun x ↦ x, by intro x y; rfl⟩, by intro r x; subst hgf; rfl⟩
  exact ⟨⟨fun x ↦ x, by intro x y; rfl⟩, by intro r x; subst hgf; rfl⟩
  rfl
  rfl

The lemma you mentioned is rfl then.

[Christian Merten]

Joël Riou said:

Then, find the suitable way to make a good (d)simp lemma of restrictScalarsComp'_hom_apply (currently the simpNF linter complains).

How can I check this locally?

lake exe runLinter Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

does not complain when I remove the nolint simpNF attribute.

[Matthew Ballard]

Can we do it without building data in tactics? It makes me nervous

[Christian Merten]

This fixes the simp NF issue:

def restrictScalarsComp'_app (M : ModuleCat R₃) :
  (restrictScalars gf).obj M ≅ (restrictScalars f).obj ((restrictScalars g).obj M) := ⟨
     ⟨⟨fun x ↦ x, fun x y ↦ rfl⟩, fun r x ↦ by subst hgf; rfl⟩,
     ⟨⟨fun x ↦ x, fun x y ↦ rfl⟩, fun r x ↦ by subst hgf; rfl⟩,
     rfl,
     rfl
  ⟩

@[simp]
lemma restrictScalarsComp'_app_hom_apply (M : ModuleCat R₃) (x : M):
  (restrictScalarsComp'_app f g gf hgf M).hom x = x := rfl

@[simp]
lemma restrictScalarsComp'_app_inv_apply (M : ModuleCat R₃) (x : M):
  (restrictScalarsComp'_app f g gf hgf M).inv x = x := rfl

/-- The restriction of scalars by a composition of ring morphisms identify to the
composition of the restriction of scalars functors. -/
abbrev restrictScalarsComp' :
    ModuleCat.restrictScalars.{v} gf ≅
      ModuleCat.restrictScalars g ⋙ ModuleCat.restrictScalars f :=
  NatIso.ofComponents <| fun M ↦ restrictScalarsComp'_app f g gf hgf M

I made restrictScalarsComp' an abbrev so that simp unfolds to the new restrictScalarsComp'_app which is already formulated in the applied form so we can have simp lemmas for it. This makes restrictScalarsComp'_hom_apply provable by simp.
(And I adressed @Matthew Ballards concern)

[Joël Riou]

This would be even better with @[simps! hom_app inv_app] def restrictScalarsComp' instead of abbrev.

Actually, after more thinking, there are circumstances where we do not want that restrictScalarsComp'_app_hom_apply is triggered automatically (in some cases, it may lead to goals like r • x = r • x where the • on both sides are not defeq), so that we may remove the simp attribute, but the lemma is now good enough in order to be used by rw!

[Joël Riou]

After @Christian Merten's PR #11597, I have also cleaned up my PR #6845 which introduces more constructors for presheaves of modules: automation seems much better now, so that I think that this API should be considered stable enough (and this PR ready for review). I have cleaned up a little bit my construction of the presheaf of absolute differentials (draft PR #11570). Then, in order to develop relative differentials for presheaves of modules, an important construction would be that of the restriction of scalars and the extension of scalars functors for presheaves of modules (i.e. develop a new file Algebra.Category.ModuleCat.Presheaf.ChangeOfRings).