Alphabeta Math
LemmaStatement: 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.

Differential of an S-morphism

Statement

Let S be a scheme and let f ⁣:X→Y be a morphism of S-schemes. Then the universal derivations of X/S and Y/S induce a unique OX-linear map df ⁣:f∗ΩY/S⟶ΩX/S,1⊗dY/S(g)⟼dX/S(g∘f), the differential of f. It satisfies:

  1. (identity) for f=idX the map df is the canonical identification idX∗ΩX/S≅ΩX/S;
  2. (chain rule) for X→fY→gZ over S the composite f∗g∗ΩZ/S→f∗ΩY/S→ΩX/S, formed with the canonical identification f∗g∗≅(g∘f)∗, equals d(g∘f);
  3. (fibres) at each x∈X, with y=f(x), the map df induces a κ(x)-linear map (ΩY/S,y⊗OY,yκ(y))⊗κ(y)κ(x)⟶ΩX/S,x⊗OX,xκ(x). Dualising over κ(x) gives a κ(x)-linear tangent map TX/S,x⟶Hom⁡κ(x)((ΩY/S,y⊗OY,yκ(y))⊗κ(y)κ(x),κ(x)). If κ(y)=κ(x), this target is TY/S,y.

No finiteness, flatness or separatedness hypothesis is imposed.

Facts & Assumptions

Given: A scheme S and a morphism f ⁣:X→Y of S-schemes.

[F1]

Transitivity sequence for schemes: the first arrow γ ⁣:f∗ΩY/S→ΩX/S of the transitivity sequence is the unique OX-linear map with γ(1⊗dY/S(g))=dX/S(g∘f).

[F2]

Relative cotangent and tangent spaces and Pullback of a module along a morphism of ringed spaces: the relative cotangent space at x is ΩX/S,x⊗OX,xκ(x), and the source stalk of df is ΩY/S,y⊗OY,yOX,x; its fibre is the cotangent space at y extended along κ(y)→κ(x).

[F3]

Pullback of a module along a morphism of ringed spaces: the composite of pullbacks is canonically identified with the pullback along the composite, f∗g∗≅(g∘f)∗, by associativity of the sheaf tensor products defining pullback; on generators 1⊗1⊗s the identification is the identity.

[F4]

Universal property of relative differential sheaves: a map out of Ω is determined by its values on the universal differentials, since these generate the module.

[F5]

Sheaf of relative Kähler differentials: the modules ΩX/S and ΩY/S and their universal derivations exist for arbitrary morphisms and kill the images of the structure maps from OS.

Proof

technique · direct
1.1F1F4F5

Construction. By [F1], applied to the S-morphism f, there is a unique OX-linear df ⁣:f∗ΩY/S→ΩX/S with df(1⊗dY/S(g))=dX/S(g∘f) for local sections g of OY; it is obtained by applying the universal property [F4] to the S-derivation OY→f∗ΩX/S, g↦dX/S(g∘f), and then the adjunction of Pullback of modules is left adjoint to pushforward, and it is natural in the data (X,Y,f) by construction.

2.1F4step 1.1

Identity. For f=idX the map sends 1⊗dX/S(g) to dX/S(g); since the elements dX/S(g) generate ΩX/S over OX by [F4], this is the canonical identification idX∗ΩX/S≅ΩX/S.

2.2F3F4step 1.1

Chain rule. Let X→fY→gZ be morphisms of S-schemes. Both d(g∘f) and the composite df∘f∗(dg) are OX-linear maps (g∘f)∗ΩZ/S→ΩX/S (the composite being formed with the identification [F3]), and on a generator 1⊗1⊗dZ/S(h) both take the value dX/S(h∘g∘f): the composite because df(1⊗dY/S(h∘g))=dX/S(h∘g∘f) and dg(1⊗dZ/S(h))=dY/S(h∘g), and d(g∘f) by its definition. As the generators 1⊗1⊗dZ/S(h) generate the source over OX, the two maps agree.

2.3F2step 1.1

Fibres and the tangent map. Fix x∈X and put y=f(x). By [F2], the source stalk of df is ΩY/S,y⊗OY,yOX,x. Tensoring it with κ(x) gives ΩY/S,y⊗OY,yκ(x), canonically (ΩY/S,y⊗OY,yκ(y))⊗κ(y)κ(x), because OY,y→κ(x) factors through the residue field κ(y). Thus the fibre of df is the κ(x)-linear cotangent map displayed in the statement. Dualising over κ(x) gives the stated map from TX/S,x to the κ(x)-dual of the extended cotangent space at y. When the residue-field map is an isomorphism, this target is TY/S,y; without that hypothesis, the latter is only a κ(y)-vector space and cannot be the target of a κ(x)-linear map.

3.1step 1.1step 2.1step 2.2step 2.3∎

Conclusion. Step 1.1 gives the asserted map and its characterisation, steps 2.1 and 2.2 give the identity and chain rules, and step 2.3 gives the fibre and tangent maps; nothing beyond the universal property of Ω and the functoriality of pullback and of extension of scalars was used, so no finiteness, flatness or separatedness hypothesis enters.

Depends on

Used by

Dependency tree · two levels

34 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