Criteria for primitive elements

Let E / F be an extension with only finitely many intermediate fields (for instance a finite separable extension, by the primitive element theorem) and let k be an infinite subfield of F. If a k-subspace V of E generates E over F, then some element of V alone generates E over F: the primitive element can be chosen in V.

Indeed each proper intermediate field meets V in a proper k-subspace, since V generates E, and a vector space over an infinite field is not a finite union of proper subspaces (Submodule.exists_forall_notMem_of_forall_ne_top). An element of V outside all of them generates E.

The typical use is a compositum E = F F₂ of two subfields over a common infinite subfield k, with V the image of F₂: some element of F₂ is then a primitive element of E / F.

A second criterion needs no prior finite-dimensionality assumption: in a separable algebraic extension, an element generates the entire extension exactly when its minimal-polynomial degree is maximal. Apply the primitive element theorem to each two-generated subextension and compare its degree with that of the proposed generator. This turns an attained uniform bound on element degrees into a generation statement.

Main results

• Field.exists_mem_adjoin_simple_eq_top: a primitive element of E / F can be chosen in any k-subspace that generates E over F.
• Field.adjoin_simple_eq_top_iff_forall_natDegree_minpoly_le: in a separable algebraic extension, an element generates the extension if and only if its minimal-polynomial degree is maximal.

theorem Field.exists_mem_adjoin_simple_eq_top (k : Type u_1) {F : Type u_2} {E : Type u_3} [Field k] [Field F] [Field E] [Algebra k F] [Algebra k E] [Algebra F E] [IsScalarTower k F E] [Infinite k] [Finite (IntermediateField F E)] {V : Submodule k E} (hV : IntermediateField.adjoin F ↑V = ⊤) : ∃ α ∈ V, F⟮α⟯ = ⊤

A primitive element inside a generating subspace. If E / F has only finitely many intermediate fields (for instance if it is finite separable, by the primitive element theorem), k ⊆ F is infinite, and the k-subspace V of E generates E over F, then F⟮α⟯ = E for some α ∈ V.

theorem Field.adjoin_simple_eq_top_iff_forall_natDegree_minpoly_le {F : Type u_4} {E : Type u_5} [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] (α : E) : F⟮α⟯ = ⊤ ↔ ∀ (β : E), (minpoly F β).natDegree ≤ (minpoly F α).natDegree

In a separable algebraic extension, an element generates the whole extension if and only if its minimal-polynomial degree bounds those of all elements. No finite-dimensionality assumption on the extension is needed.