NYLL
Module

HenselLemma.lean

Nyll.ValuedFieldTheory.Valuation.HenselLemma
11 declarations indexed from sourceView source ↗

Module documentation

Factorization-shaped Hensel consequences

Mathlib exposes the simple-root form of Hensel's lemma. The statements below turn it into a linear-factor lifting API for a simple residual linear factor.

Imports3
Imported by6

Declarations

theorem

divByMonic_X_sub_C_eval_eq_derivative_eval

L29 ↗
ValuationTheory.DiscreteValuationField.divByMonic_X_sub_C_eval_eq_derivative_eval
Documentation

The cofactor obtained by dividing by X - C a evaluates to the derivative value at a. This is the polynomial identity behind the simple-root decomposition over the residual algebra.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
Lean source · statement
theorem divByMonic_X_sub_C_eval_eq_derivative_eval
    {S : Type*} [CommRing S] (p : Polynomial S) (a : S) :
    (p /ₘ (Polynomial.X - Polynomial.C a)).eval a =
      p.derivative.eval a
theorem

isCoprime_X_sub_C_of_isUnit_eval

L49 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.isCoprime_X_sub_C_of_isUnit_eval
Documentation

A linear factor is coprime to any polynomial whose value at the root is a unit. This is the elementary Bezout step used in factorization-form Hensel arguments.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
Lean source · statement
theorem isCoprime_X_sub_C_of_isUnit_eval
    {R : Type u} [CommRing R] (q : Polynomial R) (a : R)
    (hq : IsUnit (q.eval a)) :
    IsCoprime (Polynomial.X - Polynomial.C a) q
theorem

linearFactor_isCoprime_quotient_of_derivative_isUnit

L79 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.linearFactor_isCoprime_quotient_of_derivative_isUnit
Documentation

If f = (X - a) * q and the derivative of f at a is a unit, then the linear factor and the quotient are coprime.

This is the coprime-factor algebra bridge needed after a Hensel lift proves that the lifted root remains simple.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
Lean source · statement
theorem linearFactor_isCoprime_quotient_of_derivative_isUnit
    {R : Type u} [CommRing R] (f q : Polynomial R) (a : R)
    (hfactor : f = (Polynomial.X - Polynomial.C a) * q)
    (hderiv : IsUnit (f.derivative.eval a)) :
    IsCoprime (Polynomial.X - Polynomial.C a) q
theorem

eq_of_isRoot_of_isRoot_of_residue_eq_of_derivative_isUnit

L98 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.eq_of_isRoot_of_isRoot_of_residue_eq_of_derivative_isUnit
Documentation

A simple root in a fixed residue class is unique.

This is the uniqueness half used by residue-lift constructions: if two actual roots have the same residue and one of them has unit derivative, then they are equal.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem eq_of_isRoot_of_isRoot_of_residue_eq_of_derivative_isUnit
    {f : Polynomial F.valuationSubring} {a b : F.valuationSubring}
    (ha : f.IsRoot a) (hb : f.IsRoot b)
    (hres : F.residueMap b = F.residueMap a)
    (hderiv : IsUnit (f.derivative.eval a)) :
    b = a
theorem

exists_linear_factor_lift

L144 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_linear_factor_lift
Documentation

Hensel's lemma gives a linear factor lifting from a simple approximate root.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_linear_factor_lift
    (f : Polynomial F.valuationSubring) (hf : f.Monic) (a0 : F.valuationSubring)
    (hroot : f.eval a0 ∈ F.maximalIdeal)
    (hsimple : IsUnit (Ideal.Quotient.mk F.maximalIdeal (f.derivative.eval a0))) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ a - a0 ∈ F.maximalIdeal ∧
        f = (Polynomial.X - Polynomial.C a) * q
theorem

exists_monic_linear_factor_lift

L157 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_linear_factor_lift
Documentation

The lifted linear factor is monic.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_monic_linear_factor_lift
    (f : Polynomial F.valuationSubring) (hf : f.Monic) (a0 : F.valuationSubring)
    (hroot : f.eval a0 ∈ F.maximalIdeal)
    (hsimple : IsUnit (Ideal.Quotient.mk F.maximalIdeal (f.derivative.eval a0))) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ a - a0 ∈ F.maximalIdeal ∧
        (Polynomial.X - Polynomial.C a).Monic ∧
          f = (Polynomial.X - Polynomial.C a) * q
theorem

exists_monic_linear_factor_lift_with_monic_quotient

L170 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_linear_factor_lift_with_monic_quotient
Documentation

Hensel's lemma gives a monic linear factor whose quotient is also monic.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_monic_linear_factor_lift_with_monic_quotient
    (f : Polynomial F.valuationSubring) (hf : f.Monic) (a0 : F.valuationSubring)
    (hroot : f.eval a0 ∈ F.maximalIdeal)
    (hsimple : IsUnit (Ideal.Quotient.mk F.maximalIdeal (f.derivative.eval a0))) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ a - a0 ∈ F.maximalIdeal ∧
        (Polynomial.X - Polynomial.C a).Monic ∧ q.Monic ∧
          f = (Polynomial.X - Polynomial.C a) * q
theorem

exists_monic_linear_factor_lift_of_residue_root

L187 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_linear_factor_lift_of_residue_root
Documentation

Residue-field form of the lifted monic linear factor theorem. Starting from an actual simple root of the reduced polynomial over the residue field, Hensel's lemma gives a root with the prescribed residue class, a monic lifted linear factor, and a monic quotient.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_monic_linear_factor_lift_of_residue_root
    (f : Polynomial F.valuationSubring) (hf : f.Monic)
    (aBar : F.residueField)
    (hroot : (f.map F.residueMap).eval aBar = 0)
    (hsimple : (f.derivative.map F.residueMap).eval aBar ≠ 0) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ F.residueMap a = aBar ∧
        (Polynomial.X - Polynomial.C a).Monic ∧ q.Monic ∧
          f = (Polynomial.X - Polynomial.C a) * q
theorem

exists_monic_linear_factor_lift_of_reduced_simple_root

L233 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_linear_factor_lift_of_reduced_simple_root
Documentation

Natural reduced-polynomial form of the lifted monic linear factor theorem. The simplicity condition is stated using the derivative of the reduced polynomial itself.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_monic_linear_factor_lift_of_reduced_simple_root
    (f : Polynomial F.valuationSubring) (hf : f.Monic)
    (aBar : F.residueField)
    (hroot : (f.map F.residueMap).eval aBar = 0)
    (hsimple : ((f.map F.residueMap).derivative).eval aBar ≠ 0) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ F.residueMap a = aBar ∧
        (Polynomial.X - Polynomial.C a).Monic ∧ q.Monic ∧
          f = (Polynomial.X - Polynomial.C a) * q
theorem

exists_monic_linear_factor_lift_of_reduced_simple_root_with_reduction

L249 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_linear_factor_lift_of_reduced_simple_root_with_reduction
Documentation

Reduced-factorization compatibility for the lifted monic linear factor. The lifted factorization reduces to the original reduced linear factor X - aBar. This is the linear-factor compatibility input needed for the later full factorization-form Hensel theorem.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_monic_linear_factor_lift_of_reduced_simple_root_with_reduction
    (f : Polynomial F.valuationSubring) (hf : f.Monic)
    (aBar : F.residueField)
    (hroot : (f.map F.residueMap).eval aBar = 0)
    (hsimple : ((f.map F.residueMap).derivative).eval aBar ≠ 0) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ F.residueMap a = aBar ∧
        (Polynomial.X - Polynomial.C a).Monic ∧ q.Monic ∧
          f = (Polynomial.X - Polynomial.C a) * q ∧
            (q.map F.residueMap).Monic ∧
              f.map F.residueMap =
                (Polynomial.X - Polynomial.C aBar) * q.map F.residueMap
theorem

exists_monic_linear_factor_lift_of_reduced_simple_root_with_coprime_quotient

L282 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.exists_monic_linear_factor_lift_of_reduced_simple_root_with_coprime_quotient
Documentation

A Hensel lift of a simple reduced root has a unit derivative at the lifted root, so the lifted linear factor is coprime to the lifted quotient.

This is the first construction-level bridge from simple-root Hensel to the coprime factorization form: the coprimeness is proved from the actual lifted factorization and the nonzero reduced derivative, not assumed as extra data.

Source context 8 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
namespace HenselianDVF
open ValuationTheory.DiscreteValuationField.ResidueField
variable {K : Type u} [Field K]
variable (F : HenselianDVF.{u, v} K)
Lean source · statement
theorem exists_monic_linear_factor_lift_of_reduced_simple_root_with_coprime_quotient
    (f : Polynomial F.valuationSubring) (hf : f.Monic)
    (aBar : F.residueField)
    (hroot : (f.map F.residueMap).eval aBar = 0)
    (hsimple : ((f.map F.residueMap).derivative).eval aBar ≠ 0) :
    ∃ a : F.valuationSubring, ∃ q : Polynomial F.valuationSubring,
      f.IsRoot a ∧ F.residueMap a = aBar ∧
        (Polynomial.X - Polynomial.C a).Monic ∧ q.Monic ∧
          IsUnit (f.derivative.eval a) ∧
            IsCoprime (Polynomial.X - Polynomial.C a) q ∧
              f = (Polynomial.X - Polynomial.C a) * q ∧
                (q.map F.residueMap).Monic ∧
                  f.map F.residueMap =
                    (Polynomial.X - Polynomial.C aBar) * q.map F.residueMap

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.