13.6. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexHenselMathlib proves it correct against Mathlib's Polynomial: the factorization the executable routine lifts is genuine modulo p ^ k, it extends the input factorization mod p, it preserves degrees, and it is unique among coprime monic lifts with the same reduction mod p.

theorem

HexHenselMathlib.hensel_correct (f g h : Hex.ZPoly) (p k : ℕ)
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (s t : Hex.FpPoly p)
  (hk : 1 ≤ k) (hp : 1 < p) (hprod : (g * h).congr f p)
  (hbez :
    (s * Hex.ZPoly.modP p g + t * Hex.ZPoly.modP p h).liftToZ.congr 1 p)
  (hmonic : Hex.DensePoly.Monic g)
  (hgdeg : 0 < (Hex.DensePoly.degree? g).getD 0) :
  have r := Hex.ZPoly.henselLift p k f g h s t;
  have φ := Int.castRingHom (ZMod (p ^ k));
  Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) *
      Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) =
    Polynomial.map φ (HexPolyMathlib.toPolynomial f)
HexHenselMathlib.hensel_correct
  (f g h : Hex.ZPoly) (p k : ℕ)
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (s t : Hex.FpPoly p) (hk : 1 ≤ k)
  (hp : 1 < p) (hprod : (g * h).congr f p)
  (hbez :
    (s * Hex.ZPoly.modP p g +
            t *
              Hex.ZPoly.modP p
                h).liftToZ.congr
      1 p)
  (hmonic : Hex.DensePoly.Monic g)
  (hgdeg :
    0 <
      (Hex.DensePoly.degree? g).getD 0) :
  have r :=
    Hex.ZPoly.henselLift p k f g h s t;
  have φ :=
    Int.castRingHom (ZMod (p ^ k));
  Polynomial.map φ
        (HexPolyMathlib.toPolynomial
          r.g) *
      Polynomial.map φ
        (HexPolyMathlib.toPolynomial
          r.h) =
    Polynomial.map φ
      (HexPolyMathlib.toPolynomial f)

The iterative executable lift gives a factorization of f over Mathlib polynomials modulo p^k.

theorem

HexHenselMathlib.hensel_extends (f g h : Hex.ZPoly) (p k : ℕ)
  [Hex.ZMod64.Bounds p] (s t : Hex.FpPoly p) (hk : 1 ≤ k)
  (_hprod : (g * h).congr f p)
  (_hbez :
    (s * Hex.ZPoly.modP p g + t * Hex.ZPoly.modP p h).liftToZ.congr 1 p)
  (_hmonic : Hex.DensePoly.Monic g) :
  have r := Hex.ZPoly.henselLift p k f g h s t;
  have φ := Int.castRingHom (ZMod p);
  Polynomial.map φ (HexPolyMathlib.toPolynomial r.g) =
      Polynomial.map φ (HexPolyMathlib.toPolynomial g) ∧
    Polynomial.map φ (HexPolyMathlib.toPolynomial r.h) =
      Polynomial.map φ (HexPolyMathlib.toPolynomial h)
HexHenselMathlib.hensel_extends
  (f g h : Hex.ZPoly) (p k : ℕ)
  [Hex.ZMod64.Bounds p]
  (s t : Hex.FpPoly p) (hk : 1 ≤ k)
  (_hprod : (g * h).congr f p)
  (_hbez :
    (s * Hex.ZPoly.modP p g +
            t *
              Hex.ZPoly.modP p
                h).liftToZ.congr
      1 p)
  (_hmonic : Hex.DensePoly.Monic g) :
  have r :=
    Hex.ZPoly.henselLift p k f g h s t;
  have φ := Int.castRingHom (ZMod p);
  Polynomial.map φ
        (HexPolyMathlib.toPolynomial
          r.g) =
      Polynomial.map φ
        (HexPolyMathlib.toPolynomial g) ∧
    Polynomial.map φ
        (HexPolyMathlib.toPolynomial
          r.h) =
      Polynomial.map φ
        (HexPolyMathlib.toPolynomial h)

The iterative executable lift extends the input factorization modulo p.

theorem

HexHenselMathlib.hensel_degree (f g h : Hex.ZPoly) (p k : ℕ)
  [Hex.ZMod64.Bounds p] [Hex.ZMod64.PrimeModulus p] (s t : Hex.FpPoly p)
  (hk : 1 ≤ k) (hp : 1 < p) (hprod : (g * h).congr f p)
  (hbez :
    (s * Hex.ZPoly.modP p g + t * Hex.ZPoly.modP p h).liftToZ.congr 1 p)
  (hmonic : Hex.DensePoly.Monic g)
  (hgdeg : 0 < (Hex.DensePoly.degree? g).getD 0) :
  have r := Hex.ZPoly.henselLift p k f g h s t;
  (HexPolyMathlib.toPolynomial r.g).natDegree =
    (HexPolyMathlib.toPolynomial g).natDegree
HexHenselMathlib.hensel_degree
  (f g h : Hex.ZPoly) (p k : ℕ)
  [Hex.ZMod64.Bounds p]
  [Hex.ZMod64.PrimeModulus p]
  (s t : Hex.FpPoly p) (hk : 1 ≤ k)
  (hp : 1 < p) (hprod : (g * h).congr f p)
  (hbez :
    (s * Hex.ZPoly.modP p g +
            t *
              Hex.ZPoly.modP p
                h).liftToZ.congr
      1 p)
  (hmonic : Hex.DensePoly.Monic g)
  (hgdeg :
    0 <
      (Hex.DensePoly.degree? g).getD 0) :
  have r :=
    Hex.ZPoly.henselLift p k f g h s t;
  (HexPolyMathlib.toPolynomial
        r.g).natDegree =
    (HexPolyMathlib.toPolynomial
        g).natDegree

The iterative executable lift preserves the Mathlib degree of the monic lifted factor.

theorem

HexHenselMathlib.hensel_unique (f g h g' h' : Polynomial ℤ) (p k : ℕ)
  [Fact (Nat.Prime p)] (_hk : 0 < k) (hg : g.Monic) (hg' : g'.Monic)
  (hdeg : g.natDegree = g'.natDegree)
  (hprod :
    have φ := Int.castRingHom (ZMod (p ^ k));
    Polynomial.map φ g * Polynomial.map φ h = Polynomial.map φ f)
  (hprod' :
    have φ := Int.castRingHom (ZMod (p ^ k));
    Polynomial.map φ g' * Polynomial.map φ h' = Polynomial.map φ f)
  (hg1 :
    have φ := Int.castRingHom (ZMod p);
    Polynomial.map φ g = Polynomial.map φ g')
  (_hh1 :
    have φ := Int.castRingHom (ZMod p);
    Polynomial.map φ h = Polynomial.map φ h')
  (hcop :
    have φ := Int.castRingHom (ZMod p);
    IsCoprime (Polynomial.map φ g) (Polynomial.map φ h)) :
  have φ := Int.castRingHom (ZMod (p ^ k));
  Polynomial.map φ g = Polynomial.map φ g' ∧
    Polynomial.map φ h = Polynomial.map φ h'
HexHenselMathlib.hensel_unique
  (f g h g' h' : Polynomial ℤ) (p k : ℕ)
  [Fact (Nat.Prime p)] (_hk : 0 < k)
  (hg : g.Monic) (hg' : g'.Monic)
  (hdeg : g.natDegree = g'.natDegree)
  (hprod :
    have φ :=
      Int.castRingHom (ZMod (p ^ k));
    Polynomial.map φ g *
        Polynomial.map φ h =
      Polynomial.map φ f)
  (hprod' :
    have φ :=
      Int.castRingHom (ZMod (p ^ k));
    Polynomial.map φ g' *
        Polynomial.map φ h' =
      Polynomial.map φ f)
  (hg1 :
    have φ := Int.castRingHom (ZMod p);
    Polynomial.map φ g =
      Polynomial.map φ g')
  (_hh1 :
    have φ := Int.castRingHom (ZMod p);
    Polynomial.map φ h =
      Polynomial.map φ h')
  (hcop :
    have φ := Int.castRingHom (ZMod p);
    IsCoprime (Polynomial.map φ g)
      (Polynomial.map φ h)) :
  have φ :=
    Int.castRingHom (ZMod (p ^ k));
  Polynomial.map φ g =
      Polynomial.map φ g' ∧
    Polynomial.map φ h =
      Polynomial.map φ h'

Coprime monic factorizations with the same reduction modulo p are unique modulo p^k.

The 0 < k hypothesis is part of the calling convention; the proof works for k = 0 too because ZMod 1 is the zero ring. The hh1 hypothesis is similarly redundant: the cancellation step uses hg1 to substitute g' for g mod p, which suffices in conjunction with hcop and the monic degree bound.