Approximating algebraic elements by roots of polynomials over a dense subfield

Let L be an algebraically closed normed field over a normed field K, and let k be a field whose image in K is dense. Every element of L algebraic over K is a limit of elements of L algebraic over k: approximate the minimal polynomial over K by a monic polynomial over k (Polynomial.exists_monic_and_natDegree_eq_and_norm_map_algebraMap_coeff_sub_lt), which splits in L and has a root close to the original element by continuity of roots (Polynomial.exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt).

For k = ℚ and K = ℚ_p this shows that the algebraic numbers are dense in ℂ_p, so ℂ_p is separable.

Main results

• IsAlgebraic.mem_closure_setOf_isAlgebraic: an element of L algebraic over K lies in the closure of the elements algebraic over k.

References

• A. M. Robert, A Course in p-adic Analysis, Graduate Texts in Mathematics 198, Springer, 2000, Chapter 3, for the density of the algebraic numbers in ℂ_p and the separability of ℂ_p.

theorem IsAlgebraic.mem_closure_setOf_isAlgebraic {k : Type u_1} {K : Type u_2} {L : Type u_3} [Field k] [NormedField K] [NormedField L] [NormedAlgebra K L] [Algebra k K] [Algebra k L] [IsScalarTower k K L] [IsAlgClosed L] {x : L} (hx : IsAlgebraic K x) (hk : DenseRange ⇑(algebraMap k K)) : x ∈ closure {y : L | IsAlgebraic k y}

Elements algebraic over K are limits of elements algebraic over a dense subfield k, in an algebraically closed normed field L over K.