The elimination theorem

Let e : τ → σ identify the variables τ with some of the variables σ, and let I be an ideal of MvPolynomial σ R. The elimination ideal of I is I.comap (rename e), the set of polynomials in the variables τ which lie in I once their variables are renamed by e: it consists of the consequences of the equations in I from which the remaining variables have been eliminated.

Suppose the monomial order m on σ is an elimination order for τ: every monomial below a monomial in the variables e τ is again a monomial in those variables. If G is a Gröbner basis of I for m, then the members of G which only involve the variables e τ form a Gröbner basis of the elimination ideal, for any monomial order m' on τ which e carries to m. When the coefficients form a commutative ring, they in particular generate the elimination ideal, so a single Gröbner basis of I computes the elimination ideal.

The lexicographic order is an elimination order for every upper set of variables: with the antitone variable convention, the variables of an upper set are the smallest ones. The transport of leading data along a relabeling, the description of polynomials whose leading monomial only involves the variables e τ for an elimination order, and this property of the lexicographic order are in TauCeti.RingTheory.MvPolynomial.MonomialOrder.

Main results

• MonomialOrder.IsGroebnerBasis.comap_rename: the elimination theorem, the members of a Gröbner basis in the variables e τ form a Gröbner basis of the elimination ideal.
• MonomialOrder.IsGroebnerBasis.comap_rename_eq_span: over a commutative ring, they generate the elimination ideal.
• MonomialOrder.IsGroebnerBasis.comap_rename_lex: the elimination theorem for the lexicographic order and a strictly monotone embedding onto an upper set of variables.

None of these results assume that the coefficients form a field.

References

• D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms, Chapter 3, §1, Theorem 2 (the elimination theorem), and the exercises of that section on elimination orders.

theorem MonomialOrder.IsGroebnerBasis.comap_rename {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {m : MonomialOrder σ} {m' : MonomialOrder τ} {e : τ → σ} {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hm : ∀ (a b : τ →₀ ℕ), m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b)) (helim : ∀ (a b : σ →₀ ℕ), m.toSyn a ≤ m.toSyn b → ↑b.support ⊆ Set.range e → ↑a.support ⊆ Set.range e) : m'.IsGroebnerBasis (⇑(MvPolynomial.rename e) ⁻¹' G) (Ideal.comap (MvPolynomial.rename e) I)

The elimination theorem. Let m be an elimination order for the variables e τ: every monomial below a monomial in these variables is again a monomial in these variables. If G is a Gröbner basis of I for m, then the members of G in the variables e τ form a Gröbner basis of the elimination ideal I.comap (rename e) for every monomial order m' on τ which e carries to m.

theorem MonomialOrder.IsGroebnerBasis.comap_rename_eq_span {σ : Type u_1} {τ : Type u_2} {m : MonomialOrder σ} {m' : MonomialOrder τ} {e : τ → σ} {R : Type u_4} [CommRing R] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : m.IsGroebnerBasis G I) (hm : ∀ (a b : τ →₀ ℕ), m'.toSyn a ≤ m'.toSyn b ↔ m.toSyn (Finsupp.mapDomain e a) ≤ m.toSyn (Finsupp.mapDomain e b)) (helim : ∀ (a b : σ →₀ ℕ), m.toSyn a ≤ m.toSyn b → ↑b.support ⊆ Set.range e → ↑a.support ⊆ Set.range e) : Ideal.comap (MvPolynomial.rename e) I = Ideal.span (⇑(MvPolynomial.rename e) ⁻¹' G)

In the elimination theorem over a commutative ring, the members of the Gröbner basis in the variables e τ generate the elimination ideal.

theorem MonomialOrder.IsGroebnerBasis.comap_rename_lex {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [CommSemiring R] {e : τ → σ} [LinearOrder σ] [WellFoundedGT σ] [LinearOrder τ] [WellFoundedGT τ] {G : Set (MvPolynomial σ R)} {I : Ideal (MvPolynomial σ R)} (h : lex.IsGroebnerBasis G I) (he : StrictMono e) (hup : IsUpperSet (Set.range e)) : lex.IsGroebnerBasis (⇑(MvPolynomial.rename e) ⁻¹' G) (Ideal.comap (MvPolynomial.rename e) I)

The elimination theorem for the lexicographic order. If e : τ → σ is strictly monotone with image an upper set of variables, then the members of a lexicographic Gröbner basis of I in the variables e τ form a lexicographic Gröbner basis of the elimination ideal.