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.
FALSE: an algebraic closure is unique up to a unique base-field isomorphism
Statement
For any two algebraic closures of a field , there is exactly one -isomorphism between them.
Facts & Assumptions
Given: The axiom of Choice and the field .
Assuming Choice, every field has an algebraic closure (Assuming Choice, every field has an algebraic closure).
Embeddings of a simple extension correspond to the distinct roots of its minimal polynomial (-embeddings of into an algebraically closed field correspond to the distinct roots of ).
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).
Assuming Choice, any two algebraic closures of the same field are isomorphic over that field (Assuming Choice, any two algebraic closures are base-isomorphic).
An algebraic closure is algebraic over its base and algebraically closed (An algebraic closure of a field).
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).
Refutation
Choose by [L1]. The polynomial is irreducible over and has a root by [L5]. Its roots and are distinct because has characteristic zero. By [L2], the assignment gives a nonidentity -embedding of into .
Extend that embedding across the algebraic extension using [L3]. Its image is algebraically closed because it is isomorphic to . Every is algebraic over by [L5], so [L6] gives a minimal polynomial over ; it has a root in and is therefore linear. Thus the resulting embedding is surjective, hence is a nonidentity -automorphism with .
The identity and are distinct -isomorphisms from the same algebraic closure to itself. Therefore uniqueness of the base-field isomorphism is false, although existence is true by [L4].
Depends on
- Assuming Choice, every field has an algebraic closure
- $F$-embeddings of $F(\alpha)$ into an algebraically closed field correspond to the distinct roots of $m_{\alpha}$
- Assuming Choice, a base-field embedding extends across every algebraic extension
- Assuming Choice, any two algebraic closures are base-isomorphic
- An algebraic closure of a field
- The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element
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: 48 results over 8 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)