Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Characterization and Existence of Gr\"obner Bases

**by****Christoph Schwarzweller**- Received June 11, 2003
- MML identifier: GROEB_1

- [ Mizar article, MML identifier index ]

environ vocabulary POLYNOM1, POLYNOM7, BOOLE, FUNCT_1, RELAT_1, VECTSP_1, RLVECT_1, ORDINAL1, LATTICES, ANPROJ_1, VECTSP_2, ALGSTR_1, ARYTM_1, REALSET1, GROUP_1, BINOP_1, ARYTM_3, TERMORD, IDEAL_1, RELAT_2, DICKSON, MCART_1, FINSEQ_1, FINSEQ_4, BHSP_3, REWRITE1, ORDERS_1, INT_1, BINOM, TARSKI, FINSET_1, FUNCOP_1, FILTER_2, PBOOLE, POLYRED, RLVECT_2, CARD_3, CAT_3, SQUARE_1, FUNCT_4, CARD_1, BAGORDER, GROEB_1, PARTFUN1; notation TARSKI, RELAT_1, XBOOLE_0, RELAT_2, XREAL_0, RELSET_1, FUNCT_1, ORDINAL1, ALGSTR_1, RLVECT_1, PARTFUN1, FINSEQ_4, FINSET_1, DICKSON, CARD_3, CARD_1, SUBSET_1, MCART_1, REALSET1, FINSEQ_1, YELLOW_1, PRALG_1, VECTSP_2, VECTSP_1, POLYNOM7, REAL_1, BINOM, PBOOLE, PRE_CIRC, ORDERS_1, POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, STRUCT_0, TERMORD, GROUP_1, NUMBERS, NAT_1, POLYRED; constructors REWRITE1, REAL_1, IDEAL_1, DICKSON, TERMORD, YELLOW_1, PRE_CIRC, MONOID_0, DOMAIN_1, POLYRED, BAGORDER; clusters STRUCT_0, RELAT_1, FINSET_1, RELSET_1, VECTSP_1, ORDINAL1, VECTSP_2, CARD_1, GCD_1, ALGSTR_1, POLYNOM1, POLYNOM2, NAT_1, INT_1, REWRITE1, BINOM, ORDERS_1, POLYNOM7, TERMORD, IDEAL_1, YELLOW_1, SUBSET_1, DICKSON, POLYRED, MEMBERED, NUMBERS, ORDINAL2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries definition let n be Ordinal, L be right_zeroed add-associative right_complementable unital distributive (non trivial doubleLoopStr), p be Polynomial of n,L; redefine func {p} -> non empty finite Subset of Polynom-Ring(n,L); end; theorem :: GROEB_1:1 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,p,g being Polynomial of n,L holds f reduces_to g,p,T implies ex m being Monomial of n,L st g = f - m *' p; theorem :: GROEB_1:2 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), f,p,g being Polynomial of n,L holds f reduces_to g,p,T implies ex m being Monomial of n,L st g = f - m *' p & not(HT(m*'p,T) in Support g) & HT(m*'p,T) <= HT(f,T),T; theorem :: GROEB_1:3 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), f,g being Polynomial of n,L, P,Q being Subset of Polynom-Ring(n,L) st P c= Q holds f reduces_to g,P,T implies f reduces_to g,Q,T; theorem :: GROEB_1:4 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P,Q being Subset of Polynom-Ring(n,L) holds P c= Q implies PolyRedRel(P,T) c= PolyRedRel(Q,T); theorem :: GROEB_1:5 for n being Ordinal, L being right_zeroed add-associative right_complementable (non empty doubleLoopStr), p being Polynomial of n,L holds Support(-p) = Support(p); theorem :: GROEB_1:6 for n being Ordinal, T being connected TermOrder of n, L being right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr), p being Polynomial of n,L holds HT(-p,T) = HT(p,T); theorem :: GROEB_1:7 for n being Ordinal, T being admissible connected TermOrder of n, L being right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr), p,q being Polynomial of n,L holds HT(p-q,T) <= max(HT(p,T),HT(q,T),T), T; theorem :: GROEB_1:8 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), p,q being Polynomial of n,L holds Support(q) c= Support(p) implies q <= p,T; theorem :: GROEB_1:9 for n being Ordinal, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), f,p being non-zero Polynomial of n,L holds f is_reducible_wrt p,T implies HT(p,T) <= HT(f,T),T; begin :: Characterization of Groebner Bases theorem :: GROEB_1:10 ::: proposition 5.33, p. 205 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr), p being Polynomial of n,L holds PolyRedRel({p},T) is locally-confluent; theorem :: GROEB_1:11 ::: corollary 5.34, p. 205 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L) st ex p being Polynomial of n,L st p in P & P-Ideal = {p}-Ideal holds PolyRedRel(P,T) is locally-confluent; definition let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable unital distributive non trivial (non empty doubleLoopStr), P be Subset of Polynom-Ring(n,L); func HT(P,T) -> Subset of Bags n equals :: GROEB_1:def 1 { HT(p,T) where p is Polynomial of n,L : p in P & p <> 0_(n,L) }; end; definition let n be Ordinal, S be Subset of Bags n; func multiples(S) -> Subset of Bags n equals :: GROEB_1:def 2 { b where b is Element of Bags n : ex b' being bag of n st b' in S & b' divides b }; end; theorem :: GROEB_1:12 ::: theorem 5.35 (i) ==> (ii), p. 206 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) is locally-confluent implies PolyRedRel(P,T) is confluent; theorem :: GROEB_1:13 ::: theorem 5.35 (ii) ==> (iii), p. 206 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) is confluent implies PolyRedRel(P,T) is with_UN_property; theorem :: GROEB_1:14 ::: theorem 5.35 (iii) ==> (iv), p. 206 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) is with_UN_property implies PolyRedRel(P,T) is with_Church-Rosser_property; theorem :: GROEB_1:15 ::: theorem 5.35 (iv) ==> (v), p. 206 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), P being non empty Subset of Polynom-Ring(n,L) holds PolyRedRel(P,T) is with_Church-Rosser_property implies (for f being Polynomial of n,L st f in P-Ideal holds PolyRedRel(P,T) reduces f,0_(n,L)); theorem :: GROEB_1:16 ::: theorem 5.35 (v) ==> (vi), p. 206 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds (for f being Polynomial of n,L st f in P-Ideal holds PolyRedRel(P,T) reduces f,0_(n,L)) implies (for f being non-zero Polynomial of n,L st f in P-Ideal holds f is_reducible_wrt P,T); theorem :: GROEB_1:17 ::: theorem 5.35 (vi) ==> (vii), p. 206 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds (for f being non-zero Polynomial of n,L st f in P-Ideal holds f is_reducible_wrt P,T) implies (for f being non-zero Polynomial of n,L st f in P-Ideal holds f is_top_reducible_wrt P,T); theorem :: GROEB_1:18 ::: theorem 5.35 (vii) ==> (viii), p. 206 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds (for f being non-zero Polynomial of n,L st f in P-Ideal holds f is_top_reducible_wrt P,T) implies (for b being bag of n st b in HT(P-Ideal,T) ex b' being bag of n st b' in HT(P,T) & b' divides b); theorem :: GROEB_1:19 ::: theorem 5.35 (viii) ==> (ix), p. 206 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds (for b being bag of n st b in HT(P-Ideal,T) ex b' being bag of n st b' in HT(P,T) & b' divides b) implies HT(P-Ideal,T) c= multiples(HT(P,T)); theorem :: GROEB_1:20 ::: theorem 5.35 (ix) ==> (i), p. 206 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), P being Subset of Polynom-Ring(n,L) holds HT(P-Ideal,T) c= multiples(HT(P,T)) implies PolyRedRel(P,T) is locally-confluent; definition ::: definition 5.37, p. 207 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), G be Subset of Polynom-Ring(n,L); pred G is_Groebner_basis_wrt T means :: GROEB_1:def 3 PolyRedRel(G,T) is locally-confluent; end; definition ::: definition 5.37, p. 207 let n be Ordinal, T be connected TermOrder of n, L be add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), G,I be Subset of Polynom-Ring(n,L); pred G is_Groebner_basis_of I,T means :: GROEB_1:def 4 G-Ideal = I & PolyRedRel(G,T) is locally-confluent; end; theorem :: GROEB_1:21 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), G,P being non empty Subset of Polynom-Ring(n,L) st G is_Groebner_basis_of P,T holds PolyRedRel(G,T) is Completion of PolyRedRel(P,T); theorem :: GROEB_1:22 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), p,q being Element of Polynom-Ring(n,L), G being non empty Subset of Polynom-Ring(n,L) st G is_Groebner_basis_wrt T holds p,q are_congruent_mod G-Ideal iff nf(p,PolyRedRel(G,T)) = nf(q,PolyRedRel(G,T)); theorem :: GROEB_1:23 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), f being Polynomial of n,L, P being non empty Subset of Polynom-Ring(n,L) st P is_Groebner_basis_wrt T holds f in P-Ideal iff PolyRedRel(P,T) reduces f,0_(n,L); theorem :: GROEB_1:24 ::: theorem 5.38 (o) ==> (i), p. 207 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), I being Subset of Polynom-Ring(n,L), G being non empty Subset of Polynom-Ring(n,L) holds G is_Groebner_basis_of I,T implies (for f being Polynomial of n,L st f in I holds PolyRedRel(G,T) reduces f,0_(n,L)); theorem :: GROEB_1:25 ::: theorem 5.38 (i) ==> (ii), p. 207 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), G,I being Subset of Polynom-Ring(n,L) holds (for f being Polynomial of n,L st f in I holds PolyRedRel(G,T) reduces f,0_(n,L)) implies (for f being non-zero Polynomial of n,L st f in I holds f is_reducible_wrt G,T); theorem :: GROEB_1:26 ::: theorem 5.38 (ii) ==> (iii), p. 207 for n being Nat, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal Subset of Polynom-Ring(n,L), G being Subset of Polynom-Ring(n,L) st G c= I holds (for f being non-zero Polynomial of n,L st f in I holds f is_reducible_wrt G,T) implies (for f being non-zero Polynomial of n,L st f in I holds f is_top_reducible_wrt G,T); theorem :: GROEB_1:27 ::: theorem 5.38 (iii) ==> (iv), p. 207 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), G,I being Subset of Polynom-Ring(n,L) holds (for f being non-zero Polynomial of n,L st f in I holds f is_top_reducible_wrt G,T) implies (for b being bag of n st b in HT(I,T) ex b' being bag of n st b' in HT(G,T) & b' divides b); theorem :: GROEB_1:28 ::: theorem 5.38 (iv) ==> (v), p. 207 for n being Ordinal, T being connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like (non trivial doubleLoopStr), G,I being Subset of Polynom-Ring(n,L) holds (for b being bag of n st b in HT(I,T) ex b' being bag of n st b' in HT(G,T) & b' divides b) implies HT(I,T) c= multiples(HT(G,T)); theorem :: GROEB_1:29 ::: theorem 5.38 (v) ==> (o), p. 207 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring(n,L), G being non empty Subset of Polynom-Ring(n,L) st G c= I holds HT(I,T) c= multiples(HT(G,T)) implies G is_Groebner_basis_of I,T; begin :: Existence of Groebner Bases theorem :: GROEB_1:30 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr) holds {0_(n,L)} is_Groebner_basis_of {0_(n,L)},T; theorem :: GROEB_1:31 for n being Nat, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like (non trivial doubleLoopStr), p being Polynomial of n,L holds {p} is_Groebner_basis_of {p}-Ideal,T; theorem :: GROEB_1:32 for T being admissible connected TermOrder of {}, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring({},L), P being non empty Subset of Polynom-Ring({},L) st P c= I & P <> {0_({},L)} holds P is_Groebner_basis_of I,T; theorem :: GROEB_1:33 for n being non empty Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr) ex P be Subset of Polynom-Ring(n,L) st not(P is_Groebner_basis_wrt T); definition ::: definition preceeding 5.1, p. 189 let n be Ordinal; func DivOrder(n) -> Order of Bags n means :: GROEB_1:def 5 for b1,b2 being bag of n holds [b1,b2] in it iff b1 divides b2; end; definition ::: theorem 5.2, p. 189 let n be Nat; cluster RelStr(#Bags n, DivOrder n#) -> Dickson; end; theorem :: GROEB_1:34 ::: theorem 5.2, p. 189 for n being Nat, N being Subset of RelStr(#Bags n, DivOrder n#) ex B being finite Subset of Bags n st B is_Dickson-basis_of N,RelStr(#Bags n, DivOrder n#); theorem :: GROEB_1:35 ::: theorem 5.41, p. 208 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring(n,L) ex G being finite Subset of Polynom-Ring(n,L) st G is_Groebner_basis_of I,T; theorem :: GROEB_1:36 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring(n,L) st I <> {0_(n,L)} ex G being finite Subset of Polynom-Ring(n,L) st G is_Groebner_basis_of I,T & not(0_(n,L) in G); definition let n be Ordinal, T be connected TermOrder of n, L be non empty multLoopStr_0, p be Polynomial of n,L; pred p is_monic_wrt T means :: GROEB_1:def 6 HC(p,T) = 1_ L; end; definition ::: definition 5.29, p. 203 let n be Ordinal, T be connected TermOrder of n, L be right_zeroed add-associative right_complementable commutative associative well-unital distributive Field-like non trivial (non empty doubleLoopStr), P be Subset of Polynom-Ring(n,L); pred P is_reduced_wrt T means :: GROEB_1:def 7 for p being Polynomial of n,L st p in P holds p is_monic_wrt T & p is_irreducible_wrt P\{p},T; synonym P is_autoreduced_wrt T; end; theorem :: GROEB_1:37 ::: lemma 5.42, p. 208 for n being Ordinal, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal Subset of Polynom-Ring(n,L), m being Monomial of n,L, f,g being Polynomial of n,L st f in I & g in I & HM(f,T) = m & HM(g,T) = m holds not(ex p being Polynomial of n,L st p in I & p < f,T & HM(p,T) = m) & not(ex p being Polynomial of n,L st p in I & p < g,T & HM(p,T) = m) implies f = g; theorem :: GROEB_1:38 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring(n,L), G being Subset of Polynom-Ring(n,L), p being Polynomial of n,L, q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT(q,T) divides HT(p,T) holds G is_Groebner_basis_of I,T implies G\{p} is_Groebner_basis_of I,T; theorem :: GROEB_1:39 ::: theorem 5.43, p. 209 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring(n,L) st I <> {0_ (n,L)} ex G being finite Subset of Polynom-Ring(n,L) st G is_Groebner_basis_of I,T & G is_reduced_wrt T; theorem :: GROEB_1:40 ::: theorem 5.43, p. 209 for n being Nat, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive Field-like non degenerated (non empty doubleLoopStr), I being add-closed left-ideal non empty Subset of Polynom-Ring(n,L), G1,G2 being non empty finite Subset of Polynom-Ring(n,L) st G1 is_Groebner_basis_of I,T & G1 is_reduced_wrt T & G2 is_Groebner_basis_of I,T & G2 is_reduced_wrt T holds G1 = G2;

Back to top