Zulip Chat Archive

Stream: maths

Topic: Kahler differentials


view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:08):

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

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:08):

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

view this post on Zulip Johan Commelin (Jan 13 2021 at 15:10):

@Kenny Lau had a rough definition at some point

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:10):

it was abandoned due to #4773

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:16):

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

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:17):

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

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:20):

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

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:28):

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

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:32):

No.

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:37):

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

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:40):

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

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:41):

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

view this post on Zulip Johan Commelin (Jan 13 2021 at 15:42):

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

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:42):

thanks, it's at the top of the thread

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:43):

it's the first three messages

view this post on Zulip Johan Commelin (Jan 13 2021 at 15:45):

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

view this post on Zulip Johan Commelin (Jan 13 2021 at 15:45):

didn't look close enough

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 15:51):

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

view this post on Zulip Kenny Lau (Jan 13 2021 at 15:59):

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

view this post on Zulip Kenny Lau (Jan 13 2021 at 16:00):

docs#finsupp

view this post on Zulip Johan Commelin (Jan 13 2021 at 16:01):

@Riccardo Brasca also submodule.quotient

view this post on Zulip Riccardo Brasca (Jan 13 2021 at 16:07):

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

view this post on Zulip Riccardo Brasca (Jan 14 2021 at 13:30):

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

view this post on Zulip Johan Commelin (Jan 14 2021 at 13:32):

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

view this post on Zulip Johan Commelin (Jan 14 2021 at 13:33):

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

view this post on Zulip Riccardo Brasca (Jan 14 2021 at 13:36):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 13:44):

Amelia ran into this with the explicit construction of the tensor algebra as RMM2R\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 XX is a scheme in universe u then its etale cohoology might be in universe u+1u+1. So you could imagine H2(P1,Z)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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 13:46):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 13:48):

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

view this post on Zulip Riccardo Brasca (Jan 14 2021 at 14:03):

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.


Last updated: May 12 2021 at 07:17 UTC