Module

Henselian.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Henselian

16 declarations indexed from sourceView source ↗

Module documentation

Henselian discretely valued fields

This file contains the lightweight package for a discretely valued field whose valuation ring is Henselian at its maximal ideal.

Imports2

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic
Mathlib.RingTheory.Henselian

Imported by13

theorem

idempotentPolynomial_monic

L27 ↗

ValuationTheory.DiscreteValuationField.idempotentPolynomial_monic

Documentation

The idempotent polynomial X^2 - X is monic in every nontrivial coefficient ring.

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 idempotentPolynomial_monic
    {R : Type*} [CommRing R] [Nontrivial R] :
    (Polynomial.X ^ 2 - Polynomial.X : Polynomial R).Monic

theorem

idempotentPolynomial_eval_mem_of_quotient_idempotent

L35 ↗

ValuationTheory.DiscreteValuationField.idempotentPolynomial_eval_mem_of_quotient_idempotent

Documentation

A quotient idempotent is an approximate root of X^2 - X.

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 idempotentPolynomial_eval_mem_of_quotient_idempotent
    {R : Type*} [CommRing R] {I : Ideal R} (a0 : R)
    (ha0 : IsIdempotentElem (Ideal.Quotient.mk I a0)) :
    (Polynomial.X ^ 2 - Polynomial.X : Polynomial R).eval a0 ∈ I

theorem

idempotentPolynomial_derivative_eval_isUnit_of_quotient_idempotent

L47 ↗

ValuationTheory.DiscreteValuationField.idempotentPolynomial_derivative_eval_isUnit_of_quotient_idempotent

Documentation

At a quotient idempotent, the derivative of X^2 - X is a unit in the quotient.

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 idempotentPolynomial_derivative_eval_isUnit_of_quotient_idempotent
    {R : Type*} [CommRing R] {I : Ideal R} (a0 : R)
    (ha0 : IsIdempotentElem (Ideal.Quotient.mk I a0)) :
    IsUnit
      (Ideal.Quotient.mk I
        ((Polynomial.X ^ 2 - Polynomial.X : Polynomial R).derivative.eval a0))

theorem

exists_idempotent_lift_of_surjective_henselianRing_ker

L90 ↗

ValuationTheory.DiscreteValuationField.exists_idempotent_lift_of_surjective_henselianRing_ker

Documentation

Idempotents lift along a surjective ring map whose kernel is a Henselian ideal.

This is the X^2 - X simple-root form of Hensel's lemma. At an idempotent, the derivative 2X - 1 is a unit because its square is 1.

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 exists_idempotent_lift_of_surjective_henselianRing_ker
    {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : Function.Surjective f)
    [HenselianRing R (RingHom.ker f)]
    (e : S) (he : IsIdempotentElem e) :
    ∃ e' : R, IsIdempotentElem e' ∧ f e' = e

theorem

exists_idempotent_lift_of_henselianRing_mk

L139 ↗

ValuationTheory.DiscreteValuationField.exists_idempotent_lift_of_henselianRing_mk

Documentation

Chosen-representative form of idempotent lifting for Henselian pairs.

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 exists_idempotent_lift_of_henselianRing_mk
    {R : Type*} [CommRing R] {I : Ideal R} [HenselianRing R I]
    (a0 : R) (ha0 : IsIdempotentElem (Ideal.Quotient.mk I a0)) :
    ∃ e : R,
      IsIdempotentElem e ∧
        Ideal.Quotient.mk I e = Ideal.Quotient.mk I a0 ∧
        e - a0 ∈ I

theorem

exists_idempotent_lift_of_henselianRing

L180 ↗

ValuationTheory.DiscreteValuationField.exists_idempotent_lift_of_henselianRing

Documentation

Quotient form of idempotent lifting for Henselian pairs: every idempotent modulo the Henselian ideal has an idempotent representative.

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 exists_idempotent_lift_of_henselianRing
    {R : Type*} [CommRing R] {I : Ideal R} [HenselianRing R I]
    (e : R ⧸ I) (he : IsIdempotentElem e) :
    ∃ e' : R, IsIdempotentElem e' ∧ Ideal.Quotient.mk I e' = e

structure

HenselianDVF

L191 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF

Documentation

A Henselian discretely valued field.

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 · full declaration

structure HenselianDVF (K : Type u) [Field K] extends DVF.{u, v} K where
  /-- The valuation ring is Henselian along its maximal ideal. -/
  [instHenselian : HenselianRing toDVF.valuationSubring toDVF.maximalIdeal]

abbrev

valuationSubring

L202 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring

Documentation

Introduces the abbreviation valuationSubring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev valuationSubring (F : HenselianDVF.{u, v} K) : Type u

abbrev

maximalIdeal

L206 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.maximalIdeal

Documentation

Introduces the abbreviation maximalIdeal.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev maximalIdeal (F : HenselianDVF.{u, v} K) : Ideal F.valuationSubring

abbrev

residueField

L210 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.residueField

Documentation

Introduces the abbreviation residueField.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev residueField (F : HenselianDVF.{u, v} K) : Type u

abbrev

residueMap

L214 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.residueMap

Documentation

Introduces the abbreviation residueMap.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

abbrev residueMap (F : HenselianDVF.{u, v} K) :
    RingHom F.valuationSubring F.residueField

theorem

exists_polynomial_lift_residue

L220 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.exists_polynomial_lift_residue

Documentation

Every residue-field polynomial admits a coefficientwise lift to the valuation ring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_polynomial_lift_residue (F : HenselianDVF.{u, v} K)
    (fbar : Polynomial F.residueField) :
    ∃ f : Polynomial F.valuationSubring, f.map F.residueMap = fbar

theorem

valuationSubring_isDiscreteValuationRing

L251 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.valuationSubring_isDiscreteValuationRing

Documentation

The valuation subring of the henselian model is a discrete valuation ring.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

theorem valuationSubring_isDiscreteValuationRing (F : HenselianDVF.{u, v} K) :
    IsDiscreteValuationRing F.valuationSubring

theorem

henselianRing

L256 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.henselianRing

Documentation

The valuation subring of the henselian discrete valuation field is henselian.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

theorem henselianRing (F : HenselianDVF.{u, v} K) :
    HenselianRing F.valuationSubring F.maximalIdeal

theorem

maximalIdeal_ne_bot

L262 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.maximalIdeal_ne_bot

Documentation

The maximal ideal of a Henselian DVF valuation ring is nonzero.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

theorem maximalIdeal_ne_bot (F : HenselianDVF.{u, v} K) :
    F.maximalIdeal ≠ ⊥

theorem

exists_lift_root_simple

L267 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.exists_lift_root_simple

Documentation

Hensel's lemma in the simple-root form used by mathlib.

Source context 7 commands

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

namespace ValuationTheory
noncomputable section
universe u v
namespace DiscreteValuationField
attribute [instance] HenselianDVF.instHenselian
namespace HenselianDVF
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_lift_root_simple (F : HenselianDVF.{u, v} K)
    (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, f.IsRoot a ∧ a - a0 ∈ F.maximalIdeal

Module documentation

Henselian discretely valued fields

Declarations