Polynomial pullback with cleared denominators

Definition

Esgk_PlanePolynomialRationalPullback

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

This defines the polynomial sum obtained from each monomial $cX^aY^b$ by replacing it with $cA^aB^bD^{\max(d-a-b,0)}$ , where the exponent uses truncated natural subtraction. For $d$ at least the input degree it is the denominator-cleared substitution of $A/D,B/D$ wherever $D$ is nonzero; the polynomial sum itself requires no nonvanishing hypothesis.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
-/


noncomputable section

namespace Esgk

open PachDeZeeuw.Algebraic (PlanePoly)

def planePolynomialRationalPullback
    (d : ℕ) (p A B D : PlanePoly) : PlanePoly :=
  ∑ m ∈ p.support,
    MvPolynomial.C (p.coeff m) * A ^ m 0 * B ^ m 1 *
      D ^ (d - (m 0 + m 1))


end Esgk

View graph