The rank of the sheaf of relative differentials

For a scheme X smooth of relative dimension n over Spec R, the sheaf of relative differentials Ω_{X/R} is finite locally free of rank n at every point. Around each point, X has an affine open W whose ring of functions is a standard smooth R-algebra of relative dimension n, so that its module of Kähler differentials is free of rank n; on W the sheaf Ω_{X/R} is the sheaf associated with that module.

When X is smooth of relative dimension one over Spec R, as a smooth curve over a field is, Ω_{X/R} is therefore an invertible sheaf.

Main declarations

• TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_relativeDifferentials_apply: the finite locally free sheaf FiniteLocallyFreeSheaf.relativeDifferentials R X has rank n everywhere when X is smooth of relative dimension n;
• TauCeti.AlgebraicGeometry.isInvertible_relativeDifferentials and TauCeti.AlgebraicGeometry.InvertibleSheaf.relativeDifferentials: in relative dimension one it is an invertible sheaf.

References

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

theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_relativeDifferentials_apply (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n (X ↘ AlgebraicGeometry.Spec ↧R)] (x : ↥X) : (relativeDifferentials R X).rank x = n

On a scheme smooth of relative dimension n over Spec R, the sheaf of relative differentials has rank n at every point.

theorem TauCeti.AlgebraicGeometry.isInvertible_relativeDifferentials (R : Type u) [CommRing R] {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧R)] [AlgebraicGeometry.SmoothOfRelativeDimension 1 (X ↘ AlgebraicGeometry.Spec ↧R)] : SheafOfModules.isInvertible X (AlgebraicGeometry.Scheme.relativeDifferentials R X)

On a scheme smooth of relative dimension one over Spec R, the sheaf of relative differentials is invertible.

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

The sheaf of relative differentials of a scheme smooth of relative dimension one over Spec R, as an invertible sheaf.

Equations

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

@[simp]

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

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