Kahler differentials

Stream: maths

[Riccardo Brasca]

Is anyone working on the definition of the module of Kahler differentials? If not I would like to do it.

[Riccardo Brasca]

This is needed to define unramified morphisms and so for étale morphisms.

[Johan Commelin]

@Kenny Lau had a rough definition at some point

[Kenny Lau]

it was abandoned due to #4773

[Riccardo Brasca]

Do you mean we should wait to have a better theory of base change?

[Riccardo Brasca]

The definition using the universal property should not be too complicated I guess

[Kenny Lau]

I wanted to build it as a quotient of $A \otimes_R A$ (where $x \otimes y$ represents $x ~ \mathrm dy$)

[Riccardo Brasca]

I see. Do you have any reasons to prefer that definition? I am not very familiar with using universal properties in Lean, so maybe it more complicated than I think

[Kenny Lau]

No.

[Kenny Lau]

I posted the code here somewhere, somehow I can't find it....

[Riccardo Brasca]

Looking for "kahler" I only find this topic... btw if you are not interested in it I will give it a try using derivations and the universal property

[Riccardo Brasca]

I have some teaching to do this quarter, so I will be quite slow, but I guess we are not in a hurry :smile:

[Johan Commelin]

There is this thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/derivation/near/170730598
But I didn't find Kenny's code there

[Kenny Lau]

thanks, it's at the top of the thread

[Kenny Lau]

it's the first three messages

[Johan Commelin]

aah, I didn't know that was the code you had in mind (-;

[Johan Commelin]

didn't look close enough

[Riccardo Brasca]

We don't have free modules and quotient modules? I mean something like free_algebra and ring_quot.algebra

[Kenny Lau]

the free module over R generated by set S is just S ->0 R (finsupp)

[Kenny Lau]

docs#finsupp

[Johan Commelin]

@Riccardo Brasca also submodule.quotient

[Riccardo Brasca]

Thank's! I will think about it: if I understand the other topic, the actual definition is not a big deal, but we need to have a reasonable condition to check that a module is the module of differentials

[Riccardo Brasca]

I think I am missing something here: what is the problem with defining $\Omega^1_{S/R}$ using the quotient of the free module and then saying that $(M,d)$ is isomorphic to $\Omega^1_{S/R}$ if and only if for any $R$-module $N$ and any $R$-derivation $e \colon S \to N$ there is a unique $\varphi \colon M \to N$ such that $e = \varphi \circ d$? It is the fact that we do not want to quantify over all modules because of some universes issue?

[Johan Commelin]

yes, that last point is a bit annoying... you'll have a version of $\Omega_{S/R}^1$ that works for derivations to $N : \text{Type u}$, but not for derivations $N : \text{Type v}$...

[Johan Commelin]

so if you can find an internal description, that's usually prefered

[Riccardo Brasca]

I see, this would work only in a fixed universe, that is quite unpleasant.

[Kevin Buzzard]

Amelia ran into this with the explicit construction of the tensor algebra as $R\oplus M\oplus M^{\otimes 2}\oplus\cdots$. We tried ulift for about 2 minutes but when Lean couldn't fnd a ring structure on ulift R given one on R I decided it was a bad omen, and suggested that she just stuck to rings and modules in the same universe.

Here is an example I could see in the future where a ring and a module might not be in the same universe. If we do etale cohomology in a lazy way, without keeping track of set-theoretic issues, then etale cohomology will be defined as a limit along something which isn't a set, so if $X$ is a scheme in universe u then its etale cohoology might be in universe $u+1$. So you could imagine $H^2(\mathbb{P}^1,\mathbb{Z}_\ell)$ being an abelian group in Type 1 and you might then want to make it a module over int, which is in Type 0.

[Kevin Buzzard]

But perhaps the best fix in this case is to actually prove that the limit can be taken over a reasonable object We jumped through some hoops like this in the perfectoid project when dealing with the issue that equivalence classes of valuations on a ring were not sets.

[Kevin Buzzard]

If R : Type u and M : Type v and N : Type w, is $M\otimes_R N$ in Type max u v w? Does Lean know universe max is commutative and associative?

[Riccardo Brasca]

Apparently the tensor product is of type Type max v w, without reference to the type of R. I have no idea about what Lean knows about max.

[Jack J Garzella]

@Riccardo Brasca has there been any progress on this?

[Riccardo Brasca]

I don't think so, but I would be very happy to be proven wrong. What we are really missing is a characteristic predicate.

[Joël Riou]

A similar question arises with the localization of categories. If we were to apply to Kähler differentials the same approach I am suggesting in the TODO section of PR #14422, we could define the module $\Omega^1_{S/R}$ by taking the obvious quotient of a free module, so that we have a differential $d₀ : S ⟶ \Omega^1_{S/R}$. Then, we can prove that this d₀ satisfies the universal property for all differentials d₁ : S ⟶ M₁ regardless of the universe of M₁. Then, one may define the predicate is_kahler_differential d₁ by saying that the canonical map $\Omega^1_{S/R} ⟶ M₁$ is an isomorphism. Then, when the predicate is satisfied, using what we know for d₀, it is easy to get that the tuple (d₁, M₁) is also universal (for differentials d₂ : S ⟶ M₂ with M₂ in any universe). Practically speaking, in order to verify is_kahler_differential d₁, one would have to prove the universal property of d₁ with respect to two different d : S ⟶ N: d₀ and d₁.

[Andrew Yang]

I did not now this topic exists! I am planning on implementing the module of differentials as a subquotient of $S \otimes_R S$ if no one else is working towards this. The characteristic predicate is not in my plan, but I believe the approach Joël mentioned is a good option; I am also following this pattern when doing the characteristic predicate of tensor products.

[Kevin Buzzard]

I would have thought that the definition as a quotient module was much easier to work with. Why go for the $I/I^2$ version? I'd be tempted to do that later...

[Andrew Yang]

I think taking the quotient of the free module over R generated by S × S is a bit like redoing the tensor product api but with slightly different relations? I would assume it would be a pain to even show that it is an S-module.
OTOH, I think there wouldn't be a huge difference in working on the two once we know that the module is generated by $ds$.

[Joël Riou]

Actually, it would be a quotient of the free module over S generated by the ds for all s : S: it is not that weird.

[Andrew Yang]

Ah yes of course. I'll try this as well then.

[Jack J Garzella]

Another idea about the predicate, which I haven't yet had time to pursue, is that $\Omega_{S/R}^1$ represents the functor $M \mapsto \text{Der}_R(S,M)$ (See Cutkosky's Introduction to Algebraic Geometry, Lemma 14.3). This should be mathematically equivalent to the universal property, but perhaps it's more universe-friendly as I would imagine $\text{Der}_R(S,M)$ has type $Type (max u v)$ or something.

[Joël Riou]

I do not think so. Mathematically speaking, it does not make a significant difference to say that $\text{Der}_R(S,M)$ functorialy identifies to $\Omega_{S/R}^1 ⟶ M$ for all M or to say that for any M and any R-derivation d : S ⟶ M there exists a unique linear map $f:\Omega_{S/R}^1 ⟶ M$ such that d is obtained by composing the universal derivation and f.

In Lean, (it seems) we have to quantify on objects of a certain universe. Your approach suggests using the categories Module R, but they have universe parameters: they are actually Module.{w} R for all universes w. Morphisms in these categories make sense only if the modules are in the same universe. It might be possible to use "inclusions" Module.{w} R ⥤ Module.{w'} R when w' is bigger than w, but it looks more complicated than what was suggested above.

[Kevin Buzzard]

My instinct when lean says "these two objects now need to go in the same universe" is "well five years ago I didn't even believe in universes so that's fine"