LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Lower semicontinuity of flat finitely presented fibre dimension

Statement

Assume the Axiom of Choice. Let $f : X \to S$ be flat and of finite presentation. For $s \in S$ , let $X_{s}$ be the scheme-theoretic fibre (Scheme-theoretic fibre), with $\dim \emptyset = - \infty$ . Then, for every integer $n \geq 0$ , the set $D_{n} = {s \in S : \dim X_{s} \geq n}$ is open in $S$ . Thus the fibre-dimension function is lower semicontinuous.

Facts & Assumptions

Given: The morphism and conventions in the Statement.

[F1]

Assuming AC, for a flat locally finitely presented morphism there is an open subset $W \subseteq X$ , dense in every nonempty fibre, partitioned into pairwise disjoint open subsets $W_{d}$ for $d \geq 0$ , such that every point of $W_{d}$ has local fibre dimension $d$ and $\sup {d : W_{d} \cap X_{s} \neq \emptyset} = \dim X_{s}$ for every nonempty fibre. The openness and dimension-supremum properties are proved in Dense relative-dimension strata in flat finitely presented fibres.

[F2]

A flat morphism locally of finite presentation is universally open, in particular open (Flat finite-presentation morphisms are open).

[F3]

The fibre $X_{s}$ is $X \times_{S} Spec κ (s)$ ; an empty fibre has dimension $- \infty$ (Scheme-theoretic fibre).

[F4]

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

Proof

technique · direct

1.1F1F3

Apply [F1] to $f$ ; finite presentation implies local finite presentation. If $X_{s} \neq \emptyset$ , the supremum formula of [F1] gives $\dim X_{s} \geq n ⟺ W_{d} \cap X_{s} \neq \emptyset for some integer d \geq n .$ Indeed, the dimensions appearing on the right are nonnegative integers, so a supremum at least the integer $n$ is attained at or above $n$ even if the supremum is infinite. For an empty fibre both sides are false by [F3].

2.1F1F2step 1.1

A fibre meets $W_{d}$ exactly when its base point lies in $f (W_{d})$ . Consequently step 1.1 gives the exact set equality $D_{n} = ⋃_{d \geq n} f (W_{d}) .$ Every $W_{d}$ is open in $X$ by [F1], and $f$ is open by [F2], so every $f (W_{d})$ is open in $S$ . Their union $D_{n}$ is open. This proves the claim unconditionally under the hypotheses of the Statement.

3.1F1F2F3F4step 1.1step 2.1∎

When $X = \emptyset$ the union in step 2.1 is empty for every $n$ . When a fibre has dimension zero it occurs only in $D_{0}$ ; a positive or unbounded fibre dimension is handled by the integer-supremum argument of step 1.1. AC is assumed through [F1] and [F2], with no further choice in the set identity. The proof uses the forward direction of the equivalence in step 1.1 to include points in $D_{n}$ and the reverse direction to exclude all other points.

Depends on

Used by

Fibre dimension of proper flat finitely presented families Theorem

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, More on Morphisms, Section 37.30, Lemma 37.30.5 (standard reference, not scraped)