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 α over the corresponding subfield equals K.
Русский
Если E/F конечно и E = F(α), тогда для любого промежуточного поля K над F адъюнктируется множество коэффициентов минимального полинома α над соответствующим подполем, давая K.
LaTeX
$$$\operatorname{adjoin}_F\bigl((\minpoly K\alpha).map(\operatorname{algebraMap}_K E).\operatorname{coeffs}\bigr) = K$$
Lean4
/-- If `E / F` is an infinite algebraic extension, then there exists an intermediate field
`L / F` with arbitrarily large finite extension degree. -/
theorem exists_lt_finrank_of_infinite_dimensional [Algebra.IsAlgebraic F E] (hnfd : ¬FiniteDimensional F E) (n : ℕ) :
∃ L : IntermediateField F E, FiniteDimensional F L ∧ n < finrank F L := by
induction n with
| zero => exact ⟨⊥, Subalgebra.finite_bot, finrank_pos⟩
| succ n ih =>
obtain ⟨L, fin, hn⟩ := ih
obtain ⟨x, hx⟩ : ∃ x : E, x ∉ L := by
contrapose! hnfd
rw [show L = ⊤ from eq_top_iff.2 fun x _ ↦ hnfd x] at fin
exact topEquiv.toLinearEquiv.finiteDimensional
let L' := L ⊔ F⟮x⟯
haveI := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral (R := F) x)
refine ⟨L', inferInstance, by_contra fun h ↦ ?_⟩
have h1 : L = L' := eq_of_le_of_finrank_le le_sup_left ((not_lt.1 h).trans hn)
have h2 : F⟮x⟯ ≤ L' := le_sup_right
exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
