Nyll.ValuedFieldTheory.Valuation.Henselian.CoprimeFactorLifting

Module documentation

Coprime factor lifting from the simple-root Hensel property

A coprime monic factorization over the residue field gives a point of the universal coprime factorization algebra. This algebra is etale, so its residue point lifts over a Henselian pair. The universal factors give the requested factorization, with their degrees and prescribed reductions.

theorem

exists_coprime_factor_lift

L27 ↗

ValuationTheory.Henselian.exists_coprime_factor_lift

Documentation

A coprime monic factorization modulo a maximal Henselian ideal lifts to a coprime monic factorization over the base ring with the same degrees.

Source context 3 commands

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

namespace ValuationTheory.Henselian
open Polynomial
variable {R : Type*} [CommRing R] {I : Ideal R} [I.IsMaximal] [HenselianRing R I]

Lean source · statement

theorem exists_coprime_factor_lift
    (f : R[X]) (gbar hbar : (R ⧸ I)[X])
    (hf : f.Monic) (hgbar : gbar.Monic) (hhbar : hbar.Monic)
    (hfac : f.map (Ideal.Quotient.mk I) = gbar * hbar)
    (hcop : IsCoprime gbar hbar) :
    ∃ g h : R[X], g.Monic ∧ h.Monic ∧ f = g * h ∧
      g.natDegree = gbar.natDegree ∧ h.natDegree = hbar.natDegree ∧
      g.map (Ideal.Quotient.mk I) = gbar ∧ h.map (Ideal.Quotient.mk I) = hbar ∧
      IsCoprime g h

Module documentation

Coprime factor lifting from the simple-root Hensel property

Declarations

exists_coprime_factor_lift