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

Assuming Choice, conjugates in an algebraic closure are related by a base automorphism

Statement

Assume the Axiom of Choice. Let $Ω$ be an algebraic closure of $F$ and let $α, β \in Ω$ . Then $α$ and $β$ are conjugate over $F$ if and only if some $F$ -automorphism of $Ω$ sends $α$ to $β$ .

Facts & Assumptions

Given: The Axiom of Choice, an algebraic closure $Ω / F$ , and elements $α, β \in Ω$ .

[L1]

An $F$ -embedding carries an algebraic element to a conjugate (A base-field embedding carries an algebraic element to a conjugate).

[L2]

Conjugates are roots of the same minimal polynomial over $F$ (Conjugate algebraic elements over a field).

[L3]

A chosen conjugate root induces an $F$ -isomorphism between the corresponding simple extensions (Universal property of adjoining a root of an irreducible polynomial).

[L4]

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

[L5]

An algebraic closure is an algebraic extension whose top field is algebraically closed (An algebraic closure of a field).

[L6]

Every algebraic element has a monic irreducible minimal polynomial over the base (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).

Proof

technique · direct

1.1

If an $F$ -automorphism sends $α$ to $β$ , then [L1] makes them conjugate.

1.2

Conversely, suppose they are conjugate. By [L2] and [L3], there is an $F$ -isomorphism $F (α) \to F (β)$ sending $α$ to $β$ .

L2L3

2.1

Apply [L4] with base $F (α)$ to extend this map to an embedding $τ : Ω \to Ω$ . Its image $E$ is algebraically closed because it is isomorphic to $Ω$ . Every $b \in Ω$ is algebraic over $F \subseteq E$ by [L5], so [L6] gives its minimal polynomial over $E$ ; this polynomial has a root in $E$ and is therefore linear. Hence $b \in E$ , so $τ$ is surjective and is an automorphism.

step 1.2L4L5L6

3.1

This automorphism sends $α$ to $β$ , proving the reverse implication.

step 1.2step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 44 results over 7 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, Chapters 3 to 5 (standard reference, not scraped)