[Merged by Bors] - feat: Add some equivalent characterisations of primitive elements in finite extensions of fields

Mathlib/Data/Polynomial/Splits.lean

@@ -438,6 +438,13 @@ theorem splits_id_of_splits {f : K[X]} (h : Splits i f)
     (roots_mem_range : ∀ a ∈ (f.map i).roots, a ∈ i.range) : Splits (RingHom.id K) f :=
   splits_of_comp (RingHom.id K) i h roots_mem_range
 
+theorem splits_of_algHom {R L' : Type*} [CommRing R] [Field L'] [Algebra R L] [Algebra R L']
+    {f : R[X]} (h : Polynomial.Splits (algebraMap R L) f) (e : L →ₐ[R] L') :
+    Polynomial.Splits (algebraMap R L') f := by
+  rw [← splits_id_iff_splits, ← AlgHom.comp_algebraMap_of_tower R e, ← map_map,
+    splits_id_iff_splits]
+  exact splits_of_splits_id e.toRingHom <| (splits_id_iff_splits _).mpr h
+
 theorem splits_comp_of_splits (j : L →+* F) {f : K[X]} (h : Splits i f) : Splits (j.comp i) f := by
   -- Porting note: was
   -- change i with (RingHom.id _).comp i at h

Mathlib/FieldTheory/Adjoin.lean

@@ -1296,6 +1296,25 @@ end AlgHomMkAdjoinSplits
 
 end IntermediateField
 
+section Algebra.IsAlgebraic
+
+/-- Let `K/F` be an algebraic extension of fields and `A` a field in which all the minimal
+polynomial over `F` of elements of `K` splits. Then, for `x ∈ K`, the images of `x` by the
+`F`-algebra morphisms from `K` to `A` are exactly the roots in `A` of the minimal polynomial
+of `x` over `F`. -/
+theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits {F K : Type*} (A : Type*)
+    [Field F] [Field K] [Field A] [Algebra F A] [Algebra F K]
+    (hA : ∀ x : K, (minpoly F x).Splits (algebraMap F A))
+    (hK : Algebra.IsAlgebraic F K) (x : K) :
+    (Set.range fun (ψ : K →ₐ[F] A) => ψ x) = (minpoly F x).rootSet A := by
+  ext a
+  rw [mem_rootSet_of_ne (minpoly.ne_zero (hK.isIntegral x))]
+  refine ⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
+    (fun x ↦ ⟨hK.isIntegral x, hA x⟩) ha⟩
+  rw [← hψ, Polynomial.aeval_algHom_apply ψ x, minpoly.aeval, map_zero]
+
+end Algebra.IsAlgebraic
+
 section PowerBasis
 
 variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -397,15 +397,56 @@ end EquivOfEquiv
 
 end IsAlgClosure
 
+section Algebra.IsAlgebraic
+
+variable {F K : Type*} (A : Type*) [Field F] [Field K] [Field A] [IsAlgClosed A] [Algebra F K]
+  (hK : Algebra.IsAlgebraic F K) [Algebra F A]
+
 /-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K/F` an algebraic extension
   of fields. Then the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
   the roots in `A` of the minimal polynomial of `x` over `F`. -/
-theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly {F K} (A) [Field F] [Field K] [Field A]
-    [IsAlgClosed A] [Algebra F K] (hK : Algebra.IsAlgebraic F K) [Algebra F A] (x : K) :
-    (Set.range fun ψ : K →ₐ[F] A ↦ ψ x) = (minpoly F x).rootSet A := by
-  ext a
-  rw [mem_rootSet_of_ne (minpoly.ne_zero (hK.isIntegral x))]
-  refine ⟨fun ⟨ψ, hψ⟩ ↦ ?_, fun ha ↦ IntermediateField.exists_algHom_of_splits_of_aeval
-    (fun x ↦ ⟨hK.isIntegral x, IsAlgClosed.splits_codomain _⟩) ha⟩
-  rw [← hψ, aeval_algHom_apply ψ x, minpoly.aeval, map_zero]
+theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly (x : K) :
+    (Set.range fun ψ : K →ₐ[F] A ↦ ψ x) = (minpoly F x).rootSet A :=
+  range_eval_eq_rootSet_minpoly_of_splits A (fun _ ↦ IsAlgClosed.splits_codomain _) hK x
 #align algebra.is_algebraic.range_eval_eq_root_set_minpoly Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly
+
+/-- All `F`-`AlgHom`s from `K` to an algebraic closed field `A` factor through any subextension of
+`A/F` in which the minimal polynomial of elements of `K` splits. -/
+def IntermediateField.algHomEquivAlgHomOfIsAlgClosed (L : IntermediateField F A)
+    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
+    (K →ₐ[F] L) ≃ (K →ₐ[F] A) where
+  toFun := L.val.comp
+  invFun := by
+    refine fun f => f.codRestrict _ (fun x => ?_)
+    suffices f x ∈ L.val '' rootSet (minpoly F x) L by
+      obtain ⟨z, -, hz⟩ := this
+      rw [← hz]
+      exact SetLike.coe_mem z
+    rw [image_rootSet (hL x), ← Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly _ hK]
+    exact Set.mem_range_self f
+  left_inv _ := rfl
+  right_inv _ := by rfl
+
+theorem IntermediateField.algHomEquivAlgHomOfIsAlgClosed_apply_apply (L : IntermediateField F A)
+    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
+    algHomEquivAlgHomOfIsAlgClosed A hK L hL f x = algebraMap L A (f x) := rfl
+
+/-- All `F`-`AlgHom`s from `K` to an algebraic closed field `A` factor through any subfield of `A`
+in which the minimal polynomial of elements of `K` splits. -/
+noncomputable def Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed (L : Type*) [Field L]
+    [Algebra F L] [Algebra L A] [IsScalarTower F L A]
+    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) :
+    (K →ₐ[F] L) ≃ (K →ₐ[F] A) := by
+  refine (AlgEquiv.refl.arrowCongr
+    (AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L A))).trans ?_
+  refine IntermediateField.algHomEquivAlgHomOfIsAlgClosed
+    A hK (IsScalarTower.toAlgHom F L A).fieldRange ?_
+  exact fun x => splits_of_algHom (hL x) (AlgHom.rangeRestrict _)
+
+theorem Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed_apply_apply (L : Type*) [Field L]
+    [Algebra F L] [Algebra L A] [IsScalarTower F L A]
+    (hL : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (f : K →ₐ[F] L) (x : K) :
+    Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed A hK L hL f x =
+    algebraMap L A (f x) := rfl
+
+end Algebra.IsAlgebraic

Mathlib/FieldTheory/PrimitiveElement.lean

@@ -3,9 +3,8 @@
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
-import Mathlib.FieldTheory.SplittingField.Construction
-import Mathlib.FieldTheory.IsAlgClosed.Basic
-import Mathlib.FieldTheory.Separable
+import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
+import Mathlib.FieldTheory.NormalClosure
 import Mathlib.RingTheory.IntegralDomain
 
 #align_import field_theory.primitive_element from "leanprover-community/mathlib"@"df76f43357840485b9d04ed5dee5ab115d420e87"
@@ -348,10 +347,87 @@
 
 end Field
 
+variable (F E : Type*) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [IsSeparable F E]
+
 @[simp]
-theorem AlgHom.card (F E K : Type*) [Field F] [Field E] [Field K] [IsAlgClosed K] [Algebra F E]
-    [FiniteDimensional F E] [IsSeparable F E] [Algebra F K] :
+theorem AlgHom.card (K : Type*) [Field K] [IsAlgClosed K] [Algebra F K] :
     Fintype.card (E →ₐ[F] K) = finrank F E := by
   convert (AlgHom.card_of_powerBasis (L := K) (Field.powerBasisOfFiniteOfSeparable F E)
     (IsSeparable.separable _ _) (IsAlgClosed.splits_codomain _)).trans (PowerBasis.finrank _).symm
 #align alg_hom.card AlgHom.card
+
+@[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
+  rw [← Fintype.ofEquiv_card <| Algebra.IsAlgebraic.algHomEquivAlgHomOfIsAlgClosed
+    (AlgebraicClosure L) (Algebra.IsAlgebraic.of_finite F E) _ hL]
+  convert AlgHom.card F E (AlgebraicClosure L)
+
+section iff
+
+namespace Field
+
+open FiniteDimensional IntermediateField Polynomial Algebra Set
+
+variable (F : Type*) {E : Type*} [Field F] [Field E] [Algebra F E] [FiniteDimensional F E]
+
+theorem primitive_element_iff_minpoly_natDegree_eq (α : E) :
+    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
+
+theorem primitive_element_iff_minpoly_degree_eq (α : E) :
+    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 α
+
+variable [IsSeparable F E] (A : Type*) [Field A] [Algebra F A]
+  (hA : ∀ x : E, (minpoly F x).Splits (algebraMap F A))
+
+theorem primitive_element_iff_algHom_eq_of_eval' (α : E) :
+    F⟮α⟯ = ⊤ ↔ Function.Injective fun φ : E →ₐ[F] A ↦ φ α := by
+-- ∀ φ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ := by
+  classical
+  simp_rw [primitive_element_iff_minpoly_natDegree_eq, ← card_rootSet_eq_natDegree (K := A)
+    (IsSeparable.separable 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]
+
+theorem primitive_element_iff_algHom_eq_of_eval (α : E) 
+    (φ : E →ₐ[F] A) : F⟮α⟯ = ⊤ ↔ ∀ ψ : E →ₐ[F] A, φ α = ψ α → φ = ψ := by
+  rw [Field.primitive_element_iff_algHom_eq_of_eval' F A hA]
+  refine ⟨fun h _ eq => h eq, fun h φ₀ ψ₀ h' => ?_⟩
+  let K := normalClosure F E A
+  have : IsNormalClosure F E K := by
+    refine Algebra.IsAlgebraic.isNormalClosure_normalClosure ?_ hA
+    exact Algebra.IsAlgebraic.of_finite F E
+  have hK_mem : ∀ (ψ : E →ₐ[F] A) (x : E), ψ x ∈ K :=
+    fun ψ x => AlgHom.fieldRange_le_normalClosure ψ ⟨x, rfl⟩
+  let res : (E →ₐ[F] A) → (E →ₐ[F] K) := fun ψ => AlgHom.codRestrict ψ K.toSubalgebra (hK_mem ψ)
+  rsuffices ⟨σ, hσ⟩ : ∃ σ : K →ₐ[F] A, σ (⟨φ₀ α, hK_mem _ _⟩) = φ α
+  · suffices res φ₀ = res ψ₀ by
+      ext x
+      exact Subtype.mk_eq_mk.mp (AlgHom.congr_fun this x)
+    have eq₁ : φ = AlgHom.comp σ (res φ₀) := h (AlgHom.comp σ (res φ₀)) hσ.symm
+    have eq₂ : φ = AlgHom.comp σ (res ψ₀) := by
+      refine h (AlgHom.comp σ (res ψ₀)) ?_
+      simp_rw [← hσ, h']
+      rfl
+    ext1 x
+    exact (RingHom.injective σ.toRingHom) <| AlgHom.congr_fun (eq₁.symm.trans eq₂) x
+  refine IntermediateField.exists_algHom_of_splits_of_aeval ?_ ?_
+  · refine fun x => ⟨IsAlgebraic.isIntegral (IsAlgebraic.of_finite F x), ?_⟩
+    refine Polynomial.splits_of_algHom ?_ K.toSubalgebra.val
+    exact Normal.splits (IsNormalClosure.normal (K := E)) x
+  · rw [aeval_algHom_apply, _root_.map_eq_zero]
+    convert minpoly.aeval F α
+    letI : Algebra E K := (res φ₀).toAlgebra
+    refine minpoly.algebraMap_eq ?_ α
+    exact NoZeroSMulDivisors.algebraMap_injective E K
+
+end Field
+
+end iff