Primitive Element Theorem

In this file we prove the primitive element theorem.

Main results

exists_primitive_element: a finite separable extension E / F has a primitive element, i.e. there is an α : E such that F⟮α⟯ = (⊤ : subalgebra F E).

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 is_primitive_element 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

source

theorem field.exists_primitive_element_of_fintype_top (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [fintype E] :

∃ (α : E), F⟮α⟯ = ⊤

Primitive element theorem assuming E is finite.

source

theorem field.exists_primitive_element_of_fintype_bot (F : Type u_1) [field F] (E : Type u_2) [field E] [algebra F E] [fintype F] [finite_dimensional F E] :

∃ (α : E), F⟮α⟯ = ⊤

Primitive element theorem for finite dimensional extension of a finite field.

Primitive element theorem for infinite fields

source

theorem field.primitive_element_inf_aux_exists_c {F : Type u_1} [field F] [infinite F] {E : Type u_2} [field E] (ϕ : F →+* E) (α β : E) (f g : polynomial F) :

∃ (c : F), ∀ (α' : E), α' ∈ (polynomial.map ϕ f).roots → ∀ (β' : E), β' ∈ (polynomial.map ϕ g).roots → -(α' - α) / (β' - β) ≠ ⇑ϕ c

source

theorem field.primitive_element_inf_aux {F : Type u_1} [field F] [infinite F] {E : Type u_2} [field E] (α β : E) [algebra F E] (F_sep : is_separable F E) :

∃ (γ : E), ↑F⟮α, β⟯ ⊆ ↑F⟮γ⟯

source

theorem field.exists_primitive_element_inf {F E : Type u} [field F] [field E] [algebra F E] [finite_dimensional F E] (F_sep : is_separable F E) (F_inf : infinite F) (n : ℕ) (hn : finite_dimensional.findim F E = n) :

∃ (α : E), F⟮α⟯ = ⊤

Primitive element theorem for infinite fields in the same universe.

source

theorem field.exists_primitive_element_aux {F E : Type u} [field F] [field E] [algebra F E] [finite_dimensional F E] (F_sep : is_separable F E) :

∃ (α : E), F⟮α⟯ = ⊤

Primitive element theorem for fields in the same universe.

source

theorem field.exists_primitive_element {F : Type u_1} [field F] {E : Type u_2} [field E] [algebra F E] [finite_dimensional F E] (F_sep : is_separable F E) :

∃ (α : E), F⟮α⟯ = ⊤

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).