## Stream: maths

### Topic: Kahler differentials

#### 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.

#### Riccardo Brasca (Jan 13 2021 at 15:08):

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

#### Johan Commelin (Jan 13 2021 at 15:10):

@Kenny Lau had a rough definition at some point

#### Kenny Lau (Jan 13 2021 at 15:10):

it was abandoned due to #4773

#### Riccardo Brasca (Jan 13 2021 at 15:16):

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

#### Riccardo Brasca (Jan 13 2021 at 15:17):

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

#### Kenny Lau (Jan 13 2021 at 15:20):

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

#### 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

No.

#### Kenny Lau (Jan 13 2021 at 15:37):

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

#### 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

#### 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:

#### Johan Commelin (Jan 13 2021 at 15:42):

But I didn't find Kenny's code there

#### Kenny Lau (Jan 13 2021 at 15:42):

thanks, it's at the top of the thread

#### Kenny Lau (Jan 13 2021 at 15:43):

it's the first three messages

#### Johan Commelin (Jan 13 2021 at 15:45):

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

#### Johan Commelin (Jan 13 2021 at 15:45):

didn't look close enough

#### 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

#### Kenny Lau (Jan 13 2021 at 15:59):

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

docs#finsupp

#### Johan Commelin (Jan 13 2021 at 16:01):

@Riccardo Brasca also submodule.quotient

#### 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

#### Riccardo Brasca (Jan 14 2021 at 13:30):

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 (Jan 14 2021 at 13:32):

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 (Jan 14 2021 at 13:33):

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

#### Riccardo Brasca (Jan 14 2021 at 13:36):

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

#### Kevin Buzzard (Jan 14 2021 at 13:44):

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 (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.

#### Kevin Buzzard (Jan 14 2021 at 13:48):

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 (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