Krasner's lemma

DefinitionClosest conjugate#✓fully proved

Let \(K\) be a normed field with algebraic closure \(\overline{K}\), and let \(\lVert \cdot \rVert\) be the spectral norm on \(\overline{K}\) over \(K\). For \(\alpha, \beta \in \overline{K}\), \(\alpha\) is the closest conjugate to \(\beta\) if \(\lVert \beta - \alpha \rVert < \lVert \beta - \sigma(\alpha) \rVert\) for every \(K\)-algebra automorphism \(\sigma\) of \(\overline{K}\) with \(\sigma(\alpha) \ne \alpha\).

def IsClosestConjugate (K : Type*) [NormedField K]
    (α β : AlgebraicClosure K) : Prop :=
  ∀ σ : AlgebraicClosure K ≃ₐ[K] AlgebraicClosure K,
    σ α ≠ α →
    spectralNorm K (AlgebraicClosure K) (β - α) <
      spectralNorm K (AlgebraicClosure K) (β - σ α)

Used by 4

Used byKrasner's lemma for closest conjugates · Closest conjugate roots of nearby monic polynomials · Small monic perturbations stay irreducible and separable · Closest conjugates satisfy Krasner's hypothesis

TheoremClosest conjugates satisfy Krasner's hypothesis#✓fully proved

Let \(K\) be a complete nontrivially normed field whose norm is ultrametric, with algebraic closure \(\overline{K}\), let \(\lVert \cdot \rVert\) be the spectral norm on \(\overline{K}\) over \(K\), and let \(\alpha, \beta, \alpha' \in \overline{K}\). If \(\alpha\) is the closest conjugate to \(\beta\) and \(\alpha' \ne \alpha\) is a conjugate of \(\alpha\) over \(K\), then \(\lVert \alpha - \beta \rVert < \lVert \alpha - \alpha' \rVert\).

theorem IsClosestConjugate.lt_spectralNorm_sub_of_isConjRoot
    {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    {α β α' : AlgebraicClosure K} (h : IsClosestConjugate K α β)
    (hconj : IsConjRoot K α α') (hne : α ≠ α') :
    spectralNorm K (AlgebraicClosure K) (α - β) <
      spectralNorm K (AlgebraicClosure K) (α - α')

Uses 1 · Used by 1

Statement usesClosest conjugate

Used byKrasner's lemma for closest conjugates

TheoremKrasner's lemma for closest conjugates#✓fully proved

Let \(K\) be a complete nontrivially normed field whose norm is ultrametric, with algebraic closure \(\overline{K}\), and let \(\alpha, \beta \in \overline{K}\). If \(\alpha\) is the closest conjugate to \(\beta\) and \(\alpha\) is separable over \(K\), then \(K(\alpha) \subseteq K(\beta)\).

theorem IsClosestConjugate.adjoin_le
    {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    {α β : AlgebraicClosure K} (h : IsClosestConjugate K α β)
    (hsep : IsSeparable K α) :
    IntermediateField.adjoin K {α} ≤ IntermediateField.adjoin K {β}

Uses 2 · Used by 1

Statement usesClosest conjugate

Proof usesClosest conjugates satisfy Krasner's hypothesis

Used byClosest conjugate roots of nearby monic polynomials

TheoremClosest conjugate roots of nearby monic polynomials#✓fully proved

Let \(K\) be a complete nontrivially normed field whose norm is ultrametric, with algebraic closure \(\overline{K}\), and let \(f \in K[X]\) be monic, irreducible and separable. Then there is a real \(\delta > 0\) such that for every monic \(g \in K[X]\) with \(\lVert f - g \rVert_1 < \delta\), where \(\lVert \cdot \rVert_1\) is the \(\ell^1\) norm (the sum of the norms of the coefficients), and every root \(\beta \in \overline{K}\) of \(g\), there is a root \(\alpha \in \overline{K}\) of \(f\) such that \(\alpha\) is the closest conjugate to \(\beta\) and \(K(\alpha) = K(\beta)\).

theorem exists_isClosestConjugate_root_of_l1Norm_sub_lt
    (K : Type*) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    (f : K[X]) (hf : f.Monic) (hirr : Irreducible f) (hsep : f.Separable) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ g : K[X], g.Monic →
      l1Norm (NormedField.toAbsoluteValue K) (f - g) < δ →
      ∀ β : AlgebraicClosure K, aeval β g = 0 →
        ∃ α : AlgebraicClosure K, aeval α f = 0 ∧
          AlgebraicClosure.IsClosestConjugate K α β ∧
          IntermediateField.adjoin K {α} = IntermediateField.adjoin K {β}

Uses 8 · Used by 1

Statement usesClosest conjugate · L1 norm of a polynomial

Proof usesKrasner's lemma for closest conjugates · Root bound by the L1 norm · L1 norm as a sum over the support · Nonnegativity of the L1 norm · Monic polynomials close in L1 norm have the same degree · Monic polynomials have L1 norm at least one

Used bySmall monic perturbations stay irreducible and separable

TheoremSmall monic perturbations stay irreducible and separable#✓fully proved

Let \(K\) be a complete nontrivially normed field whose norm is ultrametric, and let \(f \in K[X]\) be monic, irreducible and separable. Then there is a real \(\delta > 0\) such that every monic \(g \in K[X]\) with \(\lVert f - g \rVert_1 < \delta\), where \(\lVert \cdot \rVert_1\) is the \(\ell^1\) norm (the sum of the norms of the coefficients), is irreducible and separable.

theorem exists_pos_irreducible_and_separable_of_l1Norm_sub_lt
    (K : Type*) [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
    (f : K[X]) (hf : f.Monic) (hirr : Irreducible f) (hsep : f.Separable) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ g : K[X], g.Monic →
      l1Norm (NormedField.toAbsoluteValue K) (f - g) < δ →
      Irreducible g ∧ g.Separable

Uses 4 · Used by 1

Statement usesL1 norm of a polynomial

Proof usesClosest conjugate · Closest conjugate roots of nearby monic polynomials · Monic polynomials close in L1 norm have the same degree

Used byApproximation by irreducible separable polynomials over a dense field

TheoremApproximation by irreducible separable polynomials over a dense field#✓fully proved

Let \(K\) be a field and \(L\) a complete nontrivially normed field whose norm is ultrametric, with a \(K\)-algebra structure such that the image of \(K\) in \(L\) is dense. Let \(f \in L[X]\) be monic, irreducible and separable, and let \(\varepsilon > 0\) be real. Then there is a monic \(g \in K[X]\) with \(\deg g = \deg f\) such that, writing \(\bar g \in L[X]\) for the image of \(g\), \(\lVert f - \bar g \rVert_1 < \varepsilon\), where \(\lVert \cdot \rVert_1\) is the \(\ell^1\) norm (the sum of the norms of the coefficients), and \(\bar g\) is irreducible and separable in \(L[X]\).

theorem exists_monic_and_natDegree_eq_and_l1Norm_sub_lt_and_map_irreducible_and_separable
    {K L : Type*} [Field K] [NontriviallyNormedField L]
    [IsUltrametricDist L] [CompleteSpace L] [Algebra K L]
    (hdense : DenseRange (algebraMap K L))
    (f : L[X]) (hf : f.Monic) (hirr : Irreducible f) (hsep : f.Separable)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ g : K[X], g.Monic ∧ g.natDegree = f.natDegree ∧
      l1Norm (NormedField.toAbsoluteValue L)
        (f - g.map (algebraMap K L)) < ε ∧
      Irreducible (g.map (algebraMap K L)) ∧
      (g.map (algebraMap K L)).Separable

Uses 3

Statement usesL1 norm of a polynomial

Proof usesSmall monic perturbations stay irreducible and separable · L1 norm as a sum over the support

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.