2.3 Kahler differentials
We use the following strategy to define the Kahler differentials: first, we give the universal property, and then we give a few constructions that satisfy the universal property
Let \(A\) be an \(R\)-algebra.
An \(R\)-linear derivation of \(A\) into \(M\) is a map of \(R\)-modules \(d \colon A \to M\)
The set of derivations is denoted \(\operatorname {Der}_{R}(A,M)\)
\(\operatorname {Der}_{R}(A,M)\) is an \(R\)-module.
Derivations live in \(\operatorname {Hom}_{R} (A,M)\), so all we need to check is that Leibnitz’ rule still holds after addition, which we can do explicitly.
The module of Kahler differentials \(\Omega _{A / R}\) is the \(A\)-module that represents the functor \(M \mapsto \operatorname {Der}_{R}(A,M)\) from \(A\)-modules to \(R\)-modules.
Of course as we define by universal property via representaility, it is not clear that the module exists.
The following module satisfies the universal property of \(\Omega _{R / A}\) : Take the free \(R\)-module on the symbols \(da\) for \(a \in A\), and quotient out by the relations
\(dr = 0\) for \(r \in R\)
\(d(a + a^{\prime }) = da + da^{\prime }\)
\(d(aa^{\prime }) = ada^{\prime } + a^{\prime }da\) .
We can state another version of the universal property:
The module of Kahler differentials has the following universal property: The map \(d : A \to \Omega _{A / R}\) defined by \(a \mapsto da\) is initial in the category whose objects are derivations \(\delta : A \to M\) and morphisms are diagrams
Finally, there is a second construction:
Let \(I\) be the kernel of the multiplication map \(A \otimes _{R} A \to A\). Then \(I / I^{2}\) satisfies the universal property of \(\Omega _{A / R}\)
This proof (at least in Vakil) is a bit long, uses a lot of properties of pure tensors, and I’m not sure if it’s worth it.
The following is quite important.
By \(\phi \), we mean the ring map \(R \to A\) given by the algebra structure Let \(S\) a multiplicative subset of \(A\), and let \(T\) be a multiplicative subset of \(R\) with \(\phi (T) \subset S\). Assume the following diagram commutes
We have a (canonical) isomorphism
TODO
Given a map of schemes \(X \to S\), we have a sheaf \(\Omega _{X / S}\) which globalizes the construction \(\Omega _{A / R}\).
Use the fact that \(\Omega _{A / R}\) commutes with localization plus general scheme machinery: if we have a sheaf on an affine cover that is compatible on the intersections, then we get a sheaf on the whole scheme.
\(\Omega _{X / S}\) is quasi-coherent
Use the fact that it is defined locally as a module. This is mathematically trivial but is a good stress test of “quasicoherent sheaf machinery” in Lean.
Let \(B\) be an \(A\)-algebra, and \(I\) some ideal of \(B\). Let \(C \colonequals B / I\). We have the following right-exact sequence:
If \(B\) is a finitely generated \(A\)-algebra or a localization thereof, then \(\Omega _{B/A}\) is finitely generated as a \(B\)-module.
Calculate \(\Omega _{B/A}\) for the case of a polynomial ring. Then use the conormal sequence to pass to the quotient. Finally, Kahler differentials commute with localization.
The sheaf of kahler differentials is coherent.
We will need ideal sheaves for this.
An algebraically closed field is perfect.
Is this already in lean?
A field extension \(K/k\) is separably generated if there exists a trancendence basis \(\{ x_i\} \) for \(K/k\) such that \(K\) is a separable algebraic extension of \(k(\{ x_i\} )\).
Let \(K/k\) be a perfect field extension. Then \(K\) is separably generated over \(k\).
Let \(K\) be a finitely generated (as an algebra) field extension of \(k\). Then \(\operatorname {trdeg}K/k \leq \dim \Omega _{K/k}\), with equality if (and only if) \(K\) is separably generated over \(k\).
Let \((B,\mathfrak {m},k)\) be a local ring which contains a field \(k\) isomorphic to its residue field Then the map \(\mathfrak {m} / \mathfrak {m}^{2} \to \Omega _{B / k} \otimes _{B} k\) which is the first map in the conormal right-exact sequence is an isomorphism.
Let \(A\) be a noetherian local integral domain, with residue field \(k\) and quotient field \(K\). If \(M\) is a finitely generated \(A\)-module and \(\dim _k M \otimes _A k = \dim _K M \otimes _A K = r\), then \(M\) is free of rank \(r\).
Let \((B,\mathfrak {m},k)\) be a local ring of equal characteristic. In addition, assume that \(k\) is a perfect field, and that \(B\) is a localization of a finitely generatd \(k\)-algebra. Then \(\Omega _{B / k}\) is a free \(B\)-module of rank equal to the dimension of \(B\) if and only if \(B\) is a regular local ring.
This proof uses quite a few things.
Let \(X\) be an irreducible separated scheme of finite type over an algebraically closed field \(k\). Then \(\Omega _{X / k}\) is a locally free sheaf of rank \(\dim X\) if and only if \(X\) is regular.