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.

Unramified of finite presentation does not imply flat or etale

Statement

Let $k$ be a field, put $A = k [t]$ and let $f ⁣ : Spec k ⟶ Spec A$ be the morphism induced by the quotient $A \to A / (t) = k$ ; it is the closed immersion cutting out the origin, the closed point $(t) \in Spec A$ (Closed immersions of schemes).

$f$ is of finite presentation and unramified (Unramified morphism): the algebra $k = A / (t)$ is a finitely presented $A$ -algebra, and $Ω_{k / A} = 0$ because $Ω_{A / A} = 0$ and the conormal sequence of $A \to A \to k$ is exact.
$f$ is not flat (Flat morphism of schemes): the inclusion of ideals $(t) ↪ A$ is injective, but after tensoring over $A$ with $k$ it becomes the zero map $(t) \otimes_{A} k ≅ k \to A \otimes_{A} k ≅ k$ , which is not injective; hence $k$ is not a flat $A$ -module.
Consequently $f$ is not 'etale, although it is unramified of finite presentation. So the implication "unramified $\Rightarrow$ 'etale" is false, and the flatness clause in the flat-plus-unramified description of 'etaleness cannot be dropped.

Assume the Axiom of Choice for the flat-plus-unramified criterion of statement 3.

Facts & Assumptions

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

[F1]

The K"ahler differentials of $A$ over itself vanish: for $A \to A$ the identity every $A$ -derivation of $A$ into every $A$ -module is zero, since the whole ring is the image of $A$ and derivations annihilate that image; the universal property of $Ω_{A / A}$ makes it represent these derivations, so $Ω_{A / A} = 0$ (Universal Kähler differential module, Derivations are maps out of Ω).

[F2]

For $A \to P$ and an ideal $I \subseteq P$ with $B = P / I$ , the conormal sequence $I / I^{2} \to B \otimes_{P} Ω_{P / A} \to Ω_{B / A} \to 0$ is exact (Conormal exact sequence for an algebra quotient).

[F3]

A morphism is formally unramified if and only if its sheaf of relative differentials vanishes, and it is unramified exactly when it is locally of finite type and formally unramified, equivalently locally of finite type with $Ω_{X / S} = 0$ (Formal unramifiedness iff Omega vanishes, Unramified morphism).

[F4]

A module $M$ over a commutative ring $R$ is flat exactly when tensoring with $M$ preserves exact sequences, in particular when it preserves injectivity of every injection of $R$ -modules; $M \otimes_{R} (R / I) ≅ M / I M$ for an ideal $I$ (Flat and faithfully flat modules and ring homomorphisms, $M \otimes_{R} R / I ≅ M / I M$ naturally). A morphism of schemes is flat at a point when the corresponding stalk is flat over the base stalk, and for the affine morphism $Spec B \to Spec A$ this holds exactly when $B$ is flat over $A$ at every point (Flat morphism of schemes).

[F5]

Assume AC. For a locally finitely presented morphism, 'etale at $x$ is equivalent to flat at $x$ and unramified at $x$ ; in particular an 'etale morphism is flat at every point (Étale equals flat and unramified in finite presentation, Étale morphism of schemes).

[F6]

A quotient of a polynomial algebra by a finitely generated ideal is a finitely presented algebra, hence of finite type; $k [t] / (t)$ is such a quotient (Finitely presented modules and finitely presented algebras, Locally finite type and finite type morphisms).

[F7]

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

Proof

technique · direct

1.1F6

Setup and finite presentation. Let $A = k [t]$ , $P = A$ , $I = (t) \subseteq A$ and $B = A / I = k$ , so that the quotient map $A \to B$ induces the closed immersion $f$ of the Statement. Since $I = (t)$ is generated by one element, $B$ is a finitely presented $A$ -algebra by [F6], and the induced morphism is of finite presentation, in particular locally of finite type.

2.1F1F2F3step 1.1

Unramifiedness. By [F1] one has $Ω_{A / A} = 0$ ; applying the conormal sequence [F2] to $A \to P = A$ and $I = (t)$ gives the exact sequence $(t) / (t)^{2} \to k \otimes_{A} Ω_{A / A} \to Ω_{k / A} \to 0$ in which the middle term vanishes, so $Ω_{k / A} = 0$ as the cokernel of a map from a zero module. By [F3] the vanishing of the differentials makes the algebra map $A \to k$ formally unramified, and with finite type from step 1.1 it is unramified; on the scheme level $f$ is unramified. This gives claim 1.

2.2F4step 1.1

Non-flatness. The ideal $(t) \subseteq A$ is a free $A$ -module of rank one via $a \mapsto a t$ , so $(t) \otimes_{A} k ≅ A \otimes_{A} k ≅ k$ by [F4] applied with $M = A$ and $I = (t)$ , which is nonzero because $k$ is a field. The inclusion $ι ⁣ : (t) ↪ A$ is injective, and $ι \otimes_{A} {i d}_{k}$ sends $t \otimes 1$ to $t \otimes 1 = 1 \otimes t = 1 \otimes 0 = 0$ in $A \otimes_{A} k$ , hence is the zero map $k \to k$ , which is not injective. By [F4] tensoring with the $A$ -module $k$ therefore does not preserve injections, so $k$ is not flat over $A$ , and the affine morphism $f ⁣ : Spec k \to Spec A$ is not flat. This gives claim 2.

3.1F5step 2.1step 2.2

Not 'etale. The morphism $f$ is locally of finite presentation by step 1.1 and unramified by step 2.1, but not flat by step 2.2. By [F5] (AC), 'etaleness at a point would require flatness at that point; hence $f$ is not 'etale at its single point, and in particular not 'etale. So a finite presentation, unramified morphism need not be 'etale, which is claim 3: the flatness clause is indispensable.

4.1

Choice accounting. The Axiom of Choice [F7] is assumed in the Statement and used exactly through the flat-plus-unramified criterion [F5] in step 3.1; the conormal computation, the tensor computation and the unramifiedness argument of steps 1.1, 2.1 and 2.2 are choice-free. [F5, F7, step 3.1] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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 and Lemma 29.36.7 (unramified does not imply flat) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Chapter 26 (closed immersions are unramified but usually not flat) (standard reference, not scraped)