Alphabeta MathHow 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.
The separable degree as a count of embeddings into an algebraic closure
Definition
Let be a finite field extension (The degree of a finite field extension) and let be an algebraic closure. Assuming Choice, such a field exists by Assuming Choice, every field has an algebraic closure. The separable degree of is
where denotes the set of -embeddings of -homomorphisms and -embeddings of field extensions. This set is finite: a finite -basis generates , an embedding is determined by the images of those finitely many generators, and each image is among the finitely many roots of its minimal polynomial by -embeddings of into an algebraically closed field correspond to the distinct roots of . Thus its cardinality is defined by The cardinality of a finite set. The value is independent of the chosen algebraic closure by The separable degree is independent of the chosen algebraic closure ↗.
Depends on
- $F$-homomorphisms and $F$-embeddings of field extensions
- An algebraic closure of a field
- The degree $[K:F]=\dim_F K$ of a finite field extension
- 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}$
- The cardinality $\lvert A\rvert$ of a finite set
Used by
- The separable degree of F(α)/F is the number of distinct roots of m_α Corollary
- Aut(K/F) is a group and |Aut(K/F)|≤ [K:F]ₛ≤ [K:F] Theorem
- Equivalent characterizations of a finite Galois extension Theorem
- Norm and trace from embeddings, with the inseparable exponent in the norm formula Theorem
- Pure inseparability and its conjugate, embedding, and separable-degree criteria Theorem
- Separable degree is multiplicative in finite towers: [L:F]ₛ=[L:K]ₛ[K:F]ₛ Theorem
- The separable degree is independent of the chosen algebraic closure Theorem
Dependency tree · two levels
22 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on 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)