Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-27
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 f ⁣:X→S be a morphism of schemes and let ΩX/S=aP with universal derivation dX/S ⁣:OX→ΩX/S (Sheaf of relative Kähler differentials). For every OX-module F, composition with dX/S is a bijection Hom⁡OX(ΩX/S,F)⟶Der⁡S(OX,F),α⟼α∘dX/S, natural in F. No quasi-coherence or finiteness is assumed on F, and no condition is imposed on f; the sheaf ΩX/S is determined up to unique compatible isomorphism by this property.

Facts & Assumptions

Given: A morphism of schemes f ⁣:X→S, the presheaf P(W)=ΩOX(W)/(f−1OS)(W) of Sheaf of relative Kähler differentials, and an OX-module F.

[F1]

Sheaf of relative Kähler differentials: ΩX/S=aP, the universal derivations dW assemble to dX/S, and an S-derivation OX→F is a morphism of sheaves of abelian groups that is additive, satisfies the Leibniz rule on sections over every open W, and kills the image of f♯ ⁣:f−1OS→OX.

[F2]

Sheafification is left adjoint to the inclusion of sheaves into presheaves: every morphism of presheaves φ ⁣:P→F with F a sheaf factors uniquely through the canonical map P→aP.

[F3]

Derivations are maps out of Ω: for a ring map R→T and every T-module N, composition with the universal derivation is an isomorphism Hom⁡T(ΩT/R,N)≅Der⁡R(T,N).

[F4]

Modules on a ringed space: an OX-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.

[F5]

Derivation of an algebra: an R-derivation T→N is additive, kills the image of R and satisfies the Leibniz rule; sums and scalar multiples of derivations are derivations.

Proof

technique · direct
1.1

Sheafification adjunction. Restriction along P→aP=ΩX/S gives a bijection Hom⁡OX(ΩX/S,F)≅Hom⁡OX-presheaf(P,F): [F2] gives the factorization on underlying presheaves, and the factor is OX-linear because sections of aP are locally represented by sections of P, with scalar multiplication defined on those representatives by [F1]. Linearity therefore holds locally and hence globally. A morphism of presheaves P→F is exactly a compatible family of OX(W)-linear maps φW ⁣:P(W)→F(W).

F1F2F4
1.2

Algebraic universal property on each open. Since OX(W) is an (f−1OS)(W)-algebra, [F3] turns φW into the derivation DW:=φW∘dW ⁣:OX(W)→F(W), an (f−1OS)(W)-derivation by [F5]; conversely every such derivation arises from exactly one φW. Compatibility of the family (φW) under restriction is equivalent to compatibility of the family (DW), because the restriction maps of ΩX/S are defined so that dW′∘ρ=ρ∘dW for W′⊆W.

F1F3F5
2.1

Compatible families of derivations are S-derivations. The families (DW) in step 1.2 are in canonical bijection with morphisms of sheaves of abelian groups D ⁣:OX→F that are additive and satisfy Leibniz on every open and kill the image of each (f−1OS)(W); by gluing, the last condition is exactly D∘f♯=0, so these are precisely the S-derivations of [F1]. The two passes are inverse because a derivation determines its components DW, and φW is recovered from DW by the universal property of P(W).

F1step 1.2
3.1

Conclusion. Composing the bijections of steps 1.1, 1.2 and 2.1 gives the displayed bijection α↦α∘dX/S, since α corresponds to the composite of its components with dW and dX/S is assembled from the dW by [F1]. Each step is natural in F: a morphism F→G of OX-modules composes with φW and with DW, so the bijection is compatible with postcomposition, and by the Yoneda lemma ΩX/S is determined up to unique compatible isomorphism.

F1step 1.1step 1.2step 2.1∎

Depends on

Used by

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