NYLL
Module

Assembly.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.Factorization.Assembly
5 declarations indexed from sourceView source ↗

Module documentation

explicit valuation-ring Hensel statement

This file connects the chosen finite-minimum coefficient to the displayed-factor complete-limit theorem.

Imports3
Imported by11

Declarations

theorem

henselFactorization_exists_limit_factorization_of_coprime_lifts_valuationRing

L29 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_limit_factorization_of_coprime_lifts_valuationRing
Documentation

complete-limit factorization from coprime residual factors and chosen lifts over a valuation ring. The element π is chosen from the finite set of coefficients of the two initial error polynomials, as in the proof.

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_limit_factorization_of_coprime_lifts_valuationRing
    {R : Type*} [CommRing R] [Nontrivial R] [PreValuationRing R]
    [NoZeroDivisors R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) R]
    [IsHausdorff (IsLocalRing.maximalIdeal R) R]
    {f g0 h0 : R[X]}
    {gbar hbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hh0map : h0.map (IsLocalRing.residue R) = hbar)
    (hcop : IsCoprime gbar hbar)
    (hf : f.natDegree ≤ d)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hmd : m ≤ d) :
    ∃ G H : R[X],
      G.natDegree ≤ m ∧ H.natDegree ≤ d - m ∧ f = G * H ∧
        G.map (IsLocalRing.residue R) = gbar ∧
        H.map (IsLocalRing.residue R) = hbar
theorem

henselFactorization_exists_limit_factorization_of_coprime_lifts_valuationRing_principal

L88 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_limit_factorization_of_coprime_lifts_valuationRing_principal
Documentation

complete-limit factorization from coprime residual factors and chosen lifts over a valuation ring, using the principal filtration generated by the finite-minimum element π.

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_limit_factorization_of_coprime_lifts_valuationRing_principal
    {R : Type*} [CommRing R] [Nontrivial R] [PreValuationRing R]
    [NoZeroDivisors R]
    (hpre : ∀ π : R, π ≠ 0 → π ∈ IsLocalRing.maximalIdeal R →
      IsPrecomplete (Ideal.span ({π} : Set R)) R)
    (hhaus : ∀ π : R, π ≠ 0 → π ∈ IsLocalRing.maximalIdeal R →
      IsHausdorff (Ideal.span ({π} : Set R)) R)
    {f g0 h0 : R[X]}
    {gbar hbar : (IsLocalRing.ResidueField R)[X]} {m d : ℕ}
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar)
    (hg0map : g0.map (IsLocalRing.residue R) = gbar)
    (hh0map : h0.map (IsLocalRing.residue R) = hbar)
    (hcop : IsCoprime gbar hbar)
    (hf : f.natDegree ≤ d)
    (hg0nat : g0.natDegree = m)
    (hgbar_nat : gbar.natDegree = m)
    (hglead : gbar.leadingCoeff ≠ 0)
    (hh0deg : h0.natDegree ≤ d - m)
    (hmd : m ≤ d) :
    ∃ G H : R[X],
      G.natDegree ≤ m ∧ H.natDegree ≤ d - m ∧ f = G * H ∧
        G.map (IsLocalRing.residue R) = gbar ∧
        H.map (IsLocalRing.residue R) = hbar
theorem

henselFactorization_exists_degreeControlledLifts_of_residual_factorization

L153 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_degreeControlledLifts_of_residual_factorization
Documentation

Degree-controlled polynomial lifts of a nonzero residual factorization. This is the algebraic preparation shared by the maximal-ideal and principal-adic forms of Hensel's lemma.

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_degreeControlledLifts_of_residual_factorization
    {R : Type*} [CommRing R] [IsLocalRing R]
    {f : R[X]} {gbar hbar : (IsLocalRing.ResidueField R)[X]}
    (hprim : f.map (IsLocalRing.residue R) ≠ 0)
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar) :
    ∃ g0 h0 : R[X],
      g0.map (IsLocalRing.residue R) = gbar ∧
        h0.map (IsLocalRing.residue R) = hbar ∧
          g0.natDegree = gbar.natDegree ∧
            h0.natDegree ≤ f.natDegree - gbar.natDegree ∧
              gbar.natDegree ≤ f.natDegree ∧
                gbar.leadingCoeff ≠ 0
theorem

henselFactorization_exists_limit_factorization_of_residual_factors_valuationRing

L205 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_limit_factorization_of_residual_factors_valuationRing
Documentation

explicit residual-factor form of Hensel's lemma for a complete separated valuation ring.

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_limit_factorization_of_residual_factors_valuationRing
    {R : Type*} [CommRing R] [Nontrivial R] [PreValuationRing R]
    [NoZeroDivisors R]
    [IsPrecomplete (IsLocalRing.maximalIdeal R) R]
    [IsHausdorff (IsLocalRing.maximalIdeal R) R]
    {f : R[X]}
    {gbar hbar : (IsLocalRing.ResidueField R)[X]}
    (hprim : f.map (IsLocalRing.residue R) ≠ 0)
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar)
    (hcop : IsCoprime gbar hbar) :
    ∃ G H : R[X],
      G.natDegree = gbar.natDegree ∧
        H.natDegree ≤ f.natDegree - gbar.natDegree ∧
          f = G * H ∧
            G.map (IsLocalRing.residue R) = gbar ∧
              H.map (IsLocalRing.residue R) = hbar
theorem

henselFactorization_exists_limit_factorization_of_residual_factors_valuationRing_principal

L238 ↗
AlgebraicNumberTheory.Valuations.henselFactorization_exists_limit_factorization_of_residual_factors_valuationRing_principal
Documentation

explicit residual-factor form using the principal filtration generated by the finite-minimum element chosen in the proof.

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_limit_factorization_of_residual_factors_valuationRing_principal
    {R : Type*} [CommRing R] [Nontrivial R] [PreValuationRing R]
    [NoZeroDivisors R]
    (hpre : ∀ π : R, π ≠ 0 → π ∈ IsLocalRing.maximalIdeal R →
      IsPrecomplete (Ideal.span ({π} : Set R)) R)
    (hhaus : ∀ π : R, π ≠ 0 → π ∈ IsLocalRing.maximalIdeal R →
      IsHausdorff (Ideal.span ({π} : Set R)) R)
    {f : R[X]}
    {gbar hbar : (IsLocalRing.ResidueField R)[X]}
    (hprim : f.map (IsLocalRing.residue R) ≠ 0)
    (hfbar : f.map (IsLocalRing.residue R) = gbar * hbar)
    (hcop : IsCoprime gbar hbar) :
    ∃ G H : R[X],
      G.natDegree = gbar.natDegree ∧
        H.natDegree ≤ f.natDegree - gbar.natDegree ∧
          f = G * H ∧
            G.map (IsLocalRing.residue R) = gbar ∧
              H.map (IsLocalRing.residue R) = hbar

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