Module

SeparableRootApproximation.lean

Nyll.ValuedFieldTheory.Valuation.Completion.SeparableRootApproximation

3 declarations indexed from sourceView source ↗

Module documentation

Approximating separable generators over a dense subfield

Approximate the minimal polynomial by a monic polynomial over the dense subfield. Continuity of roots produces a nearby root in the algebraic closure, and Krasner's lemma places the original generator in its adjoin.

Imports4

Mathlib.Analysis.Normed.Field.Approximation
Mathlib.Analysis.Normed.Field.Krasner
Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure

Imported by2

theorem

exists_pos_le_norm_sub_conjugate

L25 ↗

ValuationTheory.Completion.exists_pos_le_norm_sub_conjugate

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.Completion
open Polynomial
open scoped Topology

Lean source · statement

theorem exists_pos_le_norm_sub_conjugate
    {A Ω : Type*} [Field A] [NormedField Ω] [Algebra A Ω]
    (α : Ω) (hα : IsIntegral A α) :
    ∃ δ : ℝ, 0 < δ ∧ ∀ α' : Ω, IsConjRoot A α α' → α ≠ α' →
      δ ≤ ‖α - α'‖

theorem

exists_monic_root_with_adjoin_containment_of_normed

L45 ↗

ValuationTheory.Completion.exists_monic_root_with_adjoin_containment_of_normed

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.Completion
open Polynomial
open scoped Topology

Lean source · statement

theorem exists_monic_root_with_adjoin_containment_of_normed
    {K A Ω : Type*} [Field K] [NontriviallyNormedField A]
    [CompleteSpace A] [IsUltrametricDist A] [NormedField Ω]
    [Algebra K A] [NormedAlgebra A Ω] [Algebra K Ω] [IsScalarTower K A Ω]
    [IsAlgClosed Ω] [Algebra.IsAlgebraic A Ω]
    (hd : DenseRange (algebraMap K A)) (α : Ω) (hα : IsSeparable A α) :
    ∃ g : K[X], ∃ β : Ω, g.Monic ∧
      g.natDegree = (minpoly A α).natDegree ∧ g.aeval β = 0 ∧
        α ∈ IntermediateField.adjoin A ({β} : Set Ω)

theorem

exists_monic_root_with_adjoin_containment

L92 ↗

ValuationTheory.Completion.exists_monic_root_with_adjoin_containment

Documentation

A separable element over a complete nonarchimedean field is contained in the adjoin of a root of a monic polynomial over any dense subfield, without increasing the degree of its minimal polynomial.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ValuationTheory.Completion
open Polynomial
open scoped Topology

Lean source · statement

theorem exists_monic_root_with_adjoin_containment
    {K A : Type*} [Field K] [NontriviallyNormedField A]
    [CompleteSpace A] [IsUltrametricDist A] [Algebra K A]
    (hd : DenseRange (algebraMap K A)) (α : AlgebraicClosure A)
    (hα : IsSeparable A α) :
    ∃ g : K[X], ∃ β : AlgebraicClosure A, g.Monic ∧
      g.natDegree = (minpoly A α).natDegree ∧ g.aeval β = 0 ∧
        α ∈ IntermediateField.adjoin A ({β} : Set (AlgebraicClosure A))

Module documentation

Approximating separable generators over a dense subfield

Declarations

exists_pos_le_norm_sub_conjugate

exists_monic_root_with_adjoin_containment_of_normed

exists_monic_root_with_adjoin_containment