TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Smooth maps have étale local affine-space form

Statement

Assume the Axiom of Choice (AC). Let $f : X \to S$ be smooth at $x \in X$ with relative dimension $n = {reldim}_{f} (x)$ (Relative dimension of a smooth morphism at a point). Then there are affine open subschemes $V = Spec A \subseteq S$ containing $s = f (x)$ and $U_{0} = Spec C \subseteq X$ containing $x$ with $f (U_{0}) \subseteq V$ , an element $h \in C$ and affine open subschemes $U = Spec C_{h} \subseteq U_{0}$ containing $x$ , such that $U \to f (U) \subseteq V$ factors as $U \overset{\overset{ˊ}{e} tale}{\to} A^{n} \times_{S} V ⟶ V,$ where $A_{S}^{n}$ is the relative affine space over the base (Affine n-space over an arbitrary base) and the first arrow is étale at $x$ and is an $S$ -morphism. The target is only shrunk Zariski locally: the factorisation is asserted over the chosen affine $V \subseteq S$ .

Equivalently, a smooth morphism of relative dimension $n$ is locally, on the source, étale over relative affine $n$ -space over the base.

Facts & Assumptions

Given: The data and hypotheses displayed in the Statement, with the conventions fixed there.

[F1]

Assume AC. For $f$ locally of finite presentation at $x$ with $s = f (x)$ , $f$ is smooth at $x$ if and only if there are affine opens $U_{0} = Spec C$ of $x$ and $V = Spec A$ of $s$ with $f (U_{0}) \subseteq V$ and a presentation of $C_{h}$ , for some $h \in C ∖ q$ , as $C_{h} ≅ (A [t_{1}, \dots, t_{m}] / (f_{1}, \dots, f_{r}))_{g}$ in which some $r \times r$ minor of the Jacobian matrix is a unit of $C_{h}$ ; such a chart is flat with geometrically regular fibres and exhibits relative dimension $m - r$ at $x$ (Relative Jacobian criterion with its presentation hypothesis, Relative dimension of a smooth morphism at a point).

[F2]

A standard smooth presentation of an $R$ -algebra $S$ is a presentation $S ≅ (R [x_{1}, \dots, x_{m}] / (f_{1}, \dots, f_{r}))_{g}$ with an invertible $r \times r$ Jacobian minor; the integer $m - r \geq 0$ is its relative dimension, the permutation of variables replaces a given invertible minor by one in the first $r$ columns without changing the relative dimension, and $c = 0$ (a localisation of a polynomial ring) is allowed (Standard smooth presentations and locally standard smooth maps).

[F3]

$f$ is étale at $x$ when it is smooth at $x$ and ${reldim}_{f} (x) = 0$ ; the chart of [F1] is smooth with relative dimension $m - r$ , so a chart with $m = r$ and invertible Jacobian minor is étale at the corresponding point (Étale morphism of schemes, Relative dimension of a smooth morphism at a point).

[F4]

A morphism with affine charts on which the ring map is a finitely presented algebra is locally of finite presentation (Locally finite presentation morphisms), and a standard smooth presentation is a finitely presented algebra (Standard smooth presentations and locally standard smooth maps).

[F5]

On $S = Spec A$ one defines $A_{S}^{n} = Spec A [t_{1}, \dots, t_{n}]$ with its structure morphism, and these definitions agree under localisation of $A$ , so $A^{n} \times_{S} V$ is $Spec A [t_{1}, \dots, t_{n}]$ for the affine open $V = Spec A \subseteq S$ and equals $A_{S}^{n} \times_{S} V$ (Affine n-space over an arbitrary base).

[F6]

An open subset of a scheme is given the open subscheme structure; a principal open $D (h)$ of an affine $Spec C$ is the affine open subscheme $Spec C_{h}$ (Affine open subschemes).

[F7]

The Axiom of Choice states that every family of nonempty sets has a choice function (The Axiom of Choice).

Proof

technique · direct

1.1F1

The smooth chart. By [F1] there are affine opens $U_{0} = Spec C$ containing $x$ and $V = Spec A$ containing $s$ with $f (U_{0}) \subseteq V$ , an element $h \in C$ not in the prime $q$ of $x$ , and a presentation $C_{h} ≅ (A [t_{1}, \dots, t_{m}] / (f_{1}, \dots, f_{r}))_{g}$ whose Jacobian has an invertible $r \times r$ minor; this chart exhibits relative dimension $m - r$ at $x$ . Since $f$ is smooth at $x$ by hypothesis and [F1] is an iff, such a chart exists; set $n : = {reldim}_{f} (x) = m - r$ , a nonnegative integer.

2.1F2step 1.1

Regrouping the variables. By [F2] we may permute $t_{1}, \dots, t_{m}$ so that the invertible minor involves the first $r$ columns, and we write $A^{'} : = A [t_{r + 1}, \dots, t_{m}] = A [y_{1}, \dots, y_{n}]$ with $y_{i} = t_{r + i}$ . Then $A [t_{1}, \dots, t_{m}] = A^{'} [t_{1}, \dots, t_{r}]$ , and the presentation of step 1.1 becomes $C_{h} ≅ (A^{'} [t_{1}, \dots, t_{r}] / (f_{1}, \dots, f_{r}))_{g}$ ; the $r \times r$ matrix $(\partial f_{j} / \partial t_{i})_{i, j \leq r}$ is invertible in $C_{h}$ by construction. This is a standard smooth presentation of $C_{h}$ over $A^{'}$ with $m^{'} = r$ variables and $c = r$ equations, hence of relative dimension $m^{'} - c = 0$ , by [F2].

3.1F1F3F4step 2.1

The étale arrow. The map $Spec C_{h} \to Spec A^{'}$ has an affine chart with a finitely presented algebra $A^{'} \to C_{h}$ (step 2.1), so it is locally of finite presentation by [F4] and the presentation of step 2.1 is a chart with invertible Jacobian minor in the sense of [F1]; by the two-way criterion of [F1] it is smooth at the prime of $x$ , and its relative dimension there is $r - r = 0$ . By [F3] the morphism $Spec C_{h} \to Spec A^{'}$ is étale at $x$ .

4.1F5F6step 1.1step 3.1

The factorisation. By [F5] the affine scheme $Spec A^{'} = Spec A [y_{1}, \dots, y_{n}]$ is $A^{n} \times_{S} V \subseteq A_{S}^{n}$ , the relative affine space over the affine open $V \subseteq S$ . The composite $Spec C_{h} \to Spec A^{'} \to V = Spec A$ is the morphism induced by $A \to A^{'} \to C_{h}$ , which is the restriction of the structure map $A \to C$ of the chart; hence it is the restriction of $f$ to the principal open $U = Spec C_{h} \subseteq U_{0}$ , which contains $x$ by [F6] and lies over $V$ by step 1.1. This gives the asserted factorisation of $f ∣_{U}$ through $A^{n} \times_{S} V \to V \subseteq S$ , with first arrow étale at $x$ by step 3.1.

5.1

Conclusion and accounting. Steps 1.1, 2.1, 3.1 and 4.1 produce, for a smooth $f$ of relative dimension $n$ at $x$ , the affine opens $V \subseteq S$ and $U = Spec C_{h} \subseteq X$ together with the étale $S$ -morphism $U \to A^{n} \times_{S} V$ , whose composite with the projection to $S$ is the restriction of $f$ . The Axiom of Choice [F7] is assumed in the Statement and is used exactly through the Jacobian criterion [F1] in steps 1.1 and 3.1; the regrouped presentation is built from the same data and makes no further choice. [F1, F3, F7, step 4.1] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 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

The Stacks Project, Morphisms of Schemes, Section 29.34 (smooth morphisms are locally affine space over the base, tags 01V4-01V9) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Section 25.3 (standard reference, not scraped)