English
If E/F is finite and E = F(α), then for any intermediate field K, the F-adjoin of the coefficients of the minimal polynomial of α (after mapping to E) equals K.
Русский
Если E/F конечно, и E = F(α), то для любого промежуточного поля K конъюнкция F-адъюнкта коэффициентов минимального полинома α (после отображения в E) равна K.
LaTeX
$$$\operatorname{adjoin}_F\bigl((\minpoly K\alpha)^{\text{map}}(\operatorname{algebraMap}_K E)\bigr).\operatorname{coeffs} = K$$$
Lean4
/-- If `E / F` is a finite extension such that `E = F(α)`, then for any intermediate field `K`, the
`F` adjoin the coefficients of `minpoly K α` is equal to `K` itself. -/
theorem adjoin_minpoly_coeff_of_exists_primitive_element [FiniteDimensional F E] (hprim : adjoin F { α } = ⊤)
(K : IntermediateField F E) : adjoin F ((minpoly K α).map (algebraMap K E)).coeffs = K :=
by
set g := (minpoly K α).map (algebraMap K E)
set K' : IntermediateField F E := adjoin F g.coeffs
have hsub : K' ≤ K := by
refine adjoin_le_iff.mpr fun x ↦ ?_
rw [Finset.mem_coe, mem_coeffs_iff]
rintro ⟨n, -, rfl⟩
rw [coeff_map]
apply Subtype.mem
have dvd_g : minpoly K' α ∣ g.toSubring K'.toSubring (subset_adjoin F _) :=
by
apply minpoly.dvd
rw [aeval_def, eval₂_eq_eval_map]
erw [g.map_toSubring K'.toSubring]
rw [eval_map, ← aeval_def]
exact minpoly.aeval K α
have finrank_eq : ∀ K : IntermediateField F E, finrank K E = natDegree (minpoly K α) :=
by
intro K
have := adjoin.finrank (.of_finite K α)
rw [adjoin_eq_top_of_adjoin_eq_top F hprim] at this
simp_all
refine eq_of_le_of_finrank_le' hsub ?_
simp_rw [finrank_eq]
convert
natDegree_le_of_dvd dvd_g ((g.monic_toSubring _ _).mpr <| (minpoly.monic <| .of_finite K α).map _).ne_zero using 1
rw [natDegree_toSubring, natDegree_map]
