Relative differentials of a variety over a field

For a variety X over k, this file constructs the relative cotangent module sheaf Variety.relativeDifferentials k X. The structure morphism supplies a map from the constant k-presheaf to the structure presheaf. Objectwise Kähler differentials for this map form a presheaf of modules; sheafifying it gives an object of X.Modules.

The resulting sheaf represents k-linear derivations into module sheaves: the declarations relativeDifferentialsDesc_fac and relativeDifferentialsDesc_unique are its factorization and uniqueness properties. On every open, the presheaf before sheafification is literally the ordinary Kähler differential module. On a standard-smooth chart of relative dimension n, that module is free and has rank n.

This construction uses that the base is Spec k, so its inverse-image ring can be presented on the site of X by the constant k-presheaf. It does not fill Mathlib's more general TODO for relative differentials of an arbitrary morphism of ringed spaces. The companion Canonical.Descent module passes the objectwise standard-smooth calculation through sheafification, constructs the global finite-locally-free atlas and determinant line, and exposes the automatic constructor CanonicalSheafData.ofSmoothRelativeDifferentials.

noncomputable def AlgebraicGeometry.Variety.baseFieldPresheaf (k : Type u) [Field k] (X : Scheme) : CategoryTheory.Functor X.Opensᵒᵖ CommRingCat

The constant base-field presheaf on the opens of a variety.

Equations

• AlgebraicGeometry.Variety.baseFieldPresheaf k X = (CategoryTheory.Functor.const X.Opensᵒᵖ).obj (CommRingCat.of k)

noncomputable def AlgebraicGeometry.Variety.baseFieldToGlobalSections (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : k →+* ↑(X.presheaf.obj (Opposite.op ⊤))

The map from the base field to global functions induced by the structure morphism.

Equations

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

noncomputable def AlgebraicGeometry.Variety.baseFieldToStructurePresheaf (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : baseFieldPresheaf k X ⟶ X.presheaf

The structure morphism, presented as a map from the constant base-field presheaf to the structure presheaf of X.

Equations

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

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsPresheaf (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : X.PresheafOfModules

The presheaf whose value on U is the Kähler differential module of k → Γ(U, 𝒪_X).

Equations

• AlgebraicGeometry.Variety.relativeDifferentialsPresheaf k X = PresheafOfModules.DifferentialsConstruction.relativeDifferentials' (AlgebraicGeometry.Variety.baseFieldToStructurePresheaf k X)

noncomputable def AlgebraicGeometry.Variety.relativeDifferentials (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : X.Modules

The relative cotangent sheaf Ω¹_{X/k}, obtained by sheafifying the objectwise Kähler differential presheaf.

Equations

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

noncomputable def AlgebraicGeometry.Variety.relativeDerivationPresheaf (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : PresheafOfModules.Derivation' (relativeDifferentialsPresheaf k X) (baseFieldToStructurePresheaf k X)

The objectwise universal derivation into the relative-differentials presheaf.

Equations

• AlgebraicGeometry.Variety.relativeDerivationPresheaf k X = PresheafOfModules.DifferentialsConstruction.derivation' (AlgebraicGeometry.Variety.baseFieldToStructurePresheaf k X)

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsSheafification (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : relativeDifferentialsPresheaf k X ⟶ (SheafOfModules.forget X.ringCatSheaf).obj (relativeDifferentials k X)

The sheafification unit from the objectwise Kähler differential presheaf to the underlying presheaf of the relative cotangent sheaf.

Equations

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

noncomputable def AlgebraicGeometry.Variety.relativeDerivation (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] : ((SheafOfModules.forget X.ringCatSheaf).obj (relativeDifferentials k X)).Derivation' (baseFieldToStructurePresheaf k X)

The universal k-linear derivation 𝒪_X → Ω¹_{X/k}.

Equations

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

noncomputable def AlgebraicGeometry.Variety.relativeDifferentialsDesc (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (M : X.Modules) (d : ((SheafOfModules.forget X.ringCatSheaf).obj M).Derivation' (baseFieldToStructurePresheaf k X)) : relativeDifferentials k X ⟶ M

A k-linear derivation from 𝒪_X into a module sheaf descends to a morphism from Ω¹_{X/k}.

Equations

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

theorem AlgebraicGeometry.Variety.relativeDifferentialsDesc_fac (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (M : X.Modules) (d : ((SheafOfModules.forget X.ringCatSheaf).obj M).Derivation' (baseFieldToStructurePresheaf k X)) : PresheafOfModules.Derivation.postcomp (relativeDerivation k X) ((SheafOfModules.forget X.ringCatSheaf).map (relativeDifferentialsDesc k X M d)) = d

The morphism descended from a derivation factors the universal derivation as prescribed.

theorem AlgebraicGeometry.Variety.relativeDifferentialsDesc_unique (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (M : X.Modules) (d : ((SheafOfModules.forget X.ringCatSheaf).obj M).Derivation' (baseFieldToStructurePresheaf k X)) (f : relativeDifferentials k X ⟶ M) (hf : PresheafOfModules.Derivation.postcomp (relativeDerivation k X) ((SheafOfModules.forget X.ringCatSheaf).map f) = d) : f = relativeDifferentialsDesc k X M d

The morphism descended from a derivation is unique.

theorem AlgebraicGeometry.Variety.relativeDifferentials_hom_ext (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (M : X.Modules) (f g : relativeDifferentials k X ⟶ M) (h : PresheafOfModules.Derivation.postcomp (relativeDerivation k X) ((SheafOfModules.forget X.ringCatSheaf).map f) = PresheafOfModules.Derivation.postcomp (relativeDerivation k X) ((SheafOfModules.forget X.ringCatSheaf).map g)) : f = g

Morphisms from Ω¹_{X/k} are determined by their composites with the universal derivation.

@[simp]

theorem AlgebraicGeometry.Variety.relativeDifferentialsPresheaf_obj (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (U : X.Opensᵒᵖ) : (relativeDifferentialsPresheaf k X).obj U = CommRingCat.KaehlerDifferential ((baseFieldToStructurePresheaf k X).app U)

Before sheafification, the relative differentials on an open are exactly the ordinary Kähler differential module of its ring of functions over k.

@[simp]

theorem AlgebraicGeometry.Variety.relativeDerivationPresheaf_d (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] {U : X.Opensᵒᵖ} (x : ↑(X.presheaf.obj U)) : (relativeDerivationPresheaf k X).d x = CommRingCat.KaehlerDifferential.d x

The presheaf universal derivation is objectwise the ordinary Kähler derivation.

theorem AlgebraicGeometry.Variety.relativeDifferentialsPresheaf_obj_free (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (U : X.Opensᵒᵖ) (n : ℕ) (h : RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom ((baseFieldToStructurePresheaf k X).app U))) : Module.Free ↑(X.presheaf.obj U) ↑(CommRingCat.KaehlerDifferential ((baseFieldToStructurePresheaf k X).app U))

On a standard-smooth affine chart, the objectwise relative differential module is free.

theorem AlgebraicGeometry.Variety.relativeDifferentialsPresheaf_obj_rank (k : Type u) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] (U : X.Opensᵒᵖ) (n : ℕ) (h : RingHom.IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom ((baseFieldToStructurePresheaf k X).app U))) [Nontrivial ↑(X.presheaf.obj U)] : Module.rank ↑(X.presheaf.obj U) ↑(CommRingCat.KaehlerDifferential ((baseFieldToStructurePresheaf k X).app U)) = ↑n

On a standard-smooth affine chart of relative dimension n, objectwise relative differentials have rank n.

noncomputable def AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.ofRelativeDifferentials {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (hSmooth : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) (D : (Variety.relativeDifferentials k X).DeterminantData) (hrank : D.rank = n) : CanonicalSheafData k X n

Build canonical-sheaf data using the constructed relative cotangent sheaf.

This low-level constructor retains explicit determinant data for callers with a chosen trivialization. The companion Canonical.Descent module provides the automatic constructor ofSmoothRelativeDifferentials from the smooth pure-dimension certificate alone.

Equations

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

@[simp]

theorem AlgebraicGeometry.SmoothProperVariety.CanonicalSheafData.ofRelativeDifferentials_cotangent {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] {n : ℕ} (hSmooth : SmoothOfRelativeDimension n (X ↘ Spec (CommRingCat.of k))) (D : (Variety.relativeDifferentials k X).DeterminantData) (hrank : D.rank = n) : (ofRelativeDifferentials hSmooth D hrank).cotangent = Variety.relativeDifferentials k X

The cotangent field of ofRelativeDifferentials is the constructed relative cotangent sheaf.