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

Fibres of a smooth morphism are smooth

Statement

Assume the Axiom of Choice (AC). Let $f : X \to S$ be a morphism, $s \in S$ and let $X_{s}$ be the scheme-theoretic fibre (Scheme-theoretic fibre), with base-changed fibre $X_{s, K} = X_{s} \times_{Spec κ (s)} Spec K$ for a field extension $K / κ (s)$ (a geometric fibre as in Geometric fibres and geometric points when $K$ is an algebraic closure of $κ (s)$ ).

If $f$ is smooth (Smooth morphism of schemes), then the structural morphism $X_{s} \to Spec κ (s)$ is smooth.
If $f$ is smooth, then for every field extension $K / κ (s)$ , the morphism $X_{s, K} \to Spec K$ is smooth.
Pointwise: if $f$ is smooth at $x \in X_{s} \subseteq X$ , then $X_{s} \to Spec κ (s)$ is smooth at $x$ .

Empty fibres are smooth vacuously.

Facts & Assumptions

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

[F1]

$X_{s} = X \times_{S} Spec κ (s)$ with the second projection as structure morphism, and $X_{s, K} = X_{s} \times_{Spec κ (s)} Spec K$ with its projection to $Spec K$ (Scheme-theoretic fibre, Geometric fibres and geometric points).

[F2]

The fibre $X_{s} \to Spec κ (s)$ is the base change of $f : X \to S$ along the canonical morphism $Spec κ (s) \to S$ , and $X_{s, K} \to Spec K$ is the base change of $X_{s} \to Spec κ (s)$ along $Spec K \to Spec κ (s)$ (Base change of objects, morphisms and properties, Geometric fibres and geometric points).

[F3]

Assume AC. For any morphisms $f : X \to S$ , $h : S^{'} \to S$ , the base change $f_{S^{'}} : X \times_{S} S^{'} \to S^{'}$ of a smooth $f$ is smooth (Smoothness survives base change and composition); moreover smoothness of a morphism is a condition on each point of its source, preserved by restricting the source to an open neighbourhood (Smooth morphism of schemes).

[F4]

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

Proof

technique · direct

1.1F1F2F3

Clause 1. Let $ι : Spec κ (s) \to S$ be the canonical residue-field point. By [F1] and [F2] the structural morphism $X_{s} \to Spec κ (s)$ is exactly the base change of $f$ along $ι$ . If $f$ is smooth, [F3] makes this base change smooth. If $X_{s}$ is empty the assertion is vacuous.

2.1F1F2F3step 1.1

Clause 2. Assume $f$ is smooth and fix a field extension $K / κ (s)$ . By [F1] and [F2] the morphism $X_{s, K} \to Spec K$ is the base change of the smooth morphism $X_{s} \to Spec κ (s)$ of step 1.1 along $Spec K \to Spec κ (s)$ , hence smooth by [F3]. The empty case is again vacuous.

2.2F1F3F4step 1.1

Clause 3 and accounting. Suppose $f$ is smooth at $x \in X_{s}$ and let $x$ also denote its image in the fibre. The pointwise standard-chart base-change argument of the stability theorem [F3] shows that base change of a morphism smooth at a point is smooth at every point lying over it, so $X_{s} \to Spec κ (s)$ is smooth at $x$ . The Axiom of Choice [F4] is assumed in the Statement and used exactly through the base-change stability theorem [F3] in steps 1.1 and 2.1.

$□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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-29.37 (fibres of smooth morphisms) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Chapter 25 (standard reference, not scraped)