LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

Extending an étale morphism to a smooth ambient neighbourhood

Statement

Assume the Axiom of Choice. Let $K$ be a field of characteristic zero and let $ι_{U} ⁣ : U ↪ A_{K}^{m}$ and $ι_{V} ⁣ : V ↪ A_{K}^{n}$ be closed immersions of affine $K$ -varieties of finite type (Closed immersions of schemes, Integral schemes). Let $φ ⁣ : U \to V$ be étale at a $K$ -rational point $u_{0}$ , and put $v_{0} = φ (u_{0})$ . Choose affine coordinates on the two ambient spaces carrying $u_{0}$ and $v_{0}$ to their origins.

Then there is a closed subscheme $X \subseteq A_{K}^{n} \times_{K} A_{K}^{m}$ containing the graph copy of $U$ , smooth at $(v_{0}, u_{0})$ , such that the projection $Φ : = {pr}_{1} ∣_{X} ⁣ : X \to A_{K}^{n}$ is étale at $(v_{0}, u_{0})$ and restricts on $U$ to $ι_{V} \circ φ$ . Thus $φ$ extends to a morphism of smooth ambient varieties étale at the chosen point.

After extending the ground field so the point is rational, the usual local factorization of a smooth morphism as an étale morphism followed by a projection gives the corresponding smooth ambient extension locally. This is the reduction used in the source's proof of functoriality for smooth morphisms.

Facts & Assumptions

Given: The Axiom of Choice; a characteristic-zero field $K$ ; closed immersions $U ↪ A_{K}^{m}$ and $V ↪ A_{K}^{n}$ of affine varieties of finite type; and a morphism $φ ⁣ : U \to V$ étale at the $K$ -rational point $u_{0}$ , with image $v_{0}$ .

[F1]

Étale maps induce completion isomorphisms at equal-residue points: since $u_{0}$ and $v_{0}$ are $K$ -rational, their residue fields are both $K$ , and the étale local map induces an isomorphism of completed local rings.

[F2]

Closed immersions of schemes: the graph map $U \to A_{K}^{n} \times_{K} A_{K}^{m}$ , $u \mapsto (ι_{V} (φ (u)), ι_{U} (u))$ , is a closed immersion; its ideal is finitely generated and contains the equations of the target $V$ .

[F3]

Standard smooth presentations and locally standard smooth maps, Locally standard smooth iff flat with geometrically regular fibres, Étale morphism of schemes: if $m$ equations in the $y$ -coordinates have invertible $m \times m$ Jacobian at the point, their zero scheme is standard smooth of relative dimension $0$ over $A_{K}^{n}$ , hence its projection to $A_{K}^{n}$ is étale there.

[F4]

Flat maps with geometrically regular fibres have standard smooth local presentations, Relative dimension of a smooth morphism at a point: a smooth germ of relative dimension $r$ has a standard smooth local presentation with $r$ free parameters; separating these parameters from the equations factors it locally as an étale germ to the product with $A^{r}$ followed by projection.

[F5]

Jacobson-adic completion is faithfully flat: the maximal-ideal completion of a Noetherian local ring is faithfully flat, so equality of finite defining ideals can be checked after completion.

Proof

1.1F1F2

Embed the source by its graph. Use coordinates $x_{1}, \dots, x_{n}$ on $A_{K}^{n}$ and $y_{1}, \dots, y_{m}$ on $A_{K}^{m}$ , centered at $v_{0}$ and $u_{0}$ . Write the equations of $V$ as $f_{1} (x), \dots, f_{l} (x)$ and choose further equations $h_{1} (x, y), \dots, h_{s} (x, y)$ for the graph copy of $U$ . Put $S = {\hat{O}}_{V, v_{0}}$ . By [F1] the induced map $S \to {\hat{O}}_{U, u_{0}}$ is an isomorphism. In the completed local ring of $V \times_{K} A_{K}^{m}$ , identified with $S ⟦ y_{1}, \dots, y_{m} ⟧$ , the graph map therefore sends each $y_{j}$ to some $g_{j} \in S$ with zero residue, and its ideal is generated by $y_{1} - g_{1}, \dots, y_{m} - g_{m}$ . The images of the $h_{j}$ generate this graph ideal, so their classes span its conormal space modulo the maximal-ideal multiple. The classes of $y_{j} - g_{j}$ are a basis of that $m$ -dimensional $K$ -vector space. Hence some $m$ of the $h_{j}$ have coefficient matrix on these generators invertible at the point; since each $g_{j}$ has zero residue, this matrix is their $y$ -Jacobian there.

2.1F2step 1.1

Choose equations for the ambient extension. Select $m$ of the equations $h_{j}$ , say $h_{i_{1}}, \dots, h_{i_{m}}$ , whose $y$ -linear parts form a basis of that vector space, and define $X : = V (h_{i_{1}}, \dots, h_{i_{m}}) \subseteq A_{K}^{n} \times_{K} A_{K}^{m} .$ Every point of the graph copy of $U$ satisfies these equations, so $U$ is a closed subscheme of $X$ . The determinant of the matrix $(\partial h_{i_{a}} / \partial y_{b})_{a, b = 1}^{m}$ is nonzero at $(v_{0}, u_{0})$ .

3.1F3F5step 2.1

The projection is étale. The presentation of $X$ from step 2.1 has $m$ variables $y_{1}, \dots, y_{m}$ and $m$ equations with invertible Jacobian minor, so it is standard smooth of relative dimension $0$ over $A_{K}^{n}$ at $(v_{0}, u_{0})$ . By [F3], $Φ ⁣ : X \to A_{K}^{n}$ is étale there. Consequently $X$ is smooth at $(v_{0}, u_{0})$ , and the projection restricts on $U$ to $ι_{V} \circ φ$ by construction. Moreover the germ of $U$ equals that of $X \times_{A_{K}^{n}} V$ : in $S ⟦ y_{1}, \dots, y_{m} ⟧$ the selected equations generate the graph ideal, because their coefficient matrix on $y_{j} - g_{j}$ is invertible in the complete local ring. Thus the two defining ideals agree after completion, and [F5] makes them agree in the local ring itself. Their quotient is a finite module, so it vanishes on a neighbourhood of the point. Shrinking $X$ there therefore makes this square Cartesian.

4.1F4step 3.1∎

Smooth morphisms. Let $W \to S$ be smooth at a geometric point. By [F4], after a local standard smooth chart it factors as an étale germ $W \to S \times A^{r}$ followed by projection. After extending the ground field so the point is rational, embed the two affine germs in affine spaces and apply steps 1.1–3.1 to the étale germ; composing the resulting ambient étale map with the projection gives a smooth ambient extension of the original germ.

Remarks

The source proof uses coordinates on $A^{n} \times A^{m}$ , hence the ambient dimension is $n + m$ . Its printed line saying $X \subset A^{m}$ is inconsistent with those coordinates and with its projection $A^{m + n} \to A^{n}$ ; the statement above follows the coordinate proof.
The ambient extension is proved for the source's affine-embedding and rational-point setting. The smooth-morphism consequence is used after passage to a geometric point; no claim is made here that an arbitrary non-rational point over the original field is rational.

Depends on

Used by

Resolution of singularities in characteristic zero Theorem

Dependency tree · two levels

68 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

Jaroslaw Wlodarczyk, Simple Hironaka resolution in characteristic zero, J. Amer. Math. Soc. 18 (2005) 779-822; author's arXiv version math/0401401 (28 pp., dated October 25, 2018) (standard reference, not scraped)