3.6. The Mathlib correspondence🔗

Everything above is executable and Mathlib-free. HexMvPolyMathlib identifies exponent vectors with finitely supported functions and sparse polynomials with Mathlib's MvPolynomial over Fin n.

def

HexMvPolyMathlib.monoEquiv {n : ℕ} : Hex.Mono n ≃ (Fin n →₀ ℕ)
HexMvPolyMathlib.monoEquiv {n : ℕ} :
  Hex.Mono n ≃ (Fin n →₀ ℕ)

A fixed-arity exponent vector is equivalent to a finitely supported function on the finite variable type.

def

HexMvPolyMathlib.equiv.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R]
  [DecidableEq R] : Hex.MvPoly n R cmp ≃+* MvPolynomial (Fin n) R
HexMvPolyMathlib.equiv.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R] [CommSemiring R]
  [DecidableEq R] :
  Hex.MvPoly n R cmp ≃+*
    MvPolynomial (Fin n) R

The executable sparse representation is ring-equivalent to Mathlib's multivariate polynomials.

def

HexMvPolyMathlib.algEquiv.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R]
  [DecidableEq R] : Hex.MvPoly n R cmp ≃ₐ[R] MvPolynomial (Fin n) R
HexMvPolyMathlib.algEquiv.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R] [CommSemiring R]
  [DecidableEq R] :
  Hex.MvPoly n R cmp ≃ₐ[R]
    MvPolynomial (Fin n) R

The exact representation equivalence as an equivalence of R-algebras.

Conversion preserves coefficients and all ring operations. It also matches differentiation, homogeneous projection, substitution, support, degree, and the recursive view.

theorem

HexMvPolyMathlib.coeff_toMvPolynomial.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R]
  (m : Hex.Mono n) (p : Hex.MvPoly n R cmp) :
  MvPolynomial.coeff (HexMvPolyMathlib.monoEquiv m)
      (HexMvPolyMathlib.toMvPolynomial p) =
    Hex.MvPoly.coeff m p
HexMvPolyMathlib.coeff_toMvPolynomial.{u}
  {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [CommSemiring R] [DecidableEq R]
  (m : Hex.Mono n)
  (p : Hex.MvPoly n R cmp) :
  MvPolynomial.coeff
      (HexMvPolyMathlib.monoEquiv m)
      (HexMvPolyMathlib.toMvPolynomial
        p) =
    Hex.MvPoly.coeff m p

Forward conversion preserves every coefficient.

theorem

HexMvPolyMathlib.toMvPolynomial_derivative.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [CommSemiring R] [DecidableEq R] (i : Fin n)
  (p : Hex.MvPoly n R cmp) :
  HexMvPolyMathlib.toMvPolynomial (Hex.MvPoly.derivative i p) =
    (MvPolynomial.pderiv i) (HexMvPolyMathlib.toMvPolynomial p)
HexMvPolyMathlib.toMvPolynomial_derivative.{u}
  {n : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [CommSemiring R] [DecidableEq R]
  (i : Fin n) (p : Hex.MvPoly n R cmp) :
  HexMvPolyMathlib.toMvPolynomial
      (Hex.MvPoly.derivative i p) =
    (MvPolynomial.pderiv i)
      (HexMvPolyMathlib.toMvPolynomial p)

Executable formal differentiation agrees with Mathlib's partial derivative.

theorem

HexMvPolyMathlib.toMvPolynomial_subst.{u} {n k : ℕ} {R : Type u}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering}
  {targetCmp : Hex.Mono k → Hex.Mono k → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [Std.TransCmp targetCmp]
  [Std.LawfulEqCmp targetCmp] [CommSemiring R] [DecidableEq R]
  (g : Fin n → Hex.MvPoly k R targetCmp) (p : Hex.MvPoly n R cmp) :
  HexMvPolyMathlib.toMvPolynomial (Hex.MvPoly.subst g p) =
    (MvPolynomial.bind₁ fun i => HexMvPolyMathlib.toMvPolynomial (g i))
      (HexMvPolyMathlib.toMvPolynomial p)
HexMvPolyMathlib.toMvPolynomial_subst.{u}
  {n k : ℕ} {R : Type u}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  {targetCmp :
    Hex.Mono k → Hex.Mono k → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [Std.TransCmp targetCmp]
  [Std.LawfulEqCmp targetCmp]
  [CommSemiring R] [DecidableEq R]
  (g : Fin n → Hex.MvPoly k R targetCmp)
  (p : Hex.MvPoly n R cmp) :
  HexMvPolyMathlib.toMvPolynomial
      (Hex.MvPoly.subst g p) =
    (MvPolynomial.bind₁ fun i =>
        HexMvPolyMathlib.toMvPolynomial
          (g i))
      (HexMvPolyMathlib.toMvPolynomial p)

Executable substitution agrees with Mathlib's variable bind.

def

HexMvPolyMathlib.finSuccEquiv.{u} {n : ℕ} {R : Type u}
  {cmp : Hex.Mono (n + 1) → Hex.Mono (n + 1) → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [CommSemiring R]
  [DecidableEq R] (cmp' : Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp'] [Std.LawfulEqCmp cmp'] :
  Hex.MvPoly (n + 1) R cmp ≃+* Hex.DensePoly (Hex.MvPoly n R cmp')
HexMvPolyMathlib.finSuccEquiv.{u} {n : ℕ}
  {R : Type u}
  {cmp :
    Hex.Mono (n + 1) →
      Hex.Mono (n + 1) → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [CommSemiring R] [DecidableEq R]
  (cmp' :
    Hex.Mono n → Hex.Mono n → Ordering)
  [Std.TransCmp cmp']
  [Std.LawfulEqCmp cmp'] :
  Hex.MvPoly (n + 1) R cmp ≃+*
    Hex.DensePoly (Hex.MvPoly n R cmp')

The executable recursive view at the first variable, packaged as a ring equivalence.

The bridge packages evaluation as an algebra homomorphism. Its application theorem states that executable evaluation is exactly Mathlib evaluation after conversion, and its remaining aeval_* lemmas expose the familiar homomorphism rules.

def

HexMvPolyMathlib.aeval.{u, v} {n : ℕ} {R : Type u} {S : Type v}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R]
  [CommSemiring S] [Algebra R S] (x : Fin n → S) :
  Hex.MvPoly n R cmp →ₐ[R] S
HexMvPolyMathlib.aeval.{u, v} {n : ℕ}
  {R : Type u} {S : Type v}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R] [CommSemiring R]
  [CommSemiring S] [Algebra R S]
  (x : Fin n → S) :
  Hex.MvPoly n R cmp →ₐ[R] S

Executable algebra evaluation. The function field is definitionally the direct Mathlib-free evaluator.

theorem

HexMvPolyMathlib.aeval_apply.{u, v} {n : ℕ} {R : Type u} {S : Type v}
  {cmp : Hex.Mono n → Hex.Mono n → Ordering} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [BEq R] [LawfulBEq R] [CommSemiring R]
  [DecidableEq R] [CommSemiring S] [Algebra R S] (x : Fin n → S)
  (p : Hex.MvPoly n R cmp) :
  (HexMvPolyMathlib.aeval x) p =
    (MvPolynomial.aeval x) (HexMvPolyMathlib.toMvPolynomial p)
HexMvPolyMathlib.aeval_apply.{u, v}
  {n : ℕ} {R : Type u} {S : Type v}
  {cmp :
    Hex.Mono n → Hex.Mono n → Ordering}
  [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [BEq R] [LawfulBEq R] [CommSemiring R]
  [DecidableEq R] [CommSemiring S]
  [Algebra R S] (x : Fin n → S)
  (p : Hex.MvPoly n R cmp) :
  (HexMvPolyMathlib.aeval x) p =
    (MvPolynomial.aeval x)
      (HexMvPolyMathlib.toMvPolynomial p)

Applying executable algebra evaluation agrees with Mathlib evaluation after conversion.