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.
Tangent vectors at rational points are dual-number points
Statement
Let be any -scheme and let be a -rational point. The intrinsic Zariski tangent space is naturally isomorphic, as a -vector space, to the fibre over of where the map is induced by . Equivalently, where acts on through evaluation at . The bijection is induced by writing a local -algebra map as . No identification at a nonrational point is asserted.
Facts & Assumptions
Given: A field , a -scheme , and a -rational point . Put and let send to zero.
The intrinsic Zariski tangent space: is the -linear dual of when .
The affine scheme of dual numbers: is the dual-numbers scheme, with .
Affine schemes are contravariantly equivalent to commutative rings: for commutative rings , ring maps correspond contravariantly to morphisms .
Cotangent spaces commute with localization at a rational point: if , localization induces an isomorphism .
Schemes: every point of a scheme has an affine open neighborhood.
Affine open subschemes: an open subscheme has the restricted structure sheaf; an affine open is affine with this structure.
Open immersions of schemes: the inclusion of an open subscheme is an open immersion.
The underlying space of an affine spectrum: the points of are the prime ideals of .
Schemes and morphisms over a base: a -morphism commutes with the structure maps to .
Prime ideals and maximal ideals in a commutative ring: a proper ideal is prime when implies or ; a maximal ideal has no proper ideal strictly between it and the ring.
The quotient ring with : is formed from cosets with .
is a field if and only if is a maximal ideal: for a commutative ring , is a field exactly when is maximal.
Proof
The dual-numbers scheme has one point. If is a prime ideal of , then implies by [F11]. The quotient is , so is maximal by [F12, F13]. Every prime containing this maximal ideal equals it. Thus has the single point defined by , and the map induced by selects that point.
Based morphisms can be computed in an affine neighborhood. Choose an affine open containing by [F5, F6]. Its inclusion into is an open immersion by [F7]. Since has only one point, every morphism in the fibre over factors uniquely through . The affine anti-equivalence [F3], together with the -morphism condition [F10], identifies such maps with -algebra homomorphisms whose reduction is the point . Conversely every such homomorphism gives a based morphism. If , then is the point of by [F8].
These homomorphisms are exactly derivations. Each has a unique image , where . Since is a -algebra homomorphism, is -linear and vanishes on . Comparing the -coefficients of gives , so is a derivation for the -module structure on given by evaluation at . Conversely each such derivation defines a homomorphism by this formula, since . These constructions are inverse.
Derivations on are the dual of its cotangent space at . The structure map splits evaluation , so as -vector spaces. The derivation identity makes vanish on , and restriction gives a linear form on . Conversely, for , define for , . For , the product has -part , and ; hence this formula satisfies the Leibniz rule. It is inverse to restriction.
Passing to the stalk gives the claimed intrinsic tangent and local derivation formulation. By [F9], with maximal ideal . The rational-point localization isomorphism [F4] identifies with , so their -linear duals agree; [F1] identifies the latter dual with . Also every has with , which is a unit in with inverse . Thus extends uniquely to a local -algebra map . Conversely, every local -algebra map has a unique form , where multiplicativity makes a -derivation through the residue action. Every such derivation defines a local map by this formula, since units have nonzero residue. Applying the decomposition as in step 4.1 gives . The localization, extension, and restriction maps commute on smaller affine neighborhoods, so the identifications are independent of and natural. Scaling by scales the derivation and tangent vector by .
Depends on
The intrinsic Zariski tangent space
The affine scheme of dual numbers
Affine schemes are contravariantly equivalent to commutative rings
Cotangent spaces commute with localization at a rational point
Schemes
Schemes and morphisms over a base
Affine open subschemes
Open immersions of schemes
The underlying space of an affine spectrum
The stalk of the affine structure sheaf at a prime is A_p
Prime ideals and maximal ideals in a commutative ring
The quotient ring with
is a field if and only if is a maximal ideal