TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

Pure inseparability and its conjugate, embedding, and separable-degree criteria

Statement

Let $F \subseteq K \subseteq Ω$ , where $K / F$ is algebraic and $Ω / F$ is an algebraic closure. The following are equivalent:

$K / F$ is purely inseparable;
every $α \in K$ has exactly one distinct conjugate over $F$ .

If $K / F$ is finite, these are also equivalent to the inclusion $K ↪ Ω$ being the only $F$ -embedding of $K$ into $Ω$ , and to $[K : F]_{s} = 1$ . Assuming the Axiom of Choice, the same unique-embedding criterion is equivalent to conditions 1 and 2 for arbitrary algebraic $K / F$ . In characteristic $p > 0$ , they are equivalent elementwise to the minimal polynomial of each $α$ having the form $x^{p^{e}} - a$ , or to $α^{p^{e}} \in F$ for some $e \geq 0$ . In characteristic zero they force $K = F$ .

Facts & Assumptions

Given: Fields $F \subseteq K \subseteq Ω$ , with $K / F$ algebraic and $Ω / F$ an algebraic closure.

[L1]

Pure inseparability is the elementwise $p$ -power condition in characteristic $p$ , and means the trivial extension in characteristic zero (Purely inseparable algebraic extensions).

[L2]

Embeddings of $F (α)$ into an algebraic closure correspond to distinct roots of the minimal polynomial ( $F$ -embeddings of $F (α)$ into an algebraically closed field correspond to the distinct roots of $m_{α}$ ).

[L3]

Assuming Choice, an embedding of a base field extends across every algebraic extension into an algebraically closed field (Assuming Choice, a base-field embedding extends across every algebraic extension).

[L4]

In characteristic $p$ , an irreducible polynomial is uniquely $g (x^{p^{e}})$ with $g$ irreducible and separable (In characteristic $p$ , every irreducible polynomial is uniquely $g (x^{p^{e}})$ with $g$ irreducible and separable).

[L5]

For a finite extension, separable degree counts its embeddings into an algebraic closure (The separable degree $[K : F]_{s}$ as a count of embeddings into an algebraic closure).

[L6]

In a finite tower, every embedding of the middle field into an algebraic closure extends to the top field (Restriction partitions embeddings in a finite tower into extension fibres).

[L7]

Every field of characteristic zero is perfect (A field is perfect exactly when it has characteristic zero or its Frobenius map is surjective).

[L8]

Every nonconstant irreducible polynomial over a perfect field is separable (Perfect fields: every irreducible polynomial is separable).

Proof

technique · direct

1.1

In characteristic $p$ , if $α^{p^{n}} = a \in F$ , then the minimal polynomial of $α$ divides $x^{p^{n}} - a = (x - α)^{p^{n}}$ in $Ω [x]$ , so it has only the distinct root $α$ . Conversely, if the minimal polynomial has one distinct root, write it as $g (x^{p^{e}})$ by [L4]; the separable polynomial $g$ can then have only one root and must be linear, so the minimal polynomial is $x^{p^{e}} - a$ and $α^{p^{e}} = a \in F$ .

L1L4algebra

1.2

If every element has one conjugate, [L2] shows that every $F$ -embedding fixes every element, so the inclusion is the only embedding. If some $α$ has a different conjugate, [L2] gives a nonidentity embedding of $F (α)$ into $Ω$ . When $K / F$ is finite, [L6] extends it across the finite tower $F \subseteq F (α) \subseteq K$ ; for arbitrary algebraic $K / F$ , [L3] gives the same extension under Choice. Thus the unique-embedding criterion is equivalent in exactly the two settings stated.

L2L3L6

2.1

Thus condition 1 is equivalent to condition 2 in positive characteristic. In characteristic zero [L7] and [L8] make every irreducible polynomial separable, so one distinct root forces degree one; hence condition 2 is equivalent to $K = F$ , which is condition 1 by [L1].

step 1.1L1L7L8

3.1

For finite $K / F$ , [L5] says that having exactly one embedding is exactly $[K : F]_{s} = 1$ . Together with steps 2.1 and 1.2, this proves the finite equivalences; step 1.2 also proves the asserted arbitrary-extension equivalence under Choice. The trivial extension is included by $e = 0$ .

step 2.1step 1.2L5∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 70 results over 13 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

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