Krasner's Lemma

In this file, we prove Krasner's lemma.

Main definitions

• IsKrasner K L : Given a field extension L / K where L is a normed field, IsKrasner K L is the abstraction of the conclusion of Krasner's lemma. That is, IsKrasner K L means that given two elements x y : L, such that x is separable over K, all conjugate roots of x live in L, y is integral over K, and the distance between x and y is less than the distance between x and any other conjugate root of x, then x is in the field generated by K and y.

Main results

• IsKrasner.of_complete : If K is a complete normed field, such that the norm of L extends the norm on K, then IsKrasner K L holds for every algebraic extension L over K. This implies the classical Krasner's lemma by taking L as the separable closure of K.

Reference

For the classical statement of Krasner's lemma, please see the wikipedia page.

Tags

Krasner's lemma, normed field

class IsKrasner (K : Type u_1) (L : Type u_2) [NormedField L] [Field K] [Algebra K L] : Prop

Given a field extension L / K where L is a normed field, IsKrasner K L is the abstraction of the conclusion of Krasner's lemma. That is, IsKrasner K L means that given two elements x y : L, such that x is separable over K, all conjugate roots of x live in L, y is integral over K, and the distance between x and y is less than the distance between x and any other conjugate root of x, then x is in the field generated by K and y.

• krasner' {x y : L} : IsSeparable K x → (Polynomial.map (algebraMap K L) (minpoly K x)).Splits → IsIntegral K y → (∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖) → x ∈ K⟮y⟯

theorem IsKrasner.krasner {K : Type u_1} {L : Type u_2} [NormedField L] [Field K] [Algebra K L] [IsKrasner K L] {x y : L} (hx : (minpoly K x).Separable) (sp : (Polynomial.map (algebraMap K L) (minpoly K x)).Splits) (hy : IsIntegral K y) (h : ∀ (x' : L), IsConjRoot K x x' → x ≠ x' → ‖x - y‖ < ‖x - x'‖) : x ∈ K⟮y⟯

theorem IsKrasner.of_completeSpace_of_normal (K : Type u_1) (L : Type u_2) [NormedField L] [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [NormedAlgebra K L] [Algebra.IsAlgebraic K L] [Normal K L] : IsKrasner K L

Krasner's lemma assuming Normal K L.

instance IsKrasner.of_completeSpace (K : Type u_1) (L : Type u_2) [NormedField L] [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K] [NormedAlgebra K L] [Algebra.IsAlgebraic K L] : IsKrasner K L

If K is a complete nontrivially normed field and L is an algebraic extension of K such that the norm of L extends the norm on K, then IsKrasner K L holds. This corresponds to the classical Krasner's lemma.