Quasi-coherence and finite presentation of relative differentials

The relative differentials of any scheme over a commutative ring are quasi-coherent. On an affine open, the restriction comparison identifies them with the sheaf associated to the module of Kähler differentials of its coordinate ring. The resulting local presentations give quasi-coherence on the whole scheme. If the structure morphism is locally of finite presentation, the same comparisons give finite presentation of the differential sheaf. No Noetherian, properness, or smoothness assumption is needed.

On global sections over an affine open U, the same comparisons identify Γ(Ω_{X/R}, U) with the module of Kähler differentials Ω[Γ(X, U)⁄R], matching d a with D a. In particular, if X is locally of finite type over Spec R, these modules of sections are finitely generated, which is the finiteness needed to form the Fitting ideal sheaves of Ω_{X/R}.

Main declarations

• TauCeti.AlgebraicGeometry.isQuasicoherent_relativeDifferentials: Ω_{X/R} is quasi-coherent;
• TauCeti.AlgebraicGeometry.isFinitePresentation_relativeDifferentials: Ω_{X/R} is finitely presented when X is locally of finite presentation over Spec R;
• TauCeti.AlgebraicGeometry.relativeDifferentialsSectionsEquiv: over an affine open U, Ω[Γ(X, U)⁄R] ≃ Γ(Ω_{X/R}, U), characterized by TauCeti.AlgebraicGeometry.relativeDifferentialsSectionsEquiv_D;
• TauCeti.AlgebraicGeometry.finite_relativeDifferentials_sections: these modules of sections are finitely generated when X is locally of finite type over Spec R.

References

• The Stacks Project, Section 29.33, Lemmas 29.33.3 and 29.33.5 (Tag 01UM).
• R. Hartshorne, Algebraic Geometry, Section II.8.

instance TauCeti.AlgebraicGeometry.isQuasicoherent_relativeDifferentials (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] : SheafOfModules.IsQuasicoherent (AlgebraicGeometry.Scheme.relativeDifferentials R X)

The sheaf of relative differentials of a scheme over Spec R is quasi-coherent.

instance TauCeti.AlgebraicGeometry.isFinitePresentation_relativeDifferentials (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.LocallyOfFinitePresentation (X ↘ AlgebraicGeometry.Spec ↧R)] : SheafOfModules.IsFinitePresentation (AlgebraicGeometry.Scheme.relativeDifferentials R X)

Relative differentials of a scheme locally of finite presentation over Spec R are finitely presented as a sheaf of modules.

theorem TauCeti.AlgebraicGeometry.finiteType_sections_of_locallyOfFiniteType (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧R)] (U : ↑X.affineOpens) : Algebra.FiniteType R ↑(X.presheaf.obj (Opposite.op ↑U))

If X is locally of finite type over Spec R, then the ring of functions Γ(X, U) on every affine open U is a finitely generated R-algebra.

noncomputable def TauCeti.AlgebraicGeometry.relativeDifferentialsSectionsEquiv (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] (U : ↑X.affineOpens) : Ω[↑(X.presheaf.obj (Opposite.op ↑U))⁄R] ≃ₗ[↑(X.presheaf.obj (Opposite.op ↑U))] ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op ↑U))

Over an affine open U, the sections of the sheaf of relative differentials are the Kähler differentials of the ring of functions: Ω[Γ(X, U)⁄R] ≃ Γ(Ω_{X/R}, U), sending D a to d a (relativeDifferentialsSectionsEquiv_D).

Equations

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

@[simp]

theorem TauCeti.AlgebraicGeometry.relativeDifferentialsSectionsEquiv_D (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] (U : ↑X.affineOpens) (a : ↑(X.presheaf.obj (Opposite.op ↑U))) : (relativeDifferentialsSectionsEquiv R X U) ((KaehlerDifferential.D R ↑(X.presheaf.obj (Opposite.op ↑U))) a) = (AlgebraicGeometry.Scheme.universalDerivation R X).d a

The identification Ω[Γ(X, U)⁄R] ≃ Γ(Ω_{X/R}, U) sends the Kähler differential D a of a function a on U to its differential d a.

instance TauCeti.AlgebraicGeometry.finite_relativeDifferentials_sections (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧R)] (U : ↑X.affineOpens) : Module.Finite ↑(X.presheaf.obj (Opposite.op ↑U)) ↑((AlgebraicGeometry.Scheme.relativeDifferentials R X).presheaf.obj (Opposite.op ↑U))

If X is locally of finite type over Spec R, the sections of Ω_{X/R} over every affine open U form a finitely generated Γ(X, U)-module.