English
For algebraic subextensions, there is a finite combination of root data generating x within the join of adjoined fields.
Русский
Для алгебраических подпольных расширений существует конечная совокупность данных корней, порождающая x в объединении adjoin.
LaTeX
$$∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, adjoin F ((minpoly F (i.2)).rootSet E)$$
Lean4
theorem exists_finset_of_mem_supr'' {ι : Type*} {f : ι → IntermediateField F E} (h : ∀ i, Algebra.IsAlgebraic F (f i))
{x : E} (hx : x ∈ ⨆ i, f i) : ∃ s : Finset (Σ i, f i), x ∈ ⨆ i ∈ s, adjoin F ((minpoly F (i.2 :)).rootSet E) :=
by
refine exists_finset_of_mem_iSup (SetLike.le_def.mp (iSup_le (fun i x1 hx1 => ?_)) hx)
refine SetLike.le_def.mp (le_iSup_of_le ⟨i, x1, hx1⟩ ?_) (subset_adjoin F (rootSet (minpoly F x1) E) ?_)
· rw [IntermediateField.minpoly_eq, Subtype.coe_mk]
· rw [mem_rootSet_of_ne, minpoly.aeval]
exact minpoly.ne_zero (isIntegral_iff.mp (Algebra.IsIntegral.isIntegral (⟨x1, hx1⟩ : f i)))
