Module

Core.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Core

9 declarations indexed from sourceView source ↗

Module documentation

Henselian discretely valued fields

The Henselian factorization condition and the residual linear-factor lemmas used in the residual linear-factor criterion.

Imports20

Imported by11

def

HenselFactorizationProperty

L47 ↗

ValuationTheory.DiscreteValuationField.HenselFactorizationProperty

Documentation

The factorization form of Hensel's lemma used in the Henselian factorization condition.

Every primitive polynomial whose reduction is a product of coprime factors has degree-controlled lifts with the prescribed reductions.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

def HenselFactorizationProperty {K : Type u} [Field K]
    (V : ValuationSubring K) : Prop

def

HenselianValuationByFactorization

L63 ↗

ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization

Documentation

The Henselian factorization condition: a valuation is Henselian when its valuation ring satisfies Hensel's lemma in the factorization sense.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

def HenselianValuationByFactorization {K : Type u} [Field K]
    {Γ : Type v} [LinearOrderedCommGroupWithZero Γ]
    (val : _root_.Valuation K Γ) : Prop

theorem

eval_map_quotient_mk_eq_zero_of_eval_mem

L70 ↗

ValuationTheory.DiscreteValuationField.eval_map_quotient_mk_eq_zero_of_eval_mem

Documentation

An approximate root becomes an actual root after reducing coefficients modulo the ideal.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem eval_map_quotient_mk_eq_zero_of_eval_mem
    {S : Type*} [CommRing S] {J : Ideal S} {p : Polynomial S} {a₀ : S}
    (hroot : p.eval a₀ ∈ J) :
    (p.map (Ideal.Quotient.mk J)).eval (Ideal.Quotient.mk J a₀) = 0

theorem

derivative_eval_map_quotient_mk

L81 ↗

ValuationTheory.DiscreteValuationField.derivative_eval_map_quotient_mk

Documentation

Derivatives commute with coefficient reduction and evaluation at the reduced approximate root.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem derivative_eval_map_quotient_mk
    {S : Type*} [CommRing S] (J : Ideal S) (p : Polynomial S) (a₀ : S) :
    (p.map (Ideal.Quotient.mk J)).derivative.eval (Ideal.Quotient.mk J a₀) =
      Ideal.Quotient.mk J (p.derivative.eval a₀)

theorem

derivative_isUnit_map_quotient_mk_of_simpleRoot_mod

L89 ↗

ValuationTheory.DiscreteValuationField.derivative_isUnit_map_quotient_mk_of_simpleRoot_mod

Documentation

The simple-root hypothesis is the derivative-unit condition for the residual polynomial.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem derivative_isUnit_map_quotient_mk_of_simpleRoot_mod
    {S : Type*} [CommRing S] {J : Ideal S} {p : Polynomial S} {a₀ : S}
    (hsimple : IsUnit (Ideal.Quotient.mk J (p.derivative.eval a₀))) :
    IsUnit
      ((p.map (Ideal.Quotient.mk J)).derivative.eval
        (Ideal.Quotient.mk J a₀))

theorem

isCoprime_X_sub_C_divByMonic_of_derivative_isUnit

L100 ↗

ValuationTheory.DiscreteValuationField.isCoprime_X_sub_C_divByMonic_of_derivative_isUnit

Documentation

A derivative unit makes the linear factor coprime to the cofactor obtained by monic division.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem isCoprime_X_sub_C_divByMonic_of_derivative_isUnit
    {S : Type*} [CommRing S] (p : Polynomial S) (a : S)
    (hunit : IsUnit (p.derivative.eval a)) :
    IsCoprime (Polynomial.X - Polynomial.C a)
      (p /ₘ (Polynomial.X - Polynomial.C a))

theorem

residual_X_sub_C_mul_divByMonic_eq_map_of_eval_mem

L110 ↗

ValuationTheory.DiscreteValuationField.residual_X_sub_C_mul_divByMonic_eq_map_of_eval_mem

Documentation

A residual approximate root supplies an actual linear factor after coefficient reduction.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem residual_X_sub_C_mul_divByMonic_eq_map_of_eval_mem
    {S : Type*} [CommRing S] {J : Ideal S} {p : Polynomial S} {a₀ : S}
    (hroot : p.eval a₀ ∈ J) :
    (Polynomial.X - Polynomial.C (Ideal.Quotient.mk J a₀)) *
        ((p.map (Ideal.Quotient.mk J)) /ₘ
          (Polynomial.X - Polynomial.C (Ideal.Quotient.mk J a₀))) =
      p.map (Ideal.Quotient.mk J)

theorem

isCoprime_residual_X_sub_C_divByMonic_of_simpleRoot_mod

L122 ↗

ValuationTheory.DiscreteValuationField.isCoprime_residual_X_sub_C_divByMonic_of_simpleRoot_mod

Documentation

A residual simple root splits the residual polynomial into coprime linear and complementary factors.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem isCoprime_residual_X_sub_C_divByMonic_of_simpleRoot_mod
    {S : Type*} [CommRing S] {J : Ideal S} {p : Polynomial S} {a₀ : S}
    (hsimple : IsUnit (Ideal.Quotient.mk J (p.derivative.eval a₀))) :
    IsCoprime
      (Polynomial.X - Polynomial.C (Ideal.Quotient.mk J a₀))
      ((p.map (Ideal.Quotient.mk J)) /ₘ
        (Polynomial.X - Polynomial.C (Ideal.Quotient.mk J a₀)))

theorem

henselianRing_map_algebraMap_of_moduleFinite_of_base_isPrecomplete

L136 ↗

ValuationTheory.DiscreteValuationField.henselianRing_map_algebraMap_of_moduleFinite_of_base_isPrecomplete

Documentation

Finite algebras over a Noetherian Henselian, precomplete base are Henselian along the extended ideal.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
namespace DiscreteValuationField
universe u v

Lean source · statement

theorem henselianRing_map_algebraMap_of_moduleFinite_of_base_isPrecomplete
    {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S]
    {I : Ideal R} [IsNoetherianRing R] [Module.Finite R S]
    [HenselianRing R I] [IsPrecomplete I R] :
    HenselianRing S (I.map (algebraMap R S))

Module documentation

Henselian discretely valued fields

Declarations