How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Sheaf of relative Kähler differentials
Definition
Let be a morphism of schemes (Morphisms of schemes), so that is in particular a morphism of ringed spaces and comes with a map of sheaves of rings (Inverse image presheaf and inverse image sheaf); the pair is an -scheme (Schemes and morphisms over a base). Let be a sheaf of -modules (Modules on a ringed space).
-derivations. An -derivation of into is a morphism of sheaves of abelian groups such that for all local sections of over a common open set one has
and such that annihilates the image of : the composite is the zero map. Here the products and sums are taken in the rings . The set of all such is written ; it is a -module under the pointwise operations, and for a morphism of -modules, postcomposition maps to . For -schemes and -morphisms the condition is that kills ; when is fixed one simply says derivation.
Construction of . Consider the presheaf of -modules
where is open, the ring maps to by , and is the Kähler differential module of that ring map (Universal Kähler differential module), which exists by Existence and generators of Kähler differentials. For the restriction is the unique -linear map induced, via the universal property of , by the derivation , where is viewed as an -module by restriction of scalars; the restriction maps compose, so is a presheaf of -modules. Define
the sheafification of (Sheafification of a presheaf); this is a sheaf of -modules by defining scalar multiplication on local representatives in the double-plus construction, with equality on germs making the operation well defined. The universal derivations are compatible with the restriction maps by construction, so they define a morphism of presheaves and hence a morphism of sheaves
the universal -derivation of over , and is an -derivation because each is an -derivation for and the maps are the structure maps .
Local descriptions. Two descriptions are used constantly and are recorded here for orientation; both are proved from the universal property in Universal property of relative differential sheaves and Affine charts recover the algebraic module of differentials.
- Functor of points form. For every -module there is a natural bijection , ; this is the universal property that characterizes .
- Affine charts. If is an affine open subscheme and for an affine open , then the map , exhibits as , compatibly with the universal derivations, and restriction to a basic open corresponds to the localization .
Affine module convention. The affine description (2) identifies on each affine chart with the sheaf attached to , with localization as restriction. This local description is the part used below; it needs no finiteness, flatness or separatedness hypothesis on and also applies to the identity .
Depends on
Used by
- A torsion-only extension of the canonical formula fails for Frobenius Counterexample
- The affine line is smooth but not etale Counterexample
- Canonical bundle and canonical divisors Definition
- Derivative ideals of an ideal sheaf and of a marked ideal Definition
- Dualizing line bundle and trace datum of a smooth projective variety Definition
- Ramification points, branch points and unramifiedness Definition
- Relative cotangent and tangent spaces Definition
- Relative differential-rank condition Definition
- The Chern character and the Todd class Definition
- The different divisor of a generically separable morphism of curves Definition
- Unramified morphism Definition
- Ramification indices of the power map on the projective line Example
- A uniformizer differential generates the module of differentials Lemma
- Adjunction for a smooth closed subvariety Lemma
- Affine charts recover the algebraic module of differentials Lemma
- Canonical weight of a flag variety Lemma
- Degree-p differential trace extends across normal surface valuations Lemma
- Differential of an S-morphism Lemma
- Divisors of rational differentials form one linear equivalence class Lemma
- Etale pullback commutes with derivative ideals Lemma
- Ext of a locally free cotangent sheaf via sheaf cohomology Lemma
- Local support and index bound for the different of a curve map Lemma
- Relative canonical weight for a minimal-parabolic flag projection Lemma
- Relative differentials commute with scheme base change Lemma
- The invariant differentials of a group scheme Lemma
- Top differential lattices map into point-blowup canonical modules Lemma
- Truncation, differentials and the cotangent complex of a smooth morphism Lemma
- Unramified residue extensions are finite separable Lemma
- Canonical bundle formula with the different Theorem
- Differentials of a smooth morphism Theorem
- Étale equals flat and unramified in finite presentation Theorem
- Etale morphisms are the formally etale morphisms locally of finite presentation Theorem
- Formal unramifiedness iff Omega vanishes Theorem
- Smoothness over a characteristic-zero field via free differentials Theorem
- Transitivity sequence for schemes Theorem
- Universal property of relative differential sheaves Theorem
Dependency tree · two levels
20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Stacks Modules 17.28.4 and 17.28.10, tags 08TD and 08RT (standard reference, not scraped)
- Stacks Morphisms 29.33.1 and 29.33.5, tags 01UQ and 01UT (standard reference, not scraped)
- Vakil §22.2.20, pp.584–585 (standard reference, not scraped)