The sheaf of relative differentials of a scheme over a ring

Let X be a scheme over a commutative ring R, that is, over Spec R. The sheaf of relative Kähler differentials Ω_{X/R} is the sheaf of 𝒪_X-modules associated to the presheaf U ↦ Ω[Γ(X, U)⁄R], and it carries the universal R-derivation d : 𝒪_X ⟶ Ω_{X/R}. For a smooth curve over a field k, Ω_{X/k} is the relative dualizing sheaf ω_{X/k} of Serre duality; in general it is the first object of the cotangent formalism of X over R.

The construction follows Mathlib's presheaf of relative differentials PresheafOfModulesOfCommRing.DifferentialsConstruction.relativeDifferentials' of a morphism of presheaves of commutative rings, applied to the morphism Scheme.baseRingToStructurePresheaf from the constant presheaf R to the structure presheaf 𝒪_X, followed by sheafification of presheaves of modules. Since sheafification is left adjoint to the inclusion of sheaves of modules, the universal property of the presheaf of differentials passes to the sheaf: morphisms Ω_{X/R} ⟶ M to a sheaf of 𝒪_X-modules correspond to R-derivations 𝒪_X ⟶ M, by composition with d.

The base is the affine scheme Spec R, which covers varieties over a field. Over a general base scheme S the constant presheaf R would be replaced by the inverse image of 𝒪_S.

Main declarations

• AlgebraicGeometry.Scheme.Modules.Derivation R M: the R-derivations of 𝒪_X with values in a sheaf of 𝒪_X-modules M;

• AlgebraicGeometry.Scheme.relativeDifferentials R X: the sheaf Ω_{X/R} of relative differentials;

• AlgebraicGeometry.Scheme.universalDerivation R X: the universal derivation d : 𝒪_X ⟶ Ω_{X/R};

• AlgebraicGeometry.Scheme.relativeDifferentialsHomEquiv R X M: the universal property (Ω_{X/R} ⟶ M) ≃ M.Derivation R, with AlgebraicGeometry.Scheme.relativeDifferentials_hom_ext the corresponding uniqueness statement.

• TauCeti.AlgebraicGeometry.globalDerivation R A: the global component of a derivation on Spec A, viewed as an R-derivation of A.

References

• The Stacks Project, Tag 01UM (differentials of a morphism of ringed spaces), in particular Lemma 01UP describing them as the sheafification of U ↦ Ω_{𝒪_X(U)/R}.
• R. Hartshorne, Algebraic Geometry, Section II.8.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Modules.Derivation (R : Type u) [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] (M : X.Modules) : Type u

The R-derivations of the structure sheaf of a scheme X over R with values in a sheaf of 𝒪_X-modules M: compatible families of R-linear derivations Γ(X, U) → Γ(M, U).

Equations

• AlgebraicGeometry.Scheme.Modules.Derivation R M = PresheafOfModulesOfCommRing.Derivation' M.val (AlgebraicGeometry.Scheme.baseRingToStructurePresheaf R X)

noncomputable def AlgebraicGeometry.Scheme.presheafRelativeDifferentials (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] : PresheafOfModulesOfCommRing X.presheaf

The presheaf U ↦ Ω[Γ(X, U)⁄R] of relative differentials of a scheme X over R, as a presheaf of 𝒪_X-modules. Its sheafification is Scheme.relativeDifferentials R X.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.relativeDifferentials (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] : X.Modules

The sheaf of relative differentials Ω_{X/R} of a scheme X over a commutative ring R: the sheafification of the presheaf U ↦ Ω[Γ(X, U)⁄R] of Kähler differentials.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.universalDerivation (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] : Modules.Derivation R (relativeDifferentials R X)

The universal R-derivation d : 𝒪_X ⟶ Ω_{X/R}: on sections over U, the Kähler differential Γ(X, U) → Ω[Γ(X, U)⁄R] followed by the sheafification map.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.relativeDifferentialsHomEquiv (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] (M : X.Modules) : (relativeDifferentials R X ⟶ M) ≃ Modules.Derivation R M

The universal property of the sheaf of relative differentials: morphisms Ω_{X/R} ⟶ M of sheaves of 𝒪_X-modules correspond to R-derivations of 𝒪_X with values in M, by composition with the universal derivation.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.relativeDifferentialsHomEquiv_apply (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M : X.Modules} (f : relativeDifferentials R X ⟶ M) : (relativeDifferentialsHomEquiv R X M) f = PresheafOfModulesOfCommRing.Derivation.postcomp (universalDerivation R X) f.val

The derivation corresponding to a morphism f : Ω_{X/R} ⟶ M is the universal derivation followed by f.

@[simp]

theorem AlgebraicGeometry.Scheme.relativeDifferentialsHomEquiv_symm_fac (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M : X.Modules} (D : Modules.Derivation R M) : PresheafOfModulesOfCommRing.Derivation.postcomp (universalDerivation R X) ((relativeDifferentialsHomEquiv R X M).symm D).val = D

Every R-derivation of 𝒪_X with values in M is the universal derivation followed by the corresponding morphism Ω_{X/R} ⟶ M.

theorem AlgebraicGeometry.Scheme.relativeDifferentialsHomEquiv_comp (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M N : X.Modules} (f : relativeDifferentials R X ⟶ M) (g : M ⟶ N) : (relativeDifferentialsHomEquiv R X N) (CategoryTheory.CategoryStruct.comp f g) = PresheafOfModulesOfCommRing.Derivation.postcomp ((relativeDifferentialsHomEquiv R X M) f) g.val

The universal property of Ω_{X/R} is natural in the target module.

theorem AlgebraicGeometry.Scheme.relativeDifferentials_hom_ext (R : Type u) [CommRing R] (X : Scheme) [X.Over (Spec ↧R)] {M : X.Modules} {f g : relativeDifferentials R X ⟶ M} (h : ∀ (U : X.Opensᵒᵖ) (a : ↑(X.presheaf.obj U)), (CategoryTheory.ConcreteCategory.hom (f.val.app U)) ((universalDerivation R X).d a) = (CategoryTheory.ConcreteCategory.hom (g.val.app U)) ((universalDerivation R X).d a)) : f = g

Two morphisms out of Ω_{X/R} agree as soon as they agree on the differentials d a of all local sections a of 𝒪_X.

theorem AlgebraicGeometry.Scheme.relativeDifferentials_hom_ext_iff {R : Type u} [CommRing R] {X : Scheme} [X.Over (Spec ↧R)] {M : X.Modules} {f g : relativeDifferentials R X ⟶ M} : f = g ↔ ∀ (U : X.Opensᵒᵖ) (a : ↑(X.presheaf.obj U)), (CategoryTheory.ConcreteCategory.hom (f.val.app U)) ((universalDerivation R X).d a) = (CategoryTheory.ConcreteCategory.hom (g.val.app U)) ((universalDerivation R X).d a)

noncomputable def TauCeti.AlgebraicGeometry.globalDerivation (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] {M : (AlgebraicGeometry.Spec A).Modules} (d : AlgebraicGeometry.Scheme.Modules.Derivation R M) : Derivation R ↑A ↑(M.presheaf.obj (Opposite.op ⊤))

The R-derivation A → Γ(M, ⊤) given by the global component of a derivation of 𝒪_{Spec A}.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AlgebraicGeometry.globalDerivation_apply (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] {M : (AlgebraicGeometry.Spec A).Modules} (d : AlgebraicGeometry.Scheme.Modules.Derivation R M) (a : ↑A) : (globalDerivation R A d) a = d.d ((algebraMap ↑A ↑((AlgebraicGeometry.Spec A).presheaf.obj (Opposite.op ⊤))) a)

Evaluating the global component of a sheaf derivation at a : A amounts to evaluating that derivation on the corresponding global function.