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

The etale locus is open

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $f ⁣ : X \to S$ be a morphism locally of finite presentation (Locally finite presentation morphisms) and let $Et (f) = {x \in X : f is \overset{ˊ}{e} tale at x}$ be its 'etale locus (The étale locus of a morphism). Then $Et (f)$ is open in $X$ , and the restriction of $f$ to $Et (f)$ is 'etale (Étale morphism of schemes). In particular 'etaleness is an open condition on the source, and if $X = \emptyset$ the locus is empty.

Facts & Assumptions

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

[F1]

Assume AC. If $f$ is locally of finite presentation, then $f$ is smooth at $x$ if and only if there are affine charts $U = Spec C$ of $x$ over $V = Spec A$ of $f (x)$ and a presentation of $C_{h}$ , for some $h \in C ∖ q$ with $q$ the prime of $x$ , as $C_{h} ≅ (A [t_{1}, \dots, t_{m}] / (f_{1}, \dots, f_{r}))_{g}$ in which some $r \times r$ Jacobian minor has image a unit of $C_{h}$ ; such a chart is smooth over $A$ with geometrically regular fibres and exhibits relative dimension $m - r$ at $x$ (Relative Jacobian criterion with its presentation hypothesis, Standard smooth presentations and locally standard smooth maps).

[F2]

'Etale at $x$ means smooth at $x$ together with relative dimension $0$ at $x$ ; for a smooth germ the relative dimension is a well-defined integer, and a morphism is 'etale exactly when it is smooth of relative dimension $0$ at every point (Étale morphism of schemes, Relative dimension of a smooth morphism at a point, Smooth morphism of schemes).

[F3]

The 'etale locus $Et (f)$ is the subset of points at which the conditions of 'etaleness hold; membership depends only on the germ, and the restriction of $f$ to an open subscheme $U$ has locus $Et (f ∣_{U}) = Et (f) \cap U$ (The étale locus of a morphism).

[F4]

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

Proof

technique · direct

1.1F1F2

Chart around an 'etale point. Let $x \in Et (f)$ , so $f$ is 'etale at $x$ and hence smooth at $x$ of relative dimension $0$ by [F2]; put $s = f (x)$ . Since $f$ is locally of finite presentation, the Jacobian criterion [F1] (AC) provides affine charts $U = Spec C$ of $x$ and $V = Spec A$ of $s$ with $f (U) \subseteq V$ , an element $h \in C ∖ q$ with $q$ the prime of $x$ , and a presentation $C_{h} ≅ (A [t_{1}, \dots, t_{m}] / (f_{1}, \dots, f_{r}))_{g}$ whose $r \times r$ Jacobian minor is a unit of $C_{h}$ ; the same criterion says this chart exhibits relative dimension $m - r$ at $x$ .

2.1F2step 1.1

The chart has no free parameters. By [F2] the relative dimension of the smooth germ $f$ at $x$ is the well-defined integer $0$ , and by step 1.1 the chart exhibits the relative dimension $m - r$ at $x$ ; hence $m - r = 0$ , so $m = r$ .

3.1F1F2step 2.1

The chart is 'etale throughout a neighbourhood. Since the minor is a unit of $C_{h}$ and $m = r$ , the presentation of step 1.1 exhibits an invertible $m \times m$ Jacobian minor, so for every point $y \in D (h) \subseteq U$ the same presentation and the same charts $U, V$ satisfy the hypothesis of the Jacobian criterion [F1] at $y$ (the element $h$ does not lie in the prime of $y$ because $y \in D (h)$ ). The criterion therefore makes $f$ smooth at $y$ with relative dimension $m - r = 0$ , so $f$ is 'etale at $y$ by [F2]. Hence $D (h) \subseteq Et (f)$ is an open neighbourhood of $x$ in $X$ .

4.1F2F3step 3.1

Openness and the restricted morphism. Every point $x$ of $Et (f)$ has, by steps 1.1, 2.1 and 3.1, an open neighbourhood $D (h)$ contained in $Et (f)$ ; hence $Et (f)$ is open in $X$ . By [F3] the restriction of $f$ to the open subscheme $Et (f)$ has étale locus $Et (f) \cap Et (f) = Et (f)$ , which is its whole source, so the restriction is 'etale by [F2]. For $X = \emptyset$ the locus is empty by [F3], which is open.

5.1

Choice accounting. The Axiom of Choice [F4] is assumed in the Statement and used exactly through the Jacobian criterion [F1] in steps 1.1 and 3.1; the locus description [F3] and the relative-dimension conventions [F2] are choice-free. [F1, F2, F4] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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, Lemma 29.36.6 and Section 29.36 (tag 02G4) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Chapter 26 (the etale locus is open) (standard reference, not scraped)