Mathlib.FieldTheory.PrimitiveElement

Module docstring

{"# Primitive Element Theorem

In this file we prove the primitive element theorem.

Main results

Field.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).
Field.exists_primitive_element_iff_finite_intermediateField: a finite extension E / F has a primitive element if and only if there exist only finitely many intermediate fields between E and F.

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, existsadjoinsimpleeqtop

","### Primitive element theorem for finite fields ","### Primitive element theorem for infinite fields "}

Field.exists_primitive_element_of_finite_top theorem

[Finite E] : ∃ α : E, F⟮α⟯ = ⊤

Full source

/-- **Primitive element theorem** assuming E is finite. -/
@[stacks 09HY "second part"]
theorem exists_primitive_element_of_finite_top [Finite E] : ∃ α : E, F⟮α⟯ = ⊤ := by
  obtain ⟨α, hα⟩ := @IsCyclic.exists_generator Eˣ _ _
  use α
  rw [eq_top_iff]
  rintro x -
  by_cases hx : x = 0
  · rw [hx]
    exact F⟮α.val⟯.zero_mem
  · obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))
    rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0]]
    exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n

Primitive Element Theorem for Finite Field Extensions

Informal description

For any finite field extension $E$ of a field $F$, there exists an element $\alpha \in E$ such that the smallest intermediate field containing both $F$ and $\alpha$ is equal to $E$ itself, i.e., $F(\alpha) = E$.

Field.exists_primitive_element_of_finite_bot theorem

[Finite F] [FiniteDimensional F E] : ∃ α : E, F⟮α⟯ = ⊤

Full source

/-- Primitive element theorem for finite dimensional extension of a finite field. -/
theorem exists_primitive_element_of_finite_bot [Finite F] [FiniteDimensional F E] :
    ∃ α : E, F⟮α⟯ = ⊤ :=
  haveI : Finite E := Module.finite_of_finite F
  exists_primitive_element_of_finite_top F E

Primitive Element Theorem for Finite-Dimensional Extensions of Finite Fields

Informal description

Let $F$ be a finite field and $E$ a finite-dimensional field extension of $F$. Then there exists an element $\alpha \in E$ such that the smallest intermediate field containing both $F$ and $\alpha$ is equal to $E$ itself, i.e., $F(\alpha) = E$.

Field.primitive_element_inf_aux_exists_c theorem

(f g : F[X]) : ∃ c : F, ∀ α' ∈ (f.map ϕ).roots, ∀ β' ∈ (g.map ϕ).roots, -(α' - α) / (β' - β) ≠ ϕ c

Full source

theorem primitive_element_inf_aux_exists_c (f g : F[X]) :
    ∃ c : F, ∀ α' ∈ (f.map ϕ).roots, ∀ β' ∈ (g.map ϕ).roots, -(α' - α) / (β' - β) ≠ ϕ c := by
  classical
  let sf := (f.map ϕ).roots
  let sg := (g.map ϕ).roots
  classical
  let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
  let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
  obtain ⟨c, hc⟩ := Infinite.exists_not_mem_finset s'
  simp_rw [s', s, Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map]
    at hc
  push_neg at hc
  exact ⟨c, hc⟩

Existence of Field Element Avoiding Cross-Ratios of Roots in Primitive Element Construction

Informal description

Let $F$ be a field and $E$ be a field extension of $F$ with $\alpha, \beta \in E$. Given separable polynomials $f, g \in F[X]$ with roots $\alpha'$ and $\beta'$ respectively under the embedding $\phi: F \to E$, there exists an element $c \in F$ such that for all roots $\alpha'$ of $f \circ \phi$ and $\beta'$ of $g \circ \phi$, the expression $-(\alpha' - \alpha)/(\beta' - \beta)$ is not equal to $\phi(c)$.

Field.primitive_element_inf_aux theorem

[Algebra.IsSeparable F E] : ∃ γ : E, F⟮α, β⟯ = F⟮γ⟯

Full source

/-- 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 primitive_element_inf_aux [Algebra.IsSeparable F E] : ∃ γ : E, F⟮α, β⟯ = F⟮γ⟯ := by
  classical
  have hα := Algebra.IsSeparable.isIntegral F α
  have hβ := Algebra.IsSeparable.isIntegral F β
  let f := minpoly F α
  let g := minpoly F β
  let ιFE := algebraMap F E
  let ιEE' := algebraMap E (SplittingField (g.map ιFE))
  obtain ⟨c, hc⟩ := primitive_element_inf_aux_exists_c (ιEE'.comp ιFE) (ιEE' α) (ιEE' β) f g
  let γ := α + c • β
  suffices β_in_Fγ : β ∈ F⟮γ⟯ by
    use γ
    apply le_antisymm
    · rw [adjoin_le_iff]
      have α_in_Fγ : α ∈ F⟮γ⟯ := by
        rw [← add_sub_cancel_right α (c • β)]
        exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
      rintro x (rfl | rfl) <;> assumption
    · rw [adjoin_simple_le_iff]
      have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert α {β})
      have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F {α, β} (Set.mem_insert_of_mem α rfl)
      exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)
  classical
  let p := EuclideanDomain.gcd ((f.map (algebraMap F F⟮γ⟯)).comp
    (C (AdjoinSimple.gen F γ) - (C ↑c : F⟮γ⟯F⟮γ⟯[X]) * X)) (g.map (algebraMap F F⟮γ⟯))
  let h := EuclideanDomain.gcd ((f.map ιFE).comp (C γ - C (ιFE c) * X)) (g.map ιFE)
  have map_g_ne_zero : g.map ιFE ≠ 0 := map_ne_zero (minpoly.ne_zero hβ)
  have h_ne_zero : h ≠ 0 :=
    mt EuclideanDomain.gcd_eq_zero_iff.mp (not_and.mpr fun _ => map_g_ne_zero)
  suffices p_linear : p.map (algebraMap F⟮γ⟯ E) = C h.leadingCoeff * (X - C β) by
    have finale : β = algebraMap F⟮γ⟯ E (-p.coeff 0 / p.coeff 1) := by
      simp [map_div₀, RingHom.map_neg, ← coeff_map, ← coeff_map, p_linear,
        mul_sub, coeff_C, mul_div_cancel_left₀ β (mt leadingCoeff_eq_zero.mp h_ne_zero)]
    rw [finale]
    exact Subtype.mem (-p.coeff 0 / p.coeff 1)
  have h_sep : h.Separable := separable_gcd_right _ (Algebra.IsSeparable.isSeparable F β).map
  have h_root : h.eval β = 0 := by
    apply eval_gcd_eq_zero
    · rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map, ← aeval_def, ←
        Algebra.smul_def, add_sub_cancel_right, minpoly.aeval]
    · rw [eval_map, ← aeval_def, minpoly.aeval]
  have h_splits : Splits ιEE' h :=
    splits_of_splits_gcd_right ιEE' map_g_ne_zero (SplittingField.splits _)
  have h_roots : ∀ x ∈ (h.map ιEE').roots, x = ιEE' β := by
    intro x hx
    rw [mem_roots_map h_ne_zero] at hx
    specialize hc (ιEE' γ - ιEE' (ιFE c) * x) (by
      have f_root := root_left_of_root_gcd hx
      rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
      exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root)
    specialize hc x (by
      rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
      exact root_right_of_root_gcd hx)
    by_contra a
    apply hc
    apply (div_eq_iff (sub_ne_zero.mpr a)).mpr
    simp only [γ, Algebra.smul_def, RingHom.map_add, RingHom.map_mul, RingHom.comp_apply]
    ring
  rw [← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots]
  trans EuclideanDomain.gcd (?_ : E[X]) (?_ : E[X])
  · dsimp only [γ]
    convert (gcd_map (algebraMap F⟮γ⟯ E)).symm
  · simp only [map_comp, Polynomial.map_map, ← IsScalarTower.algebraMap_eq, Polynomial.map_sub,
      map_C, AdjoinSimple.algebraMap_gen, map_add, Polynomial.map_mul, map_X]
    congr

Existence of Primitive Element for Bivariate Separable Extensions

Informal description

Let $E/F$ be a separable field extension. For any two elements $\alpha, \beta \in E$, there exists an element $\gamma \in E$ such that the field extension $F(\alpha, \beta)$ is equal to $F(\gamma)$.

Field.exists_primitive_element theorem

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

Full source

/-- **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)`. -/
@[stacks 030N "The moreover part"]
theorem exists_primitive_element : ∃ α : E, F⟮α⟯ = ⊤ := by
  rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)
  · let P : IntermediateField F E → Prop := fun K => ∃ α : E, F⟮α⟯ = K
    have base : P ⊥ := ⟨0, adjoin_zero⟩
    have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F) := by
      intro K β hK
      obtain ⟨α, hK⟩ := hK
      rw [← hK, adjoin_simple_adjoin_simple]
      haveI : Infinite F := isEmpty_fintype.mp F_inf
      obtain ⟨γ, hγ⟩ := primitive_element_inf_aux F α β
      exact ⟨γ, hγ.symm⟩
    exact induction_on_adjoin P base ih ⊤
  · exact exists_primitive_element_of_finite_bot F E

Primitive Element Theorem for Finite Separable Extensions

Informal description

Let $E/F$ be a finite separable field extension. Then there exists an element $\alpha \in E$ such that the smallest intermediate field containing $F$ and $\alpha$ is equal to $E$ itself, i.e., $F(\alpha) = E$.

Field.powerBasisOfFiniteOfSeparable definition

: PowerBasis F E

Full source

/-- Alternative phrasing of primitive element theorem:
a finite separable field extension has a basis `1, α, α^2, ..., α^n`.

See also `exists_primitive_element`. -/
noncomputable def powerBasisOfFiniteOfSeparable : PowerBasis F E :=
  let α := (exists_primitive_element F E).choose
  let pb := adjoin.powerBasis (Algebra.IsSeparable.isIntegral F α)
  have e : F⟮α⟯ = ⊤ := (exists_primitive_element F E).choose_spec
  pb.map ((IntermediateField.equivOfEq e).trans IntermediateField.topEquiv)

Power basis for finite separable extensions

Informal description

Given a finite separable field extension $ E $ of $ F $, there exists a power basis for $ E $ over $ F $. That is, there exists an element $ \alpha \in E $ such that $ \{1, \alpha, \alpha^2, \ldots, \alpha^{n-1}\} $ forms a basis for $ E $ as an $ F $-vector space, where $ n = [E:F] $ is the degree of the extension.

Field.isAlgebraic_of_adjoin_eq_adjoin theorem

{α : E} {m n : ℕ} (hneq : m ≠ n) (heq : F⟮α ^ m⟯ = F⟮α ^ n⟯) : IsAlgebraic F α

Full source

theorem isAlgebraic_of_adjoin_eq_adjoin {α : E} {m n : ℕ} (hneq : m ≠ n)
    (heq : F⟮α ^ m⟯ = F⟮α ^ n⟯) : IsAlgebraic F α := by
  wlog hmn : m < n
  · exact this F E hneq.symm heq.symm (hneq.lt_or_lt.resolve_left hmn)
  by_cases hm : m = 0
  · rw [hm] at heq hmn
    simp only [pow_zero, adjoin_one] at heq
    obtain ⟨y, h⟩ := mem_bot.1 (heq.symm ▸ mem_adjoin_simple_self F (α ^ n))
    refine ⟨X ^ n - C y, X_pow_sub_C_ne_zero hmn y, ?_⟩
    simp only [map_sub, map_pow, aeval_X, aeval_C, h, sub_self]
  obtain ⟨r, s, h⟩ := (mem_adjoin_simple_iff F _).1 (heq ▸ mem_adjoin_simple_self F (α ^ m))
  by_cases hzero : aeval (α ^ n) s = 0
  · simp only [hzero, div_zero, pow_eq_zero_iff hm] at h
    exact h.symm ▸ isAlgebraic_zero
  replace hm : 0 < m := Nat.pos_of_ne_zero hm
  rw [eq_div_iff hzero, ← sub_eq_zero] at h
  replace hzero : s ≠ 0 := by rintro rfl; simp only [map_zero, not_true_eq_false] at hzero
  let f : F[X] := X ^ m * expand F n s - expand F n r
  refine ⟨f, ?_, ?_⟩
  · have : f.coeff (n * s.natDegree + m) ≠ 0 := by
      have hn : 0 < n := by linarith only [hm, hmn]
      have hndvd : ¬ n ∣ n * s.natDegree + m := by
        rw [← Nat.dvd_add_iff_right (n.dvd_mul_right s.natDegree)]
        exact Nat.not_dvd_of_pos_of_lt hm hmn
      simp only [f, coeff_sub, coeff_X_pow_mul, s.coeff_expand_mul' hn, coeff_natDegree,
        coeff_expand hn r, hndvd, ite_false, sub_zero]
      exact leadingCoeff_ne_zero.2 hzero
    intro h
    simp only [h, coeff_zero, ne_eq, not_true_eq_false] at this
  · simp only [f, map_sub, map_mul, map_pow, aeval_X, expand_aeval, h]

Algebraicity from Equal Adjoint Fields of Distinct Powers

Informal description

Let $E$ be a field extension of $F$ and $\alpha \in E$. For any distinct natural numbers $m, n \in \mathbb{N}$, if the adjunction fields satisfy $F(\alpha^m) = F(\alpha^n)$, then $\alpha$ is algebraic over $F$.

Field.isAlgebraic_of_finite_intermediateField theorem

[Finite (IntermediateField F E)] : Algebra.IsAlgebraic F E

Full source

theorem isAlgebraic_of_finite_intermediateField
    [Finite (IntermediateField F E)] : Algebra.IsAlgebraic F E := ⟨fun α ↦
  have ⟨_m, _n, hneq, heq⟩ := Finite.exists_ne_map_eq_of_infinite fun n ↦ F⟮α ^ n⟯
  isAlgebraic_of_adjoin_eq_adjoin F E hneq heq⟩

Algebraicity from Finiteness of Intermediate Fields

Informal description

If a field extension $E/F$ has only finitely many intermediate fields, then every element of $E$ is algebraic over $F$.

Field.FiniteDimensional.of_finite_intermediateField theorem

[Finite (IntermediateField F E)] : FiniteDimensional F E

Full source

theorem FiniteDimensional.of_finite_intermediateField
    [Finite (IntermediateField F E)] : FiniteDimensional F E := by
  let IF := { K : IntermediateField F E // ∃ x, K = F⟮x⟯ }
  have := isAlgebraic_of_finite_intermediateField F E
  haveI : ∀ K : IF, FiniteDimensional F K.1 := fun ⟨_, x, rfl⟩ ↦ adjoin.finiteDimensional
    (Algebra.IsIntegral.isIntegral _)
  have hfin := finiteDimensional_iSup_of_finite (t := fun K : IF ↦ K.1)
  have htop : ⨆ K : IF, K.1 = ⊤ := le_top.antisymm fun x _ ↦
    le_iSup (fun K : IF ↦ K.1) ⟨F⟮x⟯, x, rfl⟩ <| mem_adjoin_simple_self F x
  rw [htop] at hfin
  exact topEquiv.toLinearEquiv.finiteDimensional

Finite-dimensionality from finiteness of intermediate fields

Informal description

If a field extension $E/F$ has only finitely many intermediate fields, then $E$ is finite-dimensional as a vector space over $F$.

Field.exists_primitive_element_of_finite_intermediateField theorem

[Finite (IntermediateField F E)] (K : IntermediateField F E) : ∃ α : E, F⟮α⟯ = K

Full source

theorem exists_primitive_element_of_finite_intermediateField
    [Finite (IntermediateField F E)] (K : IntermediateField F E) : ∃ α : E, F⟮α⟯ = K := by
  haveI := FiniteDimensional.of_finite_intermediateField F E
  rcases finite_or_infinite F with (_ | _)
  · obtain ⟨α, h⟩ := exists_primitive_element_of_finite_bot F K
    exact ⟨α, by simpa only [lift_adjoin_simple, lift_top] using congr_arg lift h⟩
  · apply induction_on_adjoin (fun K ↦ ∃ α : E, F⟮α⟯ = K) ⟨0, adjoin_zero⟩
    rintro K β ⟨α, rfl⟩
    simp_rw [adjoin_simple_adjoin_simple, eq_comm]
    exact primitive_element_inf_aux_of_finite_intermediateField F α β

Existence of Primitive Elements for Intermediate Fields in Extensions with Finitely Many Intermediate Fields

Informal description

Let $E/F$ be a field extension with finitely many intermediate fields. Then for any intermediate field $K$ between $F$ and $E$, there exists an element $\alpha \in E$ such that $K = F(\alpha)$, where $F(\alpha)$ denotes the smallest intermediate field containing both $F$ and $\alpha$.

Field.FiniteDimensional.of_exists_primitive_element theorem

[Algebra.IsAlgebraic F E] (h : ∃ α : E, F⟮α⟯ = ⊤) : FiniteDimensional F E

Full source

theorem FiniteDimensional.of_exists_primitive_element [Algebra.IsAlgebraic F E]
    (h : ∃ α : E, F⟮α⟯ = ⊤) : FiniteDimensional F E := by
  obtain ⟨α, hprim⟩ := h
  have hfin := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) α)
  rw [hprim] at hfin
  exact topEquiv.toLinearEquiv.finiteDimensional

Finite-dimensionality of field extensions with primitive elements

Informal description

Let $E/F$ be an algebraic field extension. If there exists an element $\alpha \in E$ such that the smallest intermediate field containing $F$ and $\alpha$ is equal to $E$ (i.e., $F(\alpha) = E$), then $E$ is a finite-dimensional vector space over $F$.

Field.finite_intermediateField_of_exists_primitive_element theorem

[Algebra.IsAlgebraic F E] (h : ∃ α : E, F⟮α⟯ = ⊤) : Finite (IntermediateField F E)

Full source

theorem finite_intermediateField_of_exists_primitive_element [Algebra.IsAlgebraic F E]
    (h : ∃ α : E, F⟮α⟯ = ⊤) : Finite (IntermediateField F E) := by
  haveI := FiniteDimensional.of_exists_primitive_element F E h
  obtain ⟨α, hprim⟩ := h
  -- Let `f` be the minimal polynomial of `α ∈ E` over `F`
  let f : F[X] := minpoly F α
  let G := { g : E[X] // g.Monic ∧ g ∣ f.map (algebraMap F E) }
  -- Then `f` has only finitely many monic factors
  have hfin : Finite G := @Finite.of_fintype _ <| fintypeSubtypeMonicDvd
    (f.map (algebraMap F E)) <| map_ne_zero (minpoly.ne_zero_of_finite F α)
  -- If `K` is an intermediate field of `E/F`, let `g` be the minimal polynomial of `α` over `K`
  -- which is a monic factor of `f`
  let g : IntermediateField F E → G := fun K ↦
    ⟨(minpoly K α).map (algebraMap K E), (minpoly.monic <| .of_finite K α).map _, by
      convert Polynomial.map_dvd (algebraMap K E) (minpoly.dvd_map_of_isScalarTower F K α)
      rw [Polynomial.map_map]; rfl⟩
  -- The map `K ↦ g` is injective
  have hinj : Function.Injective g := fun K K' heq ↦ by
    rw [Subtype.mk.injEq] at heq
    apply_fun fun f : E[X] ↦ adjoin F (f.coeffs : Set E) at heq
    simpa only [adjoin_minpoly_coeff_of_exists_primitive_element F hprim] using heq
  -- Therefore there are only finitely many intermediate fields
  exact Finite.of_injective g hinj

Finiteness of Intermediate Fields in Primitive Extensions

Informal description

Let $E/F$ be an algebraic field extension. If there exists an element $\alpha \in E$ such that $E = F(\alpha)$, then the set of intermediate fields between $F$ and $E$ is finite.

Field.exists_primitive_element_iff_finite_intermediateField theorem

: (Algebra.IsAlgebraic F E ∧ ∃ α : E, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E)

Full source

/-- **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`. -/
@[stacks 030N "Equivalence of (1) & (2)"]
theorem exists_primitive_element_iff_finite_intermediateField :
    (Algebra.IsAlgebraic F E ∧ ∃ α : E, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E) :=
  ⟨fun ⟨_, h⟩ ↦ finite_intermediateField_of_exists_primitive_element F E h,
    fun _ ↦ ⟨isAlgebraic_of_finite_intermediateField F E,
      exists_primitive_element_of_finite_intermediateField F E _⟩⟩

Primitive Element Theorem: Characterization via Finiteness of Intermediate Fields

Informal description

Let $E/F$ be an algebraic field extension. Then $E$ has a primitive element (i.e., there exists $\alpha \in E$ such that $E = F(\alpha)$) if and only if there are only finitely many intermediate fields between $F$ and $E$.

AlgHom.card_of_splits theorem

 (L : Type*) [Field L] [Algebra F L] (hL : ∀ x : E, (minpoly F x).Splits (algebraMap F L)) :
  Fintype.card (E →ₐ[F] L) = finrank F E

Full source

@[simp]
theorem AlgHom.card_of_splits (L : Type*) [Field L] [Algebra F L]
    (hL : ∀ x : E, (minpoly F x).Splits (algebraMap F L)) :
    Fintype.card (E →ₐ[F] L) = finrank F E := by
  convert (AlgHom.card_of_powerBasis (L := L) (Field.powerBasisOfFiniteOfSeparable F E)
    (Algebra.IsSeparable.isSeparable _ _) <| hL _).trans
      (PowerBasis.finrank _).symm

Cardinality of Algebra Homomorphisms Equals Extension Degree for Splitting Extensions

Informal description

Let $E/F$ be a finite field extension and $L/F$ another field extension such that for every $x \in E$, the minimal polynomial of $x$ over $F$ splits completely in $L$. Then the number of $F$-algebra homomorphisms from $E$ to $L$ is equal to the degree of the extension $[E:F]$, i.e., \[ |\mathrm{Hom}_F(E, L)| = \dim_F E. \]

AlgHom.card theorem

(K : Type*) [Field K] [IsAlgClosed K] [Algebra F K] : Fintype.card (E →ₐ[F] K) = finrank F E

Full source

@[simp]
theorem AlgHom.card (K : Type*) [Field K] [IsAlgClosed K] [Algebra F K] :
    Fintype.card (E →ₐ[F] K) = finrank F E :=
  AlgHom.card_of_splits _ _ _ (fun _ ↦ IsAlgClosed.splits_codomain _)

Cardinality of Algebra Homomorphisms to Algebraically Closed Field Equals Extension Degree

Informal description

Let $E/F$ be a finite field extension and $K/F$ be an extension where $K$ is an algebraically closed field. Then the number of $F$-algebra homomorphisms from $E$ to $K$ is equal to the degree of the extension $[E:F]$, i.e., \[ |\mathrm{Hom}_F(E, K)| = \dim_F E. \]

Field.primitive_element_iff_minpoly_natDegree_eq theorem

(α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E

Full source

theorem primitive_element_iff_minpoly_natDegree_eq (α : E) :
    F⟮α⟯F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E := by
  rw [← adjoin.finrank (IsIntegral.of_finite F α), ← finrank_top F E]
  refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩
  exact congr_arg (fun K : IntermediateField F E => finrank F K) h

Characterization of Primitive Elements via Minimal Polynomial Degree: $F(\alpha) = E \leftrightarrow \deg(\text{minpoly}_F(\alpha)) = [E : F]$

Informal description

Let $E/F$ be a finite field extension. For an element $\alpha \in E$, the field extension $F(\alpha)$ equals the entire extension $E$ if and only if the degree of the minimal polynomial of $\alpha$ over $F$ is equal to the degree $[E : F]$ of the field extension.

Field.primitive_element_iff_minpoly_degree_eq theorem

(α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = finrank F E

Full source

theorem primitive_element_iff_minpoly_degree_eq (α : E) :
    F⟮α⟯F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = finrank F E := by
  rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]
  exact minpoly.ne_zero_of_finite F α

Characterization of Primitive Elements via Minimal Polynomial Degree: $F(\alpha) = E \leftrightarrow \deg(\text{minpoly}_F(\alpha)) = [E : F]$

Informal description

Field.primitive_element_iff_algHom_eq_of_eval' theorem

(α : E) : F⟮α⟯ = ⊤ ↔ Function.Injective fun φ : E →ₐ[F] A ↦ φ α

Full source

theorem primitive_element_iff_algHom_eq_of_eval' (α : E) :
    F⟮α⟯F⟮α⟯ = ⊤ ↔ Function.Injective fun φ : E →ₐ[F] A ↦ φ α := by
  classical
  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
    (Algebra.IsSeparable.isSeparable F α) (hA _), ← toFinset_card,
    ← (Algebra.IsAlgebraic.of_finite F E).range_eval_eq_rootSet_minpoly_of_splits _ hA α,
    ← AlgHom.card_of_splits F E A hA, Fintype.card, toFinset_range, Finset.card_image_iff,
    Finset.coe_univ, ← injective_iff_injOn_univ]

Primitive Element Characterization via Injectivity of Evaluation on Algebra Homomorphisms

Informal description

Let $E/F$ be a finite field extension and $\alpha \in E$. Then $\alpha$ is a primitive element for $E/F$ (i.e., $F(\alpha) = E$) if and only if the evaluation map $\varphi \mapsto \varphi(\alpha)$ is injective on the set of $F$-algebra homomorphisms from $E$ to any $F$-algebra $A$.

Field.primitive_element_iff_algHom_eq_of_eval theorem

(α : E) (φ : E →ₐ[F] A) : F⟮α⟯ = ⊤ ↔ ∀ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ

Full source

theorem primitive_element_iff_algHom_eq_of_eval (α : E)
    (φ : E →ₐ[F] A) : F⟮α⟯F⟮α⟯ = ⊤ ↔ ∀ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ := by
  refine ⟨fun h ψ hψ ↦ (Field.primitive_element_iff_algHom_eq_of_eval' F A hA α).mp h hψ,
    fun h ↦ eq_of_le_of_finrank_eq' le_top ?_⟩
  letI : Algebra F⟮α⟯ A := (φ.comp F⟮α⟯.val).toAlgebra
  haveI := Algebra.isSeparable_tower_top_of_isSeparable F F⟮α⟯ E
  rw [IntermediateField.finrank_top, ← AlgHom.card_of_splits _ _ A, Fintype.card_eq_one_iff]
  · exact ⟨{ __ := φ, commutes' := fun _ ↦ rfl }, fun ψ ↦ AlgHom.restrictScalars_injective F <|
      Eq.symm <| h _ (ψ.commutes <| AdjoinSimple.gen F α).symm⟩
  · exact fun x ↦ (IsIntegral.of_finite F x).minpoly_splits_tower_top (hA x)

Primitive Element Criterion via Unique Extension of Algebra Homomorphisms

Informal description

Let $E/F$ be a finite field extension and $\alpha \in E$. Then $\alpha$ is a primitive element for $E/F$ (i.e., $F(\alpha) = E$) if and only if for any two $F$-algebra homomorphisms $\varphi, \psi: E \to A$, the equality $\varphi(\alpha) = \psi(\alpha)$ implies $\varphi = \psi$.