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.
Universal property of relative differential sheaves
Statement
Let be a morphism of schemes and let with universal derivation (Sheaf of relative Kähler differentials). For every -module , composition with is a bijection natural in . No quasi-coherence or finiteness is assumed on , and no condition is imposed on ; the sheaf is determined up to unique compatible isomorphism by this property.
Facts & Assumptions
Given: A morphism of schemes , the presheaf of Sheaf of relative Kähler differentials, and an -module .
Sheaf of relative Kähler differentials: , the universal derivations assemble to , and an -derivation is a morphism of sheaves of abelian groups that is additive, satisfies the Leibniz rule on sections over every open , and kills the image of .
Sheafification is left adjoint to the inclusion of sheaves into presheaves: every morphism of presheaves with a sheaf factors uniquely through the canonical map .
Derivations are maps out of Ω: for a ring map and every -module , composition with the universal derivation is an isomorphism .
Modules on a ringed space: an -module has section groups that are modules over the section rings, restriction is linear after restricting scalars, and morphisms are linear on every open set.
Derivation of an algebra: an -derivation is additive, kills the image of and satisfies the Leibniz rule; sums and scalar multiples of derivations are derivations.
Proof
Sheafification adjunction. Restriction along gives a bijection : [F2] gives the factorization on underlying presheaves, and the factor is -linear because sections of are locally represented by sections of , with scalar multiplication defined on those representatives by [F1]. Linearity therefore holds locally and hence globally. A morphism of presheaves is exactly a compatible family of -linear maps .
Algebraic universal property on each open. Since is an -algebra, [F3] turns into the derivation , an -derivation by [F5]; conversely every such derivation arises from exactly one . Compatibility of the family under restriction is equivalent to compatibility of the family , because the restriction maps of are defined so that for .
Compatible families of derivations are -derivations. The families in step 1.2 are in canonical bijection with morphisms of sheaves of abelian groups that are additive and satisfy Leibniz on every open and kill the image of each ; by gluing, the last condition is exactly , so these are precisely the -derivations of [F1]. The two passes are inverse because a derivation determines its components , and is recovered from by the universal property of .
Conclusion. Composing the bijections of steps 1.1, 1.2 and 2.1 gives the displayed bijection , since corresponds to the composite of its components with and is assembled from the by [F1]. Each step is natural in : a morphism of -modules composes with and with , so the bijection is compatible with postcomposition, and by the Yoneda lemma is determined up to unique compatible isomorphism.
Depends on
Used by
- A closed point immersion is unramified Example
- Affine charts recover the algebraic module of differentials Lemma
- Differential of an S-morphism Lemma
- Relative differentials commute with scheme base change Lemma
- Conormal sequence for a closed immersion Theorem
- Formal unramifiedness iff Omega vanishes Theorem
- Tangent vectors as dual-number points Theorem
- Transitivity sequence for schemes Theorem
Dependency tree · two levels
18 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, Lemma 17.28.4 and Definition 17.28.10, tags 08TD and 08RT (standard reference, not scraped)
- Stacks Morphisms, Lemma 29.33.2, tag 01UR (standard reference, not scraped)
- Vakil §22.2.20, pp.584–585 (standard reference, not scraped)