Finite local freeness of smooth relative differentials

For a smooth scheme over an affine base, its sheaf of relative differentials is finite locally free. On an affine chart the differential sheaf is the sheaf associated with the Kähler module, which is finite projective for a smooth algebra. The open-cover criterion for finite local freeness then gives the result on the whole scheme.

This produces the cotangent bundle of a smooth scheme without any Noetherian or field hypothesis, packaged as the finite locally free sheaf FiniteLocallyFreeSheaf.relativeDifferentials. For a smooth curve, identifying its rank as one is the further step needed to regard the differential sheaf as the canonical line bundle.

References

• The Stacks Project, Morphisms of Schemes, Lemma 29.34.12 (Tag 02G1).
• R. Hartshorne, Algebraic Geometry, Section II.8.

theorem TauCeti.AlgebraicGeometry.isFiniteLocallyFree_relativeDifferentials_spec (R : Type u) [CommRing R] (A : Type u) [CommRing A] [Algebra R A] [Algebra.Smooth R A] : AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree (AlgebraicGeometry.Spec ↧A) (AlgebraicGeometry.Scheme.relativeDifferentials R (AlgebraicGeometry.Spec ↧A))

The differential sheaf of the spectrum of a smooth algebra is finite locally free.

theorem TauCeti.AlgebraicGeometry.isFiniteLocallyFree_relativeDifferentials (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.Smooth (X ↘ AlgebraicGeometry.Spec ↧R)] : AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree X (AlgebraicGeometry.Scheme.relativeDifferentials R X)

Relative differentials of a scheme smooth over Spec R are finite locally free.

instance TauCeti.AlgebraicGeometry.isLocallyFree_relativeDifferentials (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.Smooth (X ↘ AlgebraicGeometry.Spec ↧R)] : SheafOfModules.IsLocallyFree (AlgebraicGeometry.Scheme.relativeDifferentials R X)

The sheaf of relative differentials of a smooth scheme is locally free.

noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.relativeDifferentials (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.Smooth (X ↘ AlgebraicGeometry.Spec ↧R)] : FiniteLocallyFreeSheaf X

The sheaf of relative differentials of a scheme smooth over Spec R, as a finite locally free sheaf.

Equations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.relativeDifferentials R X = { obj := AlgebraicGeometry.Scheme.relativeDifferentials R X, property := ⋯ }

@[simp]

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.relativeDifferentials_obj (R : Type u) [CommRing R] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.Smooth (X ↘ AlgebraicGeometry.Spec ↧R)] : (relativeDifferentials R X).obj = AlgebraicGeometry.Scheme.relativeDifferentials R X

The underlying sheaf of FiniteLocallyFreeSheaf.relativeDifferentials R X is Ω_{X/R}.