Stalks of relative differentials

For a scheme X over a commutative ring R, the stalk of the sheaf of relative differentials at x is canonically the module of Kähler differentials of the local ring 𝒪_{X,x} over R. The comparison sends the germ of d a to the differential of the germ of a, and its inverse has the corresponding computation rule. No finiteness, smoothness, or integrality assumption is needed. This comparison connects local-ring regularity criteria for rational differentials with the sheaf of differentials used to represent the canonical line bundle.

References

• The Stacks Project, Lemma 17.28.7, Tag 08TE.

noncomputable def AlgebraicGeometry.Scheme.relativeDifferentialsStalkEquiv (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (x : ↥X) : ↑((relativeDifferentials R X).presheaf.stalk x) ≃ₗ[↑(X.presheaf.stalk x)] Ω[↑(X.presheaf.stalk x)⁄R]

The stalk of relative differentials is canonically the Kähler differential module of the local ring over the base ring. The base algebra is the canonical Scheme.stalkBaseAlgebra.

Equations

• AlgebraicGeometry.Scheme.relativeDifferentialsStalkEquiv R X x = LinearEquiv.ofLinearMap (TauCeti.AlgebraicGeometry.stalkMap✝ R X x) (TauCeti.AlgebraicGeometry.stalkInv✝ R X x) ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.relativeDifferentialsStalkEquiv_germ_d (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (x : ↥X) (U : X.Opens) (hx : x ∈ U) (a : ↑(X.presheaf.obj (Opposite.op U))) : (relativeDifferentialsStalkEquiv R X x) ((CategoryTheory.ConcreteCategory.hom ((relativeDifferentials R X).presheaf.germ U x hx)) ((universalDerivation R X).d a)) = (KaehlerDifferential.D R ↑(X.presheaf.stalk x)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) a)

The stalk comparison sends the germ of a differential to the differential of the germ.

@[simp]

theorem AlgebraicGeometry.Scheme.relativeDifferentialsStalkEquiv_symm_D_germ (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (x : ↥X) (U : X.Opens) (hx : x ∈ U) (a : ↑(X.presheaf.obj (Opposite.op U))) : (relativeDifferentialsStalkEquiv R X x).symm ((KaehlerDifferential.D R ↑(X.presheaf.stalk x)) ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) a)) = (CategoryTheory.ConcreteCategory.hom ((relativeDifferentials R X).presheaf.germ U x hx)) ((universalDerivation R X).d a)

The inverse stalk comparison sends the differential of a germ to the germ of a differential.