CounterexampleConstruction: Literature-sourcedVerification: 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.

The affine line is smooth but not etale

Statement

Let $k$ be a field and let $f ⁣ : A_{k}^{1} = Spec k [T] ⟶ Spec k$ be the structure morphism (Affine n-space over an arbitrary base).

$f$ is flat and locally of finite presentation, and it is smooth of relative dimension $1$ (Smooth morphism of schemes, Relative dimension of a smooth morphism at a point); this is the case $n = 1$ of Polynomial rings are flat and smooth.
$f$ is 'etale at no point of $A_{k}^{1}$ (Étale morphism of schemes): its relative dimension is $1$ , not $0$ , and its sheaf of relative differentials $Ω_{A_{k}^{1} / k}$ is locally free of rank $1$ .
Consequently the implication "smooth $\Rightarrow$ 'etale" is false, and the relative dimension zero clause in the definition of 'etaleness cannot be dropped. The failure is detected both by the relative dimension and by unramifiedness: $Ω_{A_{k}^{1} / k} \neq 0$ at every point.

Assume the Axiom of Choice (The Axiom of Choice) for the smoothness statement and for the rank computation of the differentials.

Facts & Assumptions

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

[F1]

For every ring $A$ and $n \geq 0$ the polynomial algebra $A [T_{1}, \dots, T_{n}]$ is a free $A$ -module, hence flat, and the structure morphism $A_{A}^{n} = Spec A [T_{1}, \dots, T_{n}] \to Spec A$ is flat, locally of finite presentation and smooth of relative dimension $n$ ; for $n = 0$ it is the identity and 'etale (Polynomial rings are flat and smooth, Affine n-space over an arbitrary base).

[F2]

'Etale at $x$ means smooth at $x$ together with relative dimension $0$ at $x$ ; for a smooth germ the relative dimension is the well-defined local dimension of the geometric fibres over $x$ , and it equals the number of free parameters of a standard smooth chart (Étale morphism of schemes, Relative dimension of a smooth morphism at a point, Smooth morphism of schemes).

[F3]

Assume AC. If $f$ is smooth at $x$ , then $Ω_{X / S}$ is locally free of finite rank near $x$ and its rank at $x$ equals the relative dimension of $f$ at $x$ (Differentials of a smooth morphism, Sheaf of relative Kähler differentials).

[F4]

Assume AC. For a locally finitely presented morphism, 'etale at $x$ is equivalent to flatness at $x$ together with unramifiedness at $x$ ; unramifiedness at $x$ is equivalent to the vanishing of $Ω_{X / S, x}$ (Étale equals flat and unramified in finite presentation, Unramified morphism, Formal unramifiedness iff Omega vanishes).

[F5]

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

Proof

technique · direct

1.1F1

Smoothness of relative dimension one. Take $A = k$ and $n = 1$ in [F1]: the algebra $k [T]$ is a free $k$ -module (the monomials form a basis) and the structure morphism $f$ is flat, locally of finite presentation and smooth of relative dimension $1$ at every point. This is claim 1.

2.1F2step 1.1

'Etaleness fails by relative dimension. By [F2] 'etaleness of $f$ at a point $x$ requires relative dimension $0$ at $x$ ; but by step 1.1 the smooth germ $f$ has relative dimension $1$ at $x$ , and by [F2] this integer is well-defined, so $1 \neq 0$ and $f$ is not 'etale at $x$ . As $x \in A_{k}^{1}$ was arbitrary, $f$ is 'etale at no point.

2.2F3F4step 1.1

The differentials are locally free of rank one. By [F3] (AC) applied to the smooth morphism $f$ , the sheaf $Ω_{A_{k}^{1} / k}$ is locally free of finite rank near every point and its rank at a point $x$ equals the relative dimension, namely $1$ ; in particular $Ω_{A_{k}^{1} / k, x} \neq 0$ for every $x \in A_{k}^{1}$ . By [F4] (AC), applied at $x$ , $f$ is 'etale at $x$ if and only if it is flat at $x$ and unramified at $x$ , and unramifiedness at $x$ would force $Ω_{A_{k}^{1} / k, x} = 0$ ; since $f$ is flat by step 1.1 and the stalk of the differentials does not vanish, $f$ fails to be unramified and hence to be 'etale at $x$ . This corroborates claim 2 and proves claim 3.

3.1

Choice accounting. The Axiom of Choice [F5] is assumed in the Statement and used exactly through the smoothness of the affine space in [F1] in step 1.1 and the rank computation [F3] with the flat-unramified criterion [F4] in step 2.2; the relative-dimension argument of step 2.1 is choice-free. [F1, F3, F4, F5] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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.36 (etale versus smooth of relative dimension zero, tag 02G4) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Chapter 26 (the affine line is smooth but not etale) (standard reference, not scraped)