Krasner's lemma

Stream: maths

[Jiang Jiedong]

Hi everyone,

I want to add Krasner's lemma into Mathlib. I plan to define a typeclass called "IsKrasner K L" for field extensions such that Krasner's lemma holds.

import Mathlib.FieldTheory.Minpoly.Basic
import Mathlib.RingTheory.Valuation.RankOne
import Mathlib.Topology.Algebra.NormedValued

variable {R : Type*} {A : Type*} [CommRing R] [Ring A] [Algebra R A]

variable (K : Type*) {L : Type*} {Γ : outParam Type*}
    [LinearOrderedCommGroupWithZero Γ] [Field K] [Field L]
    [Algebra K L] [vL : Valued L Γ]

variable (R) in
def IsConjRoot (x x' : A) : Prop := (minpoly R x) = (minpoly R x')

variable (L) in
class IsKrasner : Prop where
  krasner' : ∀ {x y : L}, (minpoly K x).Separable → IsIntegral K y →
    (∀ x' : L, IsConjRoot K x x' →  x ≠ x' → vL.v (x - y) < vL.v (x - x')) →
      x ∈ K⟮y⟯

variable [IsKrasner K L]

theorem IsKrasner.krasner {x y : L} (hx : (minpoly K x).Separable) (hy : IsIntegral K y)
    (h : (∀ x' : L, IsConjRoot K x x' → x ≠ x' → vL.v (x - y) < vL.v (x - x'))) : x ∈ K⟮y⟯ :=
  IsKrasner.krasner' hx hy h

theorem IsKrasner.of_complete [u : UniformSpace K] [c : CompleteSpace K]
    [vL.v.RankOne] (h : Embedding (algebraMap K L)) : IsKrasner K L := sorry

It is also possible to define the property IsKrasner for a single field K, meaning for all extensions L of K equipped with a valuation that is compatible with the topology on K, the above property holds. Which one is better? Or are there other design choices?

For the theorem IsKrasner.of_complete, I think after IsValExtension is merged into mathlib, I can state another version that is easier to use, using [vK : Valued K] and [IsValExtension vK.v vL.v].

Thank you for any suggestions and comments!

[Kevin Buzzard]

You could have IsKrasnerExtension for the predicate on extensions, although I think I would have been tempted to demand a separability hypothesis for the extension itself; right now i think that an arbitrary inseparable extension is Krasner according to your definition and this is arguably confusing/misleading

[Jiang Jiedong]

Kevin Buzzard said:

although I think I would have been tempted to demand a separability hypothesis for the extension itself;

In the statement of Krasner's lemma, one only needs $x$ to be a separable element, $y$ can be any algebraic element. We would get a slightly weaker version of Krasner's lemma (by imposing a separability condition on $y$) if we require a separability of $L/K$. But it will be still enough to prove that $\widehat{\mathbb{Q}_p^{sep}} = \widehat{\mathbb{Q}_p^{alg}}$ is algebraically closed if we prove that a polynomial sufficiently close to a separable polynomial is still separable.

[Jiang Jiedong]

Maybe it is better to define the predicateIsKrasner for a single valued field K if one does not impose the separable condition on y.

[Johan Commelin]

Intuitively, I would define the predicate for an extension, instead of for K by quantifying over all extensions.

[Jiang Jiedong]

Currently, I still want to state the strongest version (allowing $y$ to be algebraic instead of separated) of Krasner's lemma, since it will save this lemma

a polynomial sufficiently close to a separable polynomial is still separable

for nothing.

Are there any suggestions for IsKrasnerExtension to be less confusing? :face_with_diagonal_mouth:

[Johan Commelin]

cc @María Inés de Frutos Fernández and @Antoine Chambert-Loir

[Johan Commelin]

and @Filippo A. E. Nuccio