Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30
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.

Differentials, open restriction, and the chain rule

Statement

Let k be a field, let X,Y be k-schemes, and let f:X→Y be a k-morphism. For points x∈X and y=f(x)∈Y whose structure maps k→κ(x) and k→κ(y) are isomorphisms (that is, the points are k-rational), write CxX=mx/mx2 and CyY=my/my2. The local map fx♯:OY,y⟶OX,x induces a k-linear map fˉx♯:CyY→CxX. Its dual is the differential dxf=(fˉx♯)∗:TxX⟶TyY. It agrees with post-composition by f on based dual-number points. For the identity, dx(id⁡X)=id⁡TxX; for composable k-morphisms X→fY→gZ and rational points x∈X(k), y=f(x), one has dx(g∘f)=dyg∘dxf. Every k-open immersion induces an isomorphism on tangent spaces at each rational point.

No finite-type, reducedness, or smoothness hypothesis is needed. No Axiom of Choice is assumed or used.

Facts & Assumptions

Given: A field k, k-schemes, a k-morphism, and points x,y=f(x) whose residue fields are identified with k by their structure maps. For the last assertion, the morphism is an open immersion over k and the source point has residue field k.

[F1]

Morphisms of schemes: a scheme morphism is a morphism of locally ringed spaces, and its induced maps on stalks are local homomorphisms.

[F2]

Morphisms of locally ringed spaces: a local stalk homomorphism sends the maximal ideal at the image point into the maximal ideal at the source.

[F3]

Schemes and morphisms over a base: a k-morphism commutes with the structure maps to Spec⁡k.

[F4]

The intrinsic cotangent space: CxX=mx/mx2 is a vector space over the residue field. At a k-rational point this residue field is identified with k by the structure map.

[F5]

The intrinsic Zariski tangent space: TxX is the linear dual of CxX over the residue field; at a rational point it is Hom⁡k(CxX,k).

[F6]

Tangent vectors at rational points are dual-number points: at a rational point of a k-scheme, tangent vectors are naturally the fibre of based morphisms from Spec⁡(k[ϵ]/(ϵ2)).

[F7]

Open immersions of schemes: an open immersion identifies its source isomorphically with an open subscheme of its target.

[F8]

Affine open subschemes: an open subscheme U⊆X has structure sheaf OX∣U.

Proof

technique · direct
1.1F1F2F3F4F5givenalgebra

Put B=OY,y, A=OX,x, n=my, and m=mx. By [F1], fx♯:B→A is local; [F2] means that fx♯(n)⊆m and fx♯(n2)⊆m2. It therefore induces a map n/n2→m/m2. Since f is a k-morphism, [F3] says that its stalk map commutes with the two structure maps from k; because x and y are rational, these maps identify both residue fields with k. The quotient map is thus k-linear by [F4]. Dualizing it over k gives the stated map dxf:TxX→TyY by [F5].

1.2F1F2F4F5F7F8givenalgebra

Let j:U→X be a k-open immersion and let u∈U(k) map to x∈X(k). By [F7], j identifies U with an open subscheme of X; by [F8] that open subscheme carries the restricted structure sheaf. Hence the induced stalk map ju♯:OX,x→OU,u is an isomorphism. It identifies maximal ideals and their squares, so the induced cotangent map CxX→CuU is an isomorphism. Its dual duj is therefore an isomorphism TuU→TxX.

2.1F1F3F4F5step 1.1givenalgebra

For the identity morphism, the local-ring and cotangent maps are identities, so their dual is the identity. If g:Y→Z is another k-morphism and z=g(y), contravariance on stalks gives (g∘f)x♯=fx♯∘gy♯. Passing to maximal ideals modulo squares gives (g∘f)‾x♯=fˉx♯∘gˉy♯. Dualizing reverses this order, so dx(g∘f)=(gˉy♯)∗∘(fˉx♯)∗=dyg∘dxf. This proves identity and chain rules without choosing coordinates or bases.

3.1F4F5F6step 1.1step 2.1givenalgebra

Under [F6], a tangent vector t∈TxX is represented by a based map γt:Spec⁡(k[ϵ]/(ϵ2))→X. For b∈n, the coefficient of ϵ in the pullback of b by f∘γt is the value of t on fx♯(b) mod m2, namely t(fˉx♯(b mod n2)). This is exactly the functional dxf(t) on CyY. Constants have zero ϵ-coefficient, so the agreement holds on the whole local ring. Thus the dualized construction is the map on based dual-number points induced by post-composition with f; the identity and composition laws also agree with composition of these maps.

4.1F4F5F6step 1.1step 2.1step 3.1givenalgebra∎

If a source or target cotangent space is zero, the induced cotangent map still has the displayed source and target, and its dual is the unique corresponding linear map; in particular zero tangent vectors map to zero. If both cotangent spaces are one-dimensional and the cotangent map sends a chosen target generator to c times a chosen source generator, its dual sends a source functional with value a on the source generator to the target functional with value ca on the target generator. This is precisely the same formula as step 1.1 and introduces no exceptional one-dimensional case. The construction is defined for every local map, including zero, noninjective, or nonsurjective cotangent maps. If X is empty there is no source rational point and the pointwise assertions are vacuous. The zero tangent vector is the based map factoring through Spec⁡k and is preserved by post-composition. All maps used are canonical, so no choice of bases or other choices, and no Axiom of Choice, is used. The statement contains no iff claim.

Depends on

Dependency tree · 2 levels

Sources