:: Characterization and Existence of {G}r\"obner Bases :: by Christoph Schwarzweller :: :: Received June 11, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, ORDINAL1, RLVECT_1, ALGSTR_0, VECTSP_1, LATTICES, ZFMISC_1, POLYNOM1, SUBSET_1, STRUCT_0, RELAT_2, BAGORDER, BINOP_1, POLYRED, POLYNOM7, ARYTM_1, ARYTM_3, PRE_POLY, TERMORD, FUNCT_1, BROUWER, RELAT_1, XBOOLE_0, XXREAL_0, SUPINF_2, VALUED_0, XCMPLX_0, CAT_3, ALGSTR_1, IDEAL_1, FINSEQ_1, PARTFUN1, MESFUNC1, CARD_3, TARSKI, CARD_1, ORDERS_2, REWRITE1, INT_1, FUNCT_4, GROUP_1, ORDERS_1, DICKSON, RLVECT_2, FUNCOP_1, PBOOLE, FINSET_1, ORDINAL4, GROEB_1, NAT_1; notations TARSKI, RELAT_1, XBOOLE_0, RELAT_2, XCMPLX_0, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, ORDINAL1, ALGSTR_0, ALGSTR_1, RLVECT_1, FINSET_1, FUNCT_7, DICKSON, CARD_3, CARD_1, SUBSET_1, XTUPLE_0, MCART_1, FINSEQ_1, YELLOW_1, ORDERS_1, PRALG_1, STRUCT_0, POLYNOM7, PBOOLE, FUNCOP_1, ORDERS_2, VFUNCT_1, POLYNOM1, IDEAL_1, REWRITE1, BAGORDER, VECTSP_1, TERMORD, GROUP_1, NUMBERS, NAT_1, PRE_POLY, POLYRED, RECDEF_1; constructors REWRITE1, VECTSP_2, PRALG_1, YELLOW_1, IDEAL_1, DICKSON, BAGORDER, TERMORD, POLYRED, RECDEF_1, DOMAIN_1, RELSET_1, PBOOLE, FUNCT_7, VFUNCT_1, XTUPLE_0; registrations XBOOLE_0, RELAT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1, INT_1, CARD_1, REWRITE1, STRUCT_0, VECTSP_1, ORDERS_2, ALGSTR_1, YELLOW_1, GCD_1, POLYNOM1, POLYNOM2, POLYNOM4, IDEAL_1, POLYNOM7, DICKSON, TERMORD, POLYRED, VALUED_0, ALGSTR_0, FINSEQ_1, PRE_POLY, FUNCOP_1, VFUNCT_1, FUNCT_1, FUNCT_2; requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM; begin :: Preliminaries definition let n be Ordinal, L be right_zeroed add-associative right_complementable well-unital distributive non trivial doubleLoopStr, p be Polynomial of n,L; redefine func {p} -> 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 almost_left_invertible 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 almost_left_invertible 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 almost_left_invertible 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 almost_left_invertible 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 well-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 well-unital distributive non trivial 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 almost_left_invertible 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 almost_left_invertible 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 for n being Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 well-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 b9 being bag of n st b9 in S & b9 divides b }; end; theorem :: GROEB_1:12 :: theorem 5.35 (i) ==> (ii), p. 206 for n being Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 almost_left_invertible 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 Element of NAT, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 almost_left_invertible 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 b9 being bag of n st b9 in HT(P,T) & b9 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 almost_left_invertible 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 b9 being bag of n st b9 in HT(P,T) & b9 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 almost_left_invertible 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 almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 almost_left_invertible 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 Element of NAT, T being admissible connected TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 almost_left_invertible 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 b9 being bag of n st b9 in HT(G,T) & b9 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 almost_left_invertible 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 b9 being bag of n st b9 in HT(G,T) & b9 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible non trivial doubleLoopStr holds {0_(n,L)} is_Groebner_basis_of {0_(n,L)},T; theorem :: GROEB_1:31 for n being Element of NAT, T being connected admissible TermOrder of n, L being add-associative right_complementable right_zeroed commutative associative well-unital distributive Abelian almost_left_invertible 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 almost_left_invertible 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 almost_left_invertible 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; registration :: theorem 5.2, p. 189 let n be Element of NAT; cluster RelStr(#Bags n, DivOrder n#) -> Dickson; end; theorem :: GROEB_1:34 :: theorem 5.2, p. 189 for n being Element of 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 almost_left_invertible non trivial 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; end; notation :: 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 almost_left_invertible non trivial doubleLoopStr, P be Subset of Polynom-Ring(n,L); synonym P is_autoreduced_wrt T for P is_reduced_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 almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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 Element of NAT, T being connected admissible TermOrder of n, L being Abelian add-associative right_complementable right_zeroed commutative associative well-unital distributive almost_left_invertible 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;