Nyll.SchemeTheory.RingTheory.HenselianFactorization

Module documentation

Lifting coprime monic factorizations over Henselian pairs

The universal coprime factorization ring is étale over the coefficient ring. Its section supplied by a factorization over the quotient therefore lifts over a Henselian pair. Naturality of its representing equivalence gives the exact reductions of both lifted factors.

theorem

exists_coprime_factorization_lift_of_henselian

L32 ↗

Polynomial.exists_coprime_factorization_lift_of_henselian

Documentation

A monic coprime factorization over a quotient of a Henselian pair lifts to a monic coprime factorization with the same fixed degrees and exact reductions.

The coefficient-based MonicDegreeEq type also handles trivial rings, so no nontriviality assumption on the ring or its quotient is needed.

Source context 3 commands

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

@[expose] public section
universe u
namespace Polynomial

Lean source · statement

theorem exists_coprime_factorization_lift_of_henselian
    {R : Type u} [CommRing R] (I : Ideal R) [HenselianRing R I]
    {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : MonicDegreeEq R n)
    (q₀ : MonicDegreeEq (R ⧸ I) m × MonicDegreeEq (R ⧸ I) k)
    (hprod : q₀.1.1 * q₀.2.1 = p.1.map (Ideal.Quotient.mk I))
    (hcoprime : IsCoprime q₀.1.1 q₀.2.1) :
    ∃ q : MonicDegreeEq R m × MonicDegreeEq R k,
      q.1.1 * q.2.1 = p.1 ∧ IsCoprime q.1.1 q.2.1 ∧
        q.1.map (Ideal.Quotient.mk I) = q₀.1 ∧
        q.2.map (Ideal.Quotient.mk I) = q₀.2

Module documentation

Lifting coprime monic factorizations over Henselian pairs

Declarations

exists_coprime_factorization_lift_of_henselian