Henselian rings and Hensel's lemma

TheoremHensel lifting of monic coprime factorizations#✓fully proved

Let \(A\) be a commutative ring and \(I\) an ideal of \(A\) such that \(A\) is \(I\)-adically complete, and let \(f \in A[X]\) be monic. Suppose the reduction of \(f\) modulo \(I\) equals \(\bar g \bar h\), where \(\bar g, \bar h \in (A/I)[X]\) are monic and coprime (that is, \(a \bar g + b \bar h = 1\) for some \(a, b \in (A/I)[X]\)). Then there exist monic \(g, h \in A[X]\) with \(f = gh\) whose reductions modulo \(I\) are \(\bar g\) and \(\bar h\) respectively.

The proof packages the residue factorization via the universal coprime factorization ring, lifts its structure map through \(I\)-adic completeness, and evaluates the universal factors over \(A\).

theorem exists_monic_coprime_factorization_of_isAdicComplete
    (I : Ideal A) [IsAdicComplete I A]
    (f : A[X]) (hf : f.Monic)
    (g_bar h_bar : (A ⧸ I)[X])
    (hg : g_bar.Monic) (hh : h_bar.Monic)
    (hfac : f.map (Ideal.Quotient.mk I) = g_bar * h_bar)
    (hcop : IsCoprime g_bar h_bar) :
    ∃ g h : A[X], g.Monic ∧ h.Monic ∧ f = g * h ∧
      g.map (Ideal.Quotient.mk I) = g_bar ∧
      h.map (Ideal.Quotient.mk I) = h_bar

Used by 4

Used byCharacterization of unramified extensions of a complete DVR · Domains integral over a complete local domain are local · Hensel lifting of monic coprime factorizations, with degrees · Hensel lifting of coprime monic factors over a complete ring

TheoremHensel lifting of monic coprime factorizations, with degrees#✓fully proved

Let \(A\) be a commutative ring and \(I\) an ideal of \(A\) such that \(A\) is \(I\)-adically complete and \(A/I\) is not the zero ring, and let \(f \in A[X]\) be monic. Suppose the reduction of \(f\) modulo \(I\) equals \(\bar g \bar h\), where \(\bar g, \bar h \in (A/I)[X]\) are monic and coprime (that is, \(a \bar g + b \bar h = 1\) for some \(a, b \in (A/I)[X]\)). Then there exist monic \(g, h \in A[X]\) with \(f = gh\) whose reductions modulo \(I\) are \(\bar g\) and \(\bar h\) respectively, and such that \(\deg g = \deg \bar g\) and \(\deg h = \deg \bar h\).

theorem exists_monic_coprime_factorization_of_isAdicComplete_natDegree
    (I : Ideal A) [IsAdicComplete I A] [Nontrivial (A ⧸ I)]
    (f : A[X]) (hf : f.Monic)
    (g_bar h_bar : (A ⧸ I)[X])
    (hg : g_bar.Monic) (hh : h_bar.Monic)
    (hfac : f.map (Ideal.Quotient.mk I) = g_bar * h_bar)
    (hcop : IsCoprime g_bar h_bar) :
    ∃ g h : A[X], g.Monic ∧ h.Monic ∧ f = g * h ∧
      g.map (Ideal.Quotient.mk I) = g_bar ∧
      h.map (Ideal.Quotient.mk I) = h_bar ∧
      g.natDegree = g_bar.natDegree ∧ h.natDegree = h_bar.natDegree

Uses 1 · Used by 2

Proof usesHensel lifting of monic coprime factorizations

Used byAlgebraic closedness of rational Hahn series · Puiseux's theorem

TheoremLocal homomorphisms reflect coprimality with a monic polynomial#✓fully proved

A local ring homomorphism reflects coprimality of polynomials when the first polynomial is monic. Neither ring needs to be local.

theorem Monic.isCoprime_of_isCoprime_map {g h : R[X]} (hg : g.Monic)
    (π : R →+* S) [IsLocalHom π]
    (hcop : IsCoprime (g.map π) (h.map π)) : IsCoprime g h

Used by 2

Used byHensel lifting of coprime monic factors over a complete ring · Unique lift of a monic factor through a nilpotent-kernel surjection

TheoremUnique lift of a monic factor through a nilpotent-kernel surjection#✓fully proved

A monic factor of a coprime factorization lifts uniquely through a surjective homomorphism with nilpotent kernel. The original polynomial and the complementary reduced factor are not required to be monic.

theorem existsUnique_monic_map_eq_dvd_of_isCoprime_of_ker_pow_eq_bot
    (π : R →+* S) (hπ : Function.Surjective π)
    (hnil : ∃ n : ℕ, RingHom.ker π ^ n = ⊥)
    (f : R[X]) (g' k' : S[X]) (hg' : g'.Monic) (hcop : IsCoprime g' k')
    (hfac : f.map π = g' * k') :
    ∃! g : R[X], g.Monic ∧ g.map π = g' ∧ g ∣ f

Uses 1

Proof usesLocal homomorphisms reflect coprimality with a monic polynomial

TheoremHensel lifting of coprime monic factors over a complete ring#✓fully proved

Coprime monic factors lift over a ring complete at the kernel of a surjective homomorphism. The lifts are coprime, and the first is the unique monic divisor of the original polynomial with its specified reduction.

theorem exists_monic_mul_eq_and_map_eq_of_isCoprime_of_isAdicComplete
    (π : R →+* S) (hπ : Function.Surjective π)
    [IsAdicComplete (RingHom.ker π) R]
    {F : R[X]} (hF : F.Monic) {g₀ h₀ : S[X]} (hg₀ : g₀.Monic) (hh₀ : h₀.Monic)
    (hcop : IsCoprime g₀ h₀) (hF₀ : F.map π = g₀ * h₀) :
    ∃ g h : R[X], g.Monic ∧ h.Monic ∧ g * h = F ∧
      g.map π = g₀ ∧ h.map π = h₀ ∧ IsCoprime g h ∧
      ∀ g' : R[X], g'.Monic → g'.map π = g₀ → g' ∣ F → g' = g

Uses 2

Proof usesLocal homomorphisms reflect coprimality with a monic polynomial · Hensel lifting of monic coprime factorizations

TheoremHensel's lemma for complete discrete valuation rings#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) that is complete and Hausdorff for the \(\mathfrak{m}\)-adic topology. Let \(f \in A[X]\) have derivative \(f'\), and let \(a_0 \in A\) satisfy \(f(a_0) \in \mathfrak{m}\) with \(f'(a_0)\) a unit of \(A\). Then \(f\) has a root \(a \in A\) with \(a - a_0 \in \mathfrak{m}\).

theorem Polynomial.exists_isRoot_sub_mem_maximalIdeal_of_isUnit_derivative (f : A[X])
    (a₀ : A) (h₁ : f.eval a₀ ∈ maximalIdeal A)
    (h₂ : IsUnit (f.derivative.eval a₀)) :
    ∃ a : A, f.IsRoot a ∧ a - a₀ ∈ maximalIdeal A

Used by 1

Used byHensel's lemma with a derivative bound

TheoremPolynomials do not decrease the valuation of differences#✓fully proved

Let \(A\) be a discrete valuation ring with normalized additive valuation \(v \colon A \to \mathbb{N} \cup \{\infty\}\). For every polynomial \(p \in A[X]\) and all \(a, a_0 \in A\), we have \(v(a - a_0) \le v(p(a) - p(a_0))\).

theorem Polynomial.addVal_sub_le_addVal_eval_sub (p : A[X]) (a a₀ : A) :
    IsDiscreteValuationRing.addVal A (a - a₀) ≤
      IsDiscreteValuationRing.addVal A (p.eval a - p.eval a₀)

Used by 1

Used byNearby roots share the derivative valuation

TheoremNearby roots share the derivative valuation#✓fully proved

A root sufficiently close to the approximation has the same derivative valuation.

theorem Polynomial.addVal_derivative_eval_eq_of_lt_addVal_sub
    (f : A[X]) (a a₀ : A)
    (hva : IsDiscreteValuationRing.addVal A (f.derivative.eval a₀) <
      IsDiscreteValuationRing.addVal A (a - a₀)) :
    IsDiscreteValuationRing.addVal A (f.derivative.eval a) =
      IsDiscreteValuationRing.addVal A (f.derivative.eval a₀)

Uses 1 · Used by 2

Proof usesPolynomials do not decrease the valuation of differences

Used byUniqueness of roots near a point · Hensel's lemma with a derivative bound

TheoremUniqueness of roots near a point#✓fully proved

Let \(A\) be a discrete valuation ring with normalized additive valuation \(v \colon A \to \mathbb{N} \cup \{\infty\}\), let \(f \in A[X]\) have derivative \(f'\), and let \(a_0 \in A\). If \(a, a' \in A\) are roots of \(f\) with \(v(f'(a_0)) < v(a - a_0)\) and \(v(f'(a_0)) < v(a' - a_0)\), then \(a = a'\).

theorem Polynomial.eq_of_isRoot_of_addVal_derivative_lt_addVal_sub
    (f : A[X]) (a a' a₀ : A)
    (hfa : f.IsRoot a) (hfa' : f.IsRoot a')
    (hva : addVal A (f.derivative.eval a₀) < addVal A (a - a₀))
    (hva' : addVal A (f.derivative.eval a₀) < addVal A (a' - a₀)) :
    a = a'

Uses 1 · Used by 1

Proof usesNearby roots share the derivative valuation

Used byHensel's lemma with a derivative bound

TheoremElements of the maximal ideal have positive valuation#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) and normalized additive valuation \(v \colon A \to \mathbb{N} \cup \{\infty\}\). If \(d \in A\) is nonzero and \(q \in \mathfrak{m}\), then \(v(d) < v(d) + v(q)\).

Since \(v(dq) = v(d) + v(q)\), multiplying a nonzero element by an element of the maximal ideal strictly increases its valuation.

theorem addVal_lt_addVal_add_of_mem_maximalIdeal {d q : A}
    (hd : d ≠ 0) (hq : q ∈ maximalIdeal A) :
    addVal A d < addVal A d + addVal A q

Used by 1

Used byHensel's lemma with a derivative bound

TheoremHensel's lemma with a derivative bound#✓fully proved

Let \(A\) be a discrete valuation ring with maximal ideal \(\mathfrak{m}\) that is complete and Hausdorff for the \(\mathfrak{m}\)-adic topology, and let \(v \colon A \to \mathbb{N} \cup \{\infty\}\) be its normalized additive valuation. Let \(f \in A[X]\) have derivative \(f'\), and let \(a_0 \in A\) satisfy \(2 v(f'(a_0)) < v(f(a_0))\). Then \(f\) has a root \(a \in A\) such that \(a - a_0 \in \mathfrak{m}\), \(v(f'(a_0)) < v(a - a_0)\), \(v(f(a_0)) \le v(a - a_0) + 2 v(f'(a_0))\) and \(v(f'(a)) = v(f'(a_0))\). Moreover, every root \(a' \in A\) of \(f\) with \(v(f'(a_0)) < v(a' - a_0)\) equals \(a\).

theorem Polynomial.exists_isRoot_of_two_mul_addVal_derivative_lt_addVal
    (f : A[X]) (a₀ : A)
    (hval : 2 * addVal A (f.derivative.eval a₀) < addVal A (f.eval a₀)) :
    ∃ a : A,
    f.IsRoot a ∧
    a - a₀ ∈ maximalIdeal A ∧
    addVal A (f.derivative.eval a₀) < addVal A (a - a₀) ∧
    addVal A (f.eval a₀) ≤
      addVal A (a - a₀) + 2 * addVal A (f.derivative.eval a₀) ∧
    (∀ a' : A, f.IsRoot a' →
      addVal A (f.derivative.eval a₀) < addVal A (a' - a₀) → a' = a) ∧
    addVal A (f.derivative.eval a) = addVal A (f.derivative.eval a₀)

Sources

• ATLAS Hensel endpoint; the published statement dropped the condition \(v(f'(a_0)) < v(a - a_0)\) on the root, which is kept here so that uniqueness applies to it.

Uses 4

Proof usesElements of the maximal ideal have positive valuation · Nearby roots share the derivative valuation · Uniqueness of roots near a point · Hensel's lemma for complete discrete valuation rings

TheoremSections of étale algebras over Henselian local rings#✓fully proved

Over a Henselian local ring, an étale algebra has a section lifting any residue-field point.

theorem HenselianLocalRing.exists_algHom_lift_of_etale
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Etale R S]
    (φ : S →ₐ[R] IsLocalRing.ResidueField R) :
    ∃ ψ : S →ₐ[R] R,
      ∀ s : S, algebraMap R (IsLocalRing.ResidueField R) (ψ s) = φ s

TheoremComplete local rings are Henselian#✓fully proved

Let \(R\) be a local ring with maximal ideal \(\mathfrak m\). If \(R\) is Hausdorff and complete for the \(\mathfrak m\)-adic topology, then \(R\) is a Henselian local ring.

theorem HenselianLocalRing.of_isAdicComplete_maximalIdeal
    (R : Type*) [CommRing R] [IsLocalRing R]
    [IsAdicComplete (IsLocalRing.maximalIdeal R) R] :
    HenselianLocalRing R

Used by 2

Used byLifting residue-field isomorphisms between complete étale DVR extensions · Algebra maps from an étale DVR extension into a complete one match residue-field maps

TheoremValuation subrings of algebraically closed fields are Henselian#✓fully proved

A valuation subring of an algebraically closed field is Henselian.

theorem ValuationSubring.henselianLocalRing_of_isAlgClosed {L : Type*} [Field L]
    [IsAlgClosed L] (A : ValuationSubring L) : HenselianLocalRing A

14 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.