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.
Restriction partitions embeddings in a finite tower into extension fibres
Statement
Let be a finite tower and let be an algebraic closure of . Restriction defines a surjection
For every -embedding , its fibre is nonempty and has cardinality after transporting the -structure along .
Facts & Assumptions
Given: A finite tower , an algebraic closure , and an -embedding .
Relative embeddings are field embeddings fixing the specified base map (-homomorphisms and -embeddings of field extensions).
A finite extension has a finite basis over its base (The degree of a finite field extension).
A field isomorphism transports polynomial coefficients, evaluation, and roots (A field isomorphism transports polynomials coefficientwise and carries roots, factorizations, and splitting to roots, factorizations, and splitting).
A chosen root of a transported irreducible polynomial induces the unique embedding of the corresponding simple root extension (Universal property of adjoining a root of an irreducible polynomial).
Every nonconstant polynomial over an algebraically closed field has a root (An algebraically closed field: every nonconstant polynomial has a root in the field).
For a finite extension, the number of base-field embeddings into an algebraic closure is independent of the chosen algebraic closure (The separable degree is independent of the chosen algebraic closure).
Proof
Restricting an -embedding to gives an -embedding by [L1].
To extend a chosen , take a finite -basis of by [L2] and put . Starting with , regard each as an isomorphism onto its image, transport the minimal polynomial of over along it by [L3], choose a root in by [L5], and extend to by [L4]. After finitely many steps, , so every has an extension and the restriction map is surjective.
Identify with . The extensions of are exactly the -embeddings of the scalar-transported copy of into . Since is algebraically closed and algebraic over , it is an algebraic closure of that copy of .
Transporting scalars and maps along the isomorphism identifies the embeddings in step 1.3 with embeddings of into an algebraic closure of . By [L6], their number is the closure-independent value . Thus every fibre of restriction has that cardinality.
In particular, transport along an isomorphism between two embedded copies of gives a bijection between their restriction fibres.
Depends on
- $F$-homomorphisms and $F$-embeddings of field extensions
- The degree $[K:F]=\dim_F K$ of a finite field extension
- A field isomorphism transports polynomials coefficientwise and carries roots, factorizations, and splitting to roots, factorizations, and splitting
- Universal property of adjoining a root of an irreducible polynomial
- An algebraically closed field: every nonconstant polynomial has a root in the field
- The separable degree is independent of the chosen algebraic closure
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 52 results over 10 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)