Documentation

Mathlib.FieldTheory.PrimitiveElement

Primitive Element Theorem #

In this file we prove the primitive element theorem.

Main results #

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 #

theorem Field.exists_primitive_element_of_finite_top (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [Finite E] :
∃ (α : E), Fα =

Primitive element theorem assuming E is finite.

theorem Field.exists_primitive_element_of_finite_bot (F : Type u_1) [Field F] (E : Type u_2) [Field E] [Algebra F E] [Finite F] [FiniteDimensional F E] :
∃ (α : E), Fα =

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

Primitive element theorem for infinite fields #

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) (β : E) (f : Polynomial F) (g : Polynomial F) :
∃ (c : F), α'(Polynomial.map ϕ f).roots, β'(Polynomial.map ϕ g).roots, -(α' - α) / (β' - β) ϕ c
theorem Field.primitive_element_inf_aux (F : Type u_1) [Field F] [Infinite F] {E : Type u_2} [Field E] (α : E) (β : E) [Algebra F E] [Algebra.IsSeparable F E] :
∃ (γ : E), Fα, β = Fγ

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.

theorem Field.exists_primitive_element (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable 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).

noncomputable def Field.powerBasisOfFiniteOfSeparable (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable 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
Instances For
    theorem Field.isAlgebraic_of_adjoin_eq_adjoin (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] {α : E} {m : } {n : } (hneq : m n) (heq : Fα ^ m = Fα ^ n) :
    @[deprecated Field.FiniteDimensional.of_finite_intermediateField]

    Alias of Field.FiniteDimensional.of_finite_intermediateField.

    theorem Field.exists_primitive_element_of_finite_intermediateField (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Finite (IntermediateField F E)] (K : IntermediateField F E) :
    ∃ (α : E), Fα = K
    theorem Field.FiniteDimensional.of_exists_primitive_element (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (h : ∃ (α : E), Fα = ) :
    @[deprecated Field.FiniteDimensional.of_exists_primitive_element]
    theorem Field.finiteDimensional_of_exists_primitive_element (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (h : ∃ (α : E), Fα = ) :

    Alias of Field.FiniteDimensional.of_exists_primitive_element.

    theorem Field.finite_intermediateField_of_exists_primitive_element (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (h : ∃ (α : E), Fα = ) :
    theorem Field.exists_primitive_element_iff_finite_intermediateField (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] :
    (Algebra.IsAlgebraic F E ∃ (α : E), Fα = ) Finite (IntermediateField F E)

    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.

    @[simp]
    theorem AlgHom.card (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (K : Type u_3) [Field K] [IsAlgClosed K] [Algebra F K] :
    @[simp]
    theorem AlgHom.card_of_splits (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (L : Type u_3) [Field L] [Algebra F L] (hL : ∀ (x : E), Polynomial.Splits (algebraMap F L) (minpoly F x)) :
    theorem Field.primitive_element_iff_minpoly_natDegree_eq (F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (α : E) :
    Fα = (minpoly F α).natDegree = Module.finrank F E
    theorem Field.primitive_element_iff_minpoly_degree_eq (F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] (α : E) :
    Fα = (minpoly F α).degree = (Module.finrank F E)
    theorem Field.primitive_element_iff_algHom_eq_of_eval' (F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (A : Type u_5) [Field A] [Algebra F A] (hA : ∀ (x : E), Polynomial.Splits (algebraMap F A) (minpoly F x)) (α : E) :
    Fα = Function.Injective fun (φ : E →ₐ[F] A) => φ α
    theorem Field.primitive_element_iff_algHom_eq_of_eval (F : Type u_3) {E : Type u_4} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] (A : Type u_5) [Field A] [Algebra F A] (hA : ∀ (x : E), Polynomial.Splits (algebraMap F A) (minpoly F x)) (α : E) (φ : E →ₐ[F] A) :
    Fα = ∀ (ψ : E →ₐ[F] A), φ α = ψ αφ = ψ