Relative differentials of an affine scheme #

Let A be an algebra over a commutative ring R. The sheaf of relative differentials of Spec A over R is the quasi-coherent sheaf associated with the module of Kähler differentials: Ω_{Spec A/R} ≅ Ω[A⁄R]~, with d a ↦ D a on the sections coming from A. In particular Ω_{Spec A/R} is quasi-coherent, and its global sections are the Kähler differentials Ω[A⁄R]. This is the local computation behind the identification of Ω_{X/k} with a line bundle on a smooth curve X over a field k.

Both sheaves carry an R-derivation of 𝒪_{Spec A}, and the isomorphism compares them.

The sheaf Ω[A⁄R]~ receives a derivation 𝒪_{Spec A} → Ω[A⁄R]~ extending D : A → Ω[A⁄R]. On a basic open D(f) the ring of sections is the localization A_f, and D extends uniquely to A_f by the quotient rule (Derivation.extendOfIsLocalization). By uniqueness these extensions are compatible with restriction, so they glue along the basis of basic opens. The universal property of Ω_{Spec A/R} turns this derivation into a morphism Ω_{Spec A/R} ⟶ Ω[A⁄R]~.
Conversely, the global component of the universal derivation is an R-derivation A → Γ(Spec A, Ω_{Spec A/R}). It corresponds to an A-linear map Ω[A⁄R] → Γ(Spec A, Ω_{Spec A/R}), hence by the adjunction between M ↦ M~ and global sections to a morphism Ω[A⁄R]~ ⟶ Ω_{Spec A/R}.

The two composites are identities because an R-derivation of 𝒪_{Spec A} is determined by its values on the global sections coming from A (Scheme.Modules.Derivation.Spec_ext): on a basic open D(f) every section is a fraction a / fⁿ, whose derivative is forced by the Leibniz rule.

Main declarations #

TauCeti.AlgebraicGeometry.relativeDifferentialsSpecIso R A: the isomorphism Ω_{Spec A/R} ≅ Ω[A⁄R]~, characterized by relativeDifferentialsSpecIso_hom_app_d and relativeDifferentialsSpecIso_inv_app_toOpen;
TauCeti.AlgebraicGeometry.isQuasicoherent_relativeDifferentials_Spec: Ω_{Spec A/R} is quasi-coherent;
TauCeti.AlgebraicGeometry.Scheme.Modules.Derivation.Spec_ext: an R-derivation of 𝒪_{Spec A} is determined by its values on the global sections coming from A.

References #

R. Hartshorne, Algebraic Geometry, Section II.8.
The Stacks Project, Morphisms of Schemes, Section Sheaf of differential forms.

source

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

d₁ = d₂

An R-derivation of 𝒪_{Spec A} is determined by its values on the global sections coming from A.

The derivation of `𝒪_{Spec A}` into `Ω[A⁄R]~` #

The comparison isomorphism #

source

noncomputable def TauCeti.AlgebraicGeometry.relativeDifferentialsSpecIso (R : Type u) [CommRing R] (A : CommRingCat) [Algebra R ↑A] :

AlgebraicGeometry.Scheme.relativeDifferentials R (AlgebraicGeometry.Spec A) ≅ AlgebraicGeometry.tilde ↧Ω[↑A⁄R]

The sheaf of relative differentials of an affine scheme: for an R-algebra A, Ω_{Spec A/R} is the quasi-coherent sheaf Ω[A⁄R]~ associated with the Kähler differentials, with d a ↦ D a for a ∈ A.

Equations