Module

CoefficientMinimum.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.CoefficientMinimum

13 declarations indexed from sourceView source ↗

Module documentation

the finite minimum coefficient

The coefficientwise proof of Hensel's lemma chooses, among the finitely many coefficients of f - g₀h₀ and ag₀ + bh₀ - 1, one coefficient of minimum valuation and calls it π. In a valuation ring this is the same algebraic input as choosing one coefficient that divides all coefficients in the finite set.

Imports2

Mathlib.RingTheory.Valuation.ValuationRing
Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.ErrorPowers

Imported by11

theorem

henselFactorization_exists_mem_finset_dvd_all

L29 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_mem_finset_dvd_all

Documentation

finite divisibility minimum in a valuation ring: every nonempty finite set has an element that divides all elements of the set.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_mem_finset_dvd_all
    {R : Type*} [Monoid R] [PreValuationRing R] {s : Finset R}
    (hs : s.Nonempty) :
    ∃ π ∈ s, ∀ x ∈ s, π ∣ x

def

henselFactorization_twoPolynomialCoeffFinset

L63 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_twoPolynomialCoeffFinset

Documentation

the finite set of coefficients of two polynomials from which the construction chooses the minimum-value coefficient.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

def henselFactorization_twoPolynomialCoeffFinset
    {R : Type*} [Semiring R] (P Q : R[X]) : Finset R

theorem

henselFactorization_mem_twoPolynomialCoeffFinset_left

L71 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_mem_twoPolynomialCoeffFinset_left

Documentation

A coefficient supported in the left polynomial belongs to the two-polynomial coefficient set.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_mem_twoPolynomialCoeffFinset_left
    {R : Type*} [Semiring R] {P Q : R[X]} {n : ℕ}
    (hn : n ∈ P.support) :
    P.coeff n ∈ henselFactorization_twoPolynomialCoeffFinset P Q

theorem

henselFactorization_mem_twoPolynomialCoeffFinset_right

L82 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_mem_twoPolynomialCoeffFinset_right

Documentation

A coefficient supported in the right polynomial belongs to the two-polynomial coefficient set.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_mem_twoPolynomialCoeffFinset_right
    {R : Type*} [Semiring R] {P Q : R[X]} {n : ℕ}
    (hn : n ∈ Q.support) :
    Q.coeff n ∈ henselFactorization_twoPolynomialCoeffFinset P Q

theorem

henselFactorization_ne_zero_of_mem_twoPolynomialCoeffFinset

L93 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_ne_zero_of_mem_twoPolynomialCoeffFinset

Documentation

every element of the finite coefficient set is a nonzero coefficient.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_ne_zero_of_mem_twoPolynomialCoeffFinset
    {R : Type*} [Semiring R] {P Q : R[X]} {x : R}
    (hx : x ∈ henselFactorization_twoPolynomialCoeffFinset P Q) :
    x ≠ 0

theorem

henselFactorization_exists_coeff_dvd_all_two_polynomials

L108 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_coeff_dvd_all_two_polynomials

Documentation

if the two-polynomial coefficient set is nonempty, one of its coefficients divides every coefficient of both polynomials.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_coeff_dvd_all_two_polynomials
    {R : Type*} [CommRing R] [PreValuationRing R] {P Q : R[X]}
    (hs : (henselFactorization_twoPolynomialCoeffFinset P Q).Nonempty) :
    ∃ π ∈ henselFactorization_twoPolynomialCoeffFinset P Q,
      (∀ n : ℕ, π ∣ P.coeff n) ∧
        (∀ n : ℕ, π ∣ Q.coeff n)

theorem

henselFactorization_exists_coeff_mem_ideal_dvd_all_two_polynomials

L136 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_coeff_mem_ideal_dvd_all_two_polynomials

Documentation

if the two polynomials have coefficients in an ideal, the chosen finite-minimum coefficient lies in the same ideal.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_coeff_mem_ideal_dvd_all_two_polynomials
    {R : Type*} [CommRing R] [PreValuationRing R] {I : Ideal R}
    {P Q : R[X]}
    (hP : ∀ n : ℕ, P.coeff n ∈ I)
    (hQ : ∀ n : ℕ, Q.coeff n ∈ I)
    (hs : (henselFactorization_twoPolynomialCoeffFinset P Q).Nonempty) :
    ∃ π ∈ I,
      π ∈ henselFactorization_twoPolynomialCoeffFinset P Q ∧
        (∀ n : ℕ, π ∣ P.coeff n) ∧
          (∀ n : ℕ, π ∣ Q.coeff n)

theorem

henselFactorization_exists_coeff_mem_ideal_minimum_factor_two_polynomials

L166 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_coeff_mem_ideal_minimum_factor_two_polynomials

Documentation

nonempty finite-minimum branch with the ideal membership retained: if both source polynomials have coefficients in I, the chosen coefficient π lies in I and simultaneously factors both polynomials.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_coeff_mem_ideal_minimum_factor_two_polynomials
    {R : Type*} [CommRing R] [PreValuationRing R] {I : Ideal R}
    {P Q : R[X]}
    (hP : ∀ n : ℕ, P.coeff n ∈ I)
    (hQ : ∀ n : ℕ, Q.coeff n ∈ I)
    (hs : (henselFactorization_twoPolynomialCoeffFinset P Q).Nonempty) :
    ∃ π ∈ I,
      π ∈ henselFactorization_twoPolynomialCoeffFinset P Q ∧
        (∃ P' : R[X], P = Polynomial.C π * P') ∧
          (∃ Q' : R[X], Q = Polynomial.C π * Q')

theorem

henselFactorization_exists_pi_factor_initial_errors_of_nonempty

L196 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_pi_factor_initial_errors_of_nonempty

Documentation

the first choice of π in the nonempty branch: from the two initial source polynomials f - g0*h0 and a*g0 + b*h0 - 1, choose a coefficient π lying in the maximal ideal that factors both source polynomials.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_pi_factor_initial_errors_of_nonempty
    {R : Type*} [CommRing R] [IsLocalRing R] [PreValuationRing R]
    {f g0 h0 a b : R[X]}
    (herr : ∀ n : ℕ, (f - g0 * h0).coeff n ∈
      IsLocalRing.maximalIdeal R)
    (hbezerr : ∀ n : ℕ, (a * g0 + b * h0 - 1).coeff n ∈
      IsLocalRing.maximalIdeal R)
    (hs :
      (henselFactorization_twoPolynomialCoeffFinset
        (f - g0 * h0) (a * g0 + b * h0 - 1)).Nonempty) :
    ∃ π ∈ IsLocalRing.maximalIdeal R,
      π ∈ henselFactorization_twoPolynomialCoeffFinset
        (f - g0 * h0) (a * g0 + b * h0 - 1) ∧
        (∃ f1 : R[X], f - g0 * h0 = Polynomial.C π * f1) ∧
          (∃ e1 : R[X],
            a * g0 + b * h0 - 1 = Polynomial.C π * e1)

theorem

henselFactorization_exists_pi_factor_initial_errors_of_residue_lifts_of_nonempty

L221 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_exists_pi_factor_initial_errors_of_residue_lifts_of_nonempty

Documentation

residue-factorization form of the first π choice in the nonempty branch. The two coefficient-in-the-maximal-ideal inputs are produced from the residue factorization and lifted Bezout congruence.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_exists_pi_factor_initial_errors_of_residue_lifts_of_nonempty
    {R : Type*} [CommRing R] [IsLocalRing R] [PreValuationRing R]
    {f g0 h0 a b : R[X]}
    {gbar hbar : (IsLocalRing.ResidueField R)[X]}
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar)
    (hg0 : g0.map (IsLocalRing.residue R) = gbar)
    (hh0 : h0.map (IsLocalRing.residue R) = hbar)
    (hbez : (a * g0 + b * h0).map (IsLocalRing.residue R) = 1)
    (hs :
      (henselFactorization_twoPolynomialCoeffFinset
        (f - g0 * h0) (a * g0 + b * h0 - 1)).Nonempty) :
    ∃ π ∈ IsLocalRing.maximalIdeal R,
      π ∈ henselFactorization_twoPolynomialCoeffFinset
        (f - g0 * h0) (a * g0 + b * h0 - 1) ∧
        (∃ f1 : R[X], f - g0 * h0 = Polynomial.C π * f1) ∧
          (∃ e1 : R[X],
            a * g0 + b * h0 - 1 = Polynomial.C π * e1)

theorem

henselFactorization_left_eq_zero_of_twoPolynomialCoeffFinset_empty

L247 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_left_eq_zero_of_twoPolynomialCoeffFinset_empty

Documentation

if the finite coefficient set is empty, the first polynomial is zero.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_left_eq_zero_of_twoPolynomialCoeffFinset_empty
    {R : Type*} [Semiring R] {P Q : R[X]}
    (h : henselFactorization_twoPolynomialCoeffFinset P Q = ∅) :
    P = 0

theorem

henselFactorization_right_eq_zero_of_twoPolynomialCoeffFinset_empty

L263 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_right_eq_zero_of_twoPolynomialCoeffFinset_empty

Documentation

if the finite coefficient set is empty, the second polynomial is zero.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_right_eq_zero_of_twoPolynomialCoeffFinset_empty
    {R : Type*} [Semiring R] {P Q : R[X]}
    (h : henselFactorization_twoPolynomialCoeffFinset P Q = ∅) :
    Q = 0

theorem

henselFactorization_twoPolynomialCoeffFinset_empty_iff

L279 ↗

AlgebraicNumberTheory.Valuations.henselFactorization_twoPolynomialCoeffFinset_empty_iff

Documentation

the empty finite coefficient set is exactly the branch where both source polynomials are zero.

Source context 4 commands

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

noncomputable section
open scoped Polynomial
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem henselFactorization_twoPolynomialCoeffFinset_empty_iff
    {R : Type*} [Semiring R] {P Q : R[X]} :
    henselFactorization_twoPolynomialCoeffFinset P Q = ∅ ↔ P = 0 ∧ Q = 0

Module documentation

the finite minimum coefficient

Declarations