Characterization of primitive elements in field extensions

Stream: Is there code for X?

[Xavier Roblot]

I could not find the following characterisations of primitive elements in finite extension of fields:

import Mathlib.FieldTheory.PrimitiveElement

open FiniteDimensional IntermediateField

variable {F E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E]

theorem aux1 (α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E := by
  refine ⟨fun h => ?_, fun h => ?_⟩
  · rw [← adjoin.finrank (isIntegral_of_finite F α), h, ← finrank_top F E]
    rfl
  · refine IntermediateField.eq_of_le_of_finrank_eq le_top ?_
    rw [adjoin.finrank (isIntegral_of_finite F α), h, ← finrank_top]
    rfl

variable [IsSeparable F E] {A : Type*} [Field A] [IsAlgClosed A] [Algebra F A]

theorem aux2 (α : E) : F⟮α⟯ = ⊤ ↔ ∀ φ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ := by
  classical
  rw [aux1, ← Polynomial.card_rootSet_eq_natDegree (K := A) (IsSeparable.separable F α)
    (IsAlgClosed.splits_codomain (minpoly F α)), ← AlgHom.card F E A, ← Set.toFinset_card]
  simp_rw [← Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly A
    (Algebra.isAlgebraic_of_finite F E) α]
  rw [Fintype.card, Set.toFinset_range (fun f : E →ₐ[F] A ↦ f α), Finset.card_image_iff,
    Finset.coe_univ, ← Set.injective_iff_injOn_univ]
  rfl

[Anne Baanen]

I think the forward direction of both exists for docs#PowerBasis, up to heavy rephrasing, and aux1 might exist in both directions. In any case, there would be sufficient work to connect this to existing machinery that I see the value in adding this to Mathlib.

[Riccardo Brasca]

We have docs#IntermediateField.powerBasisAux that looks close

[Riccardo Brasca]

I thought we had something with the explicit assumption that the degree of the minpoly is the dimension, but I don't find it. Anyway it seems a good addition.

[Xavier Roblot]

#8609