Primitive Element Theorem #
In this file we prove the primitive element theorem.
Main results #
exists_primitive_element: a finite separable extensionE / Fhas a primitive element, i.e. there is anα : Esuch thatF⟮α⟯ = (⊤ : Subalgebra F E).exists_primitive_element_iff_finite_intermediateField: a finite extensionE / Fhas a primitive element if and only if there exist only finitely many intermediate fields betweenEandF.
Implementation notes #
In declaration names, primitive_element abbreviates adjoin_simple_eq_top:
it stands for the statement F⟮α⟯ = (⊤ : Subalgebra F E). We did not add an extra
declaration IsPrimitiveElement F α := F⟮α⟯ = (⊤ : Subalgebra F E) because this
requires more unfolding without much obvious benefit.
Tags #
primitive element, separable field extension, separable extension, intermediate field, adjoin, exists_adjoin_simple_eq_top
Primitive element theorem for finite fields #
Primitive element theorem for infinite fields #
This is the heart of the proof of the primitive element theorem. It shows that if F is
infinite and α and β are separable over F then F⟮α, β⟯ is generated by a single element.
Primitive element theorem: a finite separable field extension E of F has a
primitive element, i.e. there is an α ∈ E such that F⟮α⟯ = (⊤ : Subalgebra F E).
Alternative phrasing of primitive element theorem:
a finite separable field extension has a basis 1, α, α^2, ..., α^n.
See also exists_primitive_element.
Equations
- Field.powerBasisOfFiniteOfSeparable F E = (IntermediateField.adjoin.powerBasis ⋯).map ((IntermediateField.equivOfEq ⋯).trans IntermediateField.topEquiv)
Instances For
Alias of Field.FiniteDimensional.of_finite_intermediateField.
Alias of Field.FiniteDimensional.of_exists_primitive_element.
Steinitz theorem: an algebraic extension E of F has a
primitive element (i.e. there is an α ∈ E such that F⟮α⟯ = (⊤ : Subalgebra F E))
if and only if there exist only finitely many intermediate fields between E and F.