TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17

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.

Assuming Choice, a base-field embedding extends across every algebraic extension

Statement

Assume the Axiom of Choice. Let $K / F$ be algebraic, let $Ω$ be algebraically closed, and let $σ : F \to Ω$ be a field embedding. Then $σ$ extends to a field embedding $\tilde{σ} : K \to Ω$ . The proof uses Zorn's lemma.

Facts & Assumptions

Given: The Axiom of Choice, an algebraic extension $K / F$ , an algebraically closed field $Ω$ , and an embedding $σ : F \to Ω$ .

[L1]

Assuming Choice, a nonempty poset in which every chain has an upper bound has a maximal element (Zorn's lemma).

[L2]

A chosen root of an irreducible polynomial induces the unique embedding of the corresponding simple root extension (Universal property of adjoining a root of an irreducible polynomial).

[L3]

A field isomorphism transports coefficients, evaluation, and roots of polynomials (A field isomorphism transports polynomials coefficientwise and carries roots, factorizations, and splitting to roots, factorizations, and splitting).

[L4]

Relative embeddings are field embeddings agreeing with the specified map on the base ( $F$ -homomorphisms and $F$ -embeddings of field extensions).

[L5]

Every nonconstant polynomial over an algebraically closed field has a root (An algebraically closed field: every nonconstant polynomial has a root in the field).

Proof

technique · direct

1.1

Let $P$ consist of pairs $(E, τ)$ where $F \subseteq E \subseteq K$ is an intermediate field and $τ : E \to Ω$ is an embedding extending $σ$ , ordered by extension of the domain and map. The pair $(F, σ)$ shows that $P$ is nonempty.

L4construct

2.1

The union of a chain of such pairs has the union of the domains as an intermediate field and the union of the compatible maps as an embedding into $Ω$ , so every chain has an upper bound.

step 1.1L4

3.1

By Zorn's lemma [L1], choose a maximal pair $(M, τ)$ in $P$ .

step 1.1step 2.1L1choose

4.1

If $M \neq K$ , choose $α \in K ∖ M$ . It is algebraic over $M$ . Transport its minimal polynomial through the isomorphism $M \to τ (M)$ using [L3], choose a root in $Ω$ by [L5], and use [L2] to extend $τ$ to an embedding of $M (α)$ .

step 3.1L2L3L5choose

5.1

Step 4.1 contradicts maximality unless $M = K$ . Thus $τ$ on the maximal domain is the required extension of $σ$ ; the use of Choice is precisely [L1].

step 3.1step 4.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 39 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. S. Milne, Fields and Galois Theory, Chapter 6 (standard reference, not scraped)
P. L. Clark, Field Theory, Chapter 4 (standard reference, not scraped)