ExampleConstruction: 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.

Polynomial rings are flat and smooth

Statement

Let $A$ be a commutative ring and $n \geq 0$ an integer. The polynomial algebra $P = A [T_{1}, \dots, T_{n}]$ is a free $A$ -module with the monomials as a basis, hence flat over $A$ , and the structure morphism $A_{A}^{n} = Spec P ⟶ Spec A$ (Affine n-space over an arbitrary base) is flat, locally of finite presentation and smooth of relative dimension $n$ (Smooth morphism of schemes, Relative dimension of a smooth morphism at a point). Its fibres are affine $n$ -spaces over the residue fields, and for $n = 0$ the morphism is the identity of $Spec A$ , which is étale (Étale morphism of schemes).

Assume the Axiom of Choice for the smoothness conclusion, since the Jacobian criterion used below assumes it; the flatness statement is choice-free.

Facts & Assumptions

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

[F1]

A free module over a commutative ring is flat without a choice assumption (Under the stated choice boundary, free modules are projective and hence flat), and for affine charts $f (U) \subseteq V$ with $U = Spec B$ , $V = Spec A$ flatness of $B$ over $A$ implies flatness at every point of $U$ without choice (the converse assumes AC) (Affine-local flatness); the pointwise definition of flatness is in Flat morphism of schemes.

[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 case $r = 0$ is allowed and is exactly a localisation of a polynomial ring, and the relative dimension is $m - r$ (Standard smooth presentations and locally standard smooth maps). In particular $R [x_{1}, \dots, x_{m}]$ itself is standard smooth over $R$ of relative dimension $m$ , by the empty equation list with $g = 1$ .

[F3]

Assume AC. For $f$ locally of finite presentation at $x$ , $f$ is smooth at $x$ if and only if some affine chart has a presentation with an invertible Jacobian minor; moreover such a chart is flat with geometrically regular fibres and exhibits relative dimension $m - r$ at $x$ (Relative Jacobian criterion with its presentation hypothesis).

[F4]

A morphism is smooth at $x$ when it is locally of finite presentation at $x$ , flat at $x$ and the fibre is geometrically regular at $x$ (Smooth morphism of schemes), and its relative dimension is the common local dimension of the geometric fibres over $x$ (Relative dimension of a smooth morphism at a point).

[F5]

A polynomial algebra over a ring is a finitely presented algebra, so the corresponding affine morphism is locally of finite presentation (Locally finite presentation morphisms).

[F6]

On $S = Spec A$ one has $A_{S}^{n} = Spec A [T_{1}, \dots, T_{n}]$ with its structure morphism, and these definitions agree under localisation of $A$ (Affine n-space over an arbitrary base).

[F7]

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

Proof

technique · direct

1.1F1F6

Flatness. The monomials $T_{1}^{a_{1}} \dots T_{n}^{a_{n}}$ form a basis of $P$ as an $A$ -module, so $P$ is free, hence flat over $A$ by [F1]. The morphism $A_{A}^{n} \to Spec A$ is the affine morphism $Spec P \to Spec A$ by [F6], so it is flat at every point by the affine-local criterion [F1].

1.2F2F5

Finite presentation and the standard smooth chart. The $A$ -algebra $P = A [T_{1}, \dots, T_{n}]$ is a polynomial algebra, hence finitely presented, so the structure morphism is locally of finite presentation by [F5]. The empty equation list exhibits $P$ as $(A [T_{1}, \dots, T_{n}] / (\emptyset))_{1}$ ; by [F2] this is a standard smooth presentation of relative dimension $n - 0 = n$ with the empty Jacobian having invertible $0 \times 0$ minor, in the convention of [F2] in which the case $r = 0$ is the localisation of a polynomial ring.

2.1F2F3F4step 1.2

Smoothness of relative dimension n. The chart of step 1.2 is an affine chart of the morphism with an invertible Jacobian minor and with $r = 0$ , $m = n$ ; since the morphism is locally of finite presentation by step 1.2, the smoothness direction of the Jacobian criterion [F3] applies at every point and exhibits relative dimension $n$ . By [F4] the morphism is smooth with relative dimension $n$ at every point, i.e. pure relative dimension $n$ ; its fibres are $A^{n}$ over the residue fields.

3.1

The case $n = 0$ and accounting. For $n = 0$ the polynomial algebra is $P = A$ , the morphism is the identity of $Spec A$ , and the same argument gives smoothness of relative dimension $0$ , i.e. étaleness, by [F4]. The Axiom of Choice [F7] is assumed in the Statement and is used exactly through the Jacobian criterion [F3] in step 2.1; steps 1.1 and 1.2 are choice-free. [F3, F4, F6, F7, step 1.1] $□$

Depends on

Used by

The affine line is smooth but not etale Counterexample

Dependency tree · two levels

40 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, Sections 29.25 and 29.34-29.35 (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Chapters 25-26 (standard reference, not scraped)