Documentation

Groebner.Defs

@[simp]
theorem MonomialOrder.zero_le {σ : Type u_1} (m : MonomialOrder σ) (a : m.syn) :
0 a

a \in Partially Ordered Set, a \geq 0

theorem MonomialOrder.degree_mem_support_iff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) :
noncomputable def MonomialOrder.leadingTerm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (f : MvPolynomial σ R) :

Given a nonzero polynomial $f \in k[x]$, let $$ f = c_0 x^m + c_1 x^{m-1} + \cdots + c_m, $$ where $c_i \in k$ and $c_0 \neq 0$ [thus, $m = \deg(f)$]. Then we say that $c_0 x^m$ is the leading term of $f$, written $$ \operatorname{LT}(f) = c_0 x^m. $$

Equations
Instances For
    def MonomialOrder.IsRemainder {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) :

    Fix a monomial order $>$ on $\mathbb{Z}_{\geq 0}^n$, and let $F = (f_1, \ldots, f_s)$ be an ordered $s$-tuple of polynomials in $k[x_1, \ldots, x_n]$. Then every $f \in k[x_1, \ldots, x_n]$ can be written as $$ f = a_1 f_1 + \cdots + a_s f_s + r, $$ where $a_i, r \in k[x_1, \ldots, x_n]$, and either $r = 0$ or $r$ is a linear combination, with coefficients in $k$, of monomials, none of which is divisible by any of $\mathrm{LT}(f_1), \ldots, \mathrm{LT}(f_s)$. We will call $r$ a remainder of $f$ on division by $F$.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem MonomialOrder.IsRemainder_def' {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) :
      m.IsRemainder p B r (∃ (g : MvPolynomial σ R →₀ MvPolynomial σ R), g.support B p = (Finsupp.linearCombination (MvPolynomial σ R) id) g + r bB, m.toSyn (m.degree (b * g b)) m.toSyn (m.degree p)) cr.support, g'B, g' 0¬m.degree g' c

      Let $p \in R[\mathbf{X}]$, $G'' \subseteq R[\mathbf{X}]$ be a set of polynomials, and $r \in R[\mathbf{X}]$. Then $r$ is a remainder of $p$ modulo $G''$ with respect to monomial order $m$ if and only if there exists a finite linear combination from $G''$ such that:

      1. The support of the combination is contained in $G''$
      2. $p$ decomposes as the sum of this combination and $r$
      3. For each $g' \in G''$, the degree of $g' \cdot (coefficient\ of\ g')$ is bounded by $\deg_m(p)$
      4. No term of $r$ is divisible by any leading term of non-zero elements in $G''$
      theorem MonomialOrder.IsRemainder_def'' {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) :
      m.IsRemainder p B r (∃ (g : MvPolynomial σ RMvPolynomial σ R) (B' : Finset (MvPolynomial σ R)), B' B p = xB', g x * x + r b'B', m.toSyn (m.degree (b' * g b')) m.toSyn (m.degree p)) cr.support, bB, b 0¬m.degree b c

      Let $p, r \in k[x_i : i \in \sigma]$, and let $G' \subseteq k[x_i : i \in \sigma]$ be a finite set. We say that $r$ is a generalized remainder of $p$ upon division by $G'$ if the following two conditions hold:

      1. For every nonzero $g \in G'$ and every monomial $x^s \in \operatorname{supp}(r)$, there exists some component $j \in \sigma$ such that $$ \operatorname{multideg}(g)_j > s_j. $$
      2. There exists a function $q : G' \to k[x_i : i \in \sigma]$ such that:
      - For every $g \in G'$,
            $$
            \operatorname{multideg}''(q(g)g) \leq \operatorname{multideg}''(p);
            $$
      - The decomposition holds:
            $$
            p = \sum_{g \in G'} q(g)g + r.
            $$
      
      theorem MonomialOrder.lm_eq_zero_iff {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) :
      m.leadingTerm p = 0 p = 0

      Let $p \in R[\mathbf{X}]$ be a multivariate polynomial. Then the leading term of $p$ vanishes with respect to monomial order $m$ if and only if $p$ is the zero polynomial: $$ \LT_m(p) = 0 \iff p = 0 $$

      For any set of polynomials $G'' \subseteq R[\mathbf{X}]$ and monomial order $m$, the image of leading terms on the nonzero elements of $G''$ equals the image on all elements minus zero: $$ \LT_m(G'' \setminus \{0\}) = \LT_m(G'') \setminus \{0\} $$

      theorem MonomialOrder.isRemainder_of_insert_zero_iff_isRemainder {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) :
      m.IsRemainder p (insert 0 B) r m.IsRemainder p B r

      Let $p \in R[\mathbf{X}]$ be a polynomial, $G'' \subseteq R[\mathbf{X}]$ a set of polynomials, and $r \in R[\mathbf{X}]$ a remainder. Then the remainder property is invariant under inserting the zero polynomial: $$ \mathsf{IsRemainder}_m\,p\,(G'' \cup \{0\})\,r \iff \mathsf{IsRemainder}_m\,p\,G''\,r $$

      theorem MonomialOrder.isRemainder_sdiff_singleton_zero_iff_isRemainder {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommSemiring R] (p : MvPolynomial σ R) (B : Set (MvPolynomial σ R)) (r : MvPolynomial σ R) :
      m.IsRemainder p (B \ {0}) r m.IsRemainder p B r

      Let $p \in R[\mathbf{X}]$ be a polynomial, $G'' \subseteq R[\mathbf{X}]$ a set of polynomials, and $r \in R[\mathbf{X}]$ a remainder. Then the remainder property is invariant under removal of the zero polynomial: $$ \mathsf{IsRemainder}_m\,p\,(G'' \setminus \{0\})\,r \iff \mathsf{IsRemainder}_m\,p\,G''\,r $$

      def MonomialOrder.IsGroebnerBasis {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_3} [CommSemiring R] (G' : Finset (MvPolynomial σ R)) (I : Ideal (MvPolynomial σ R)) :

      Fix a monomial order on the polynomial ring $k[x_1, \ldots, x_n]$.A finite subset $G = \{g_1, \ldots, g_t\}$ of an ideal $I \subseteq k[x_1, \ldots, x_n]$, with $I \ne \{0\}$, is said to be a Gröbner basis (or standard basis) if $$ \langle \operatorname{LT}(g_1), \ldots, \operatorname{LT}(g_t) \rangle = \langle \operatorname{LT}(I) \rangle. $$ Using the convention that $\langle \emptyset \rangle = \{0\}$, we define the empty set $\emptyset$ to be the Gröbner basis of the zero ideal $\{0\}$.

      Equations
      Instances For
        noncomputable def MonomialOrder.sPolynomial {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

        The $S$-polynomial of $f$ and $g$ is the combination $$ S(f, g) = \frac{x^\gamma}{\mathrm{LT}(f)} \cdot f - \frac{x^\gamma}{\mathrm{LT}(g)} \cdot g. $$

        Equations
        Instances For
          theorem MonomialOrder.sPolynomial_antisymm {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (f g : MvPolynomial σ R) :

          the S-polynomial of $f$ and $g$ is antisymmetric: $$ \Sph{f}{g} = -\Sph{g}{f} $$

          theorem MonomialOrder.sPolynomial_eq_zero_of_left_eq_zero {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] (g : MvPolynomial σ R) :
          m.sPolynomial 0 g = 0

          For any polynomial $g \in \MvPolynomial{\sigma}{R}$ and monomial order $m$, the S-polynomial with zero as first argument vanishes: $$ \Sph{0}{g} = 0 $$

          For any polynomial $g \in \MvPolynomial{\sigma}{R}$ and monomial order $m$, the S-polynomial with zero as second argument vanishes: $$ \Sph{f}{0} = 0 $$

          theorem MonomialOrder.div_set' {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [CommRing R] {B : Set (MvPolynomial σ R)} (hB : bB, IsUnit (m.leadingCoeff b) b = 0) (p : MvPolynomial σ R) :
          ∃ (r : MvPolynomial σ R), m.IsRemainder p B r

          Let $G'' \subseteq R[\mathbf{X}]$ be a set of polynomials where every nonzero element has a unit leading coefficient: $$ \forall g \in G'',\ \big(\mathrm{IsUnit}(\LC_m(g)) \lor g = 0\big) $$ Then for any polynomial $p \in R[\mathbf{X}]$, there exists a remainder $r$ satisfying: $$ \mathsf{IsRemainder}_m\,p\,G''\,r $$ where $\LC_m(g)$ denotes the leading coefficient of $g$ under monomial order $m$.

          theorem MonomialOrder.div_set'' {σ : Type u_1} (m : MonomialOrder σ) {k : Type u_2} [Field k] {B : Set (MvPolynomial σ k)} (p : MvPolynomial σ k) :
          ∃ (r : MvPolynomial σ k), m.IsRemainder p B r

          Let $k$ be a field, and let $G'' \subseteq k[x_i : i \in \sigma]$ be a set of polynomials. Then for any $p \in k[x_i : i \in \sigma]$, there exists a generalized remainder $r$ of $p$ upon division by $G''$.