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.

Finite field extensions and etaleness

Statement

Let $k$ be a field and let $L / k$ be a finite field extension (The degree $[K : F] = \dim_{F} K$ of a finite field extension), with structure morphism $f ⁣ : Spec L ⟶ Spec k .$ Then $f$ is finite 'etale (Finite morphisms of schemes, Étale morphism of schemes) if and only if the extension $L / k$ is separable (Separable algebraic elements and separable extensions).

Assume the Axiom of Choice (The Axiom of Choice) for the forward implication, which uses the separability of residue fields of morphisms with vanishing differentials; the reverse implication is choice-free.

Facts & Assumptions

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

[F1]

'Etale at $x$ implies locally of finite presentation and flat at $x$ , and for locally finitely presented morphisms 'etale at $x$ is equivalent to flat and unramified at $x$ , where unramifiedness is equivalent to the vanishing of $Ω_{X / S, x}$ (Étale morphism of schemes, Étale equals flat and unramified in finite presentation, Unramified morphism, Formal unramifiedness iff Omega vanishes).

[F2]

Assume AC. If $f$ is locally of finite type at $x$ and $Ω_{X / S, x} = 0$ , then $κ (x) / κ (s)$ is a finite separable extension (Unramified residue extensions are finite separable).

[F3]

A finite separable extension $L / k$ is simple: $L = k (α)$ for some $α$ , whose minimal polynomial $P \in k [T]$ is monic and separable, and evaluation at $α$ identifies $k [T] / (P) ≅ k (α) = L$ (A finite extension generated by elements all but possibly one of which are separable is simple, The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element, Separable algebraic elements and separable extensions).

[F4]

For $0 \neq P \in k [T]$ , $P$ is separable if and only if $\gcd (P, P^{'}) = 1$ , and in that case Bezout supplies $A, B \in k [T]$ with $A P + B P^{'} = 1$ (A nonzero polynomial over a field is separable exactly when its gcd with its derivative is $1$ , Bézout identity and the Euclidean algorithm for polynomials over a field).

[F5]

If $P \in A [T]$ is monic and the image of $P^{'}$ is a unit of $(A [T] / (P))_{g}$ , then $(A [T] / (P))_{g}$ is standard 'etale over $A$ ; a standard 'etale $A$ -algebra is 'etale over $A$ in the sense of Étale morphism of schemes when $A \to B$ is finitely presented, and $A [T] / (P)$ with $P$ monic is finitely presented because $A [T]$ is a finitely presented $A$ -algebra and $(P)$ is a finitely generated ideal (Standard étale algebra, Finitely presented modules and finitely presented algebras, Locally finite presentation morphisms).

[F6]

A finite field extension $L / k$ is finite-dimensional as a $k$ -vector space, hence a finite $k$ -module; a morphism $Spec B \to Spec A$ is finite when $B$ is a module-finite $A$ -algebra (The degree $[K : F] = \dim_{F} K$ of a finite field extension, Finite morphisms of schemes).

[F7]

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

Proof

technique · direct

1.1F1F2

Forward: 'etale implies separable. Assume $f$ is finite 'etale. Then $f$ is 'etale, hence locally of finite presentation, in particular locally of finite type at every point; let $x$ be the unique point of $Spec L$ and $s$ the unique point of $Spec k$ . By [F1] 'etaleness at $x$ gives unramifiedness at $x$ , equivalently $Ω_{X / S, x} = 0$ . By [F2] (AC) the residue extension $κ (x) / κ (s)$ is finite separable. Here $κ (x) = L$ and $κ (s) = k$ , so $L / k$ is finite separable.

1.2F3F4F5

Reverse: separable implies standard 'etale. Assume $L / k$ is finite separable. By [F3] $L = k (α)$ for some $α$ with monic minimal polynomial $P \in k [T]$ and $k [T] / (P) ≅ L$ ; the element $α$ is separable over $k$ because every element of the separable extension is, so $P$ is separable and $\gcd (P, P^{'}) = 1$ by [F4]. Bezout [F4] gives $A, B \in k [T]$ with $A P + B P^{'} = 1$ ; reducing modulo $P$ exhibits the class of $P^{'}$ as a unit of $k [T] / (P)$ . With $g = 1$ in the presentation $k [T] / (P) = (k [T] / (P))_{1}$ , the algebra $k [T] / (P)$ is standard 'etale over $k$ by [F5], and since it is finitely presented over $k$ it is 'etale over $k$ ; transport along the isomorphism $k [T] / (P) ≅ L$ makes $Spec L \to Spec k$ 'etale.

2.1F6step 1.1step 1.2

Finiteness and conclusion. By [F6] the algebra $L$ is a finite $k$ -module, so the morphism $Spec L \to Spec k$ is finite; together with step 1.2 it is finite 'etale. Combined with step 1.1 this proves both implications.

3.1

Choice accounting. The Axiom of Choice [F7] is assumed in the Statement and used exactly through the residue-field lemma [F2] in step 1.1; the primitive-element, Bezout and standard-'etale arguments of steps 1.2 and 2.1 are choice-free, and the statement records this asymmetry. [F2, F7, step 1.1] $□$

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

87 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 (tag 02G4) and Algebra, Section 10.143 (standard etale) (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022 public draft, Chapter 26 (finite etale k-schemes and separable extensions) (standard reference, not scraped)