:: Characterization and Existence of {G}r\"obner Bases
:: by Christoph Schwarzweller
::
:: Received June 11, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users


definition
let n be Ordinal;
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let p be Polynomial of n,L;
:: original: {
redefine func {p} -> Subset of (Polynom-Ring (n,L));
coherence
{p} is Subset of (Polynom-Ring (n,L))
proof end;
end;

theorem Th1: :: GROEB_1:1
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
ex m being Monomial of n,L st g = f - (m *' p)
proof end;

theorem :: GROEB_1:2
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f, p, g being Polynomial of n,L st f reduces_to g,p,T holds
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 )
proof end;

Lm1: for L being non empty add-cancelable right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for P being Subset of L
for p being Element of L st p in P holds
p in P -Ideal
proof end;

Lm2: for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L
for f, g being Element of (Polynom-Ring (n,L)) st f = p & g = q holds
f - g = p - q
proof end;

Lm3: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L holds f is_irreducible_wrt 0_ (n,L),T
proof end;

theorem Th3: :: GROEB_1:3
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q & f reduces_to g,P,T holds
f reduces_to g,Q,T
proof end;

theorem Th4: :: GROEB_1:4
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P, Q being Subset of (Polynom-Ring (n,L)) st P c= Q holds
PolyRedRel (P,T) c= PolyRedRel (Q,T)
proof end;

theorem Th5: :: GROEB_1:5
for n being Ordinal
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds Support (- p) = Support p
proof end;

theorem Th6: :: GROEB_1:6
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds HT ((- p),T) = HT (p,T)
proof end;

theorem Th7: :: GROEB_1:7
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for p, q being Polynomial of n,L holds HT ((p - q),T) <= max ((HT (p,T)),(HT (q,T)),T),T
proof end;

theorem Th8: :: GROEB_1:8
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Polynomial of n,L st Support q c= Support p holds
q <= p,T
proof end;

theorem Th9: :: GROEB_1:9
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, p being non-zero Polynomial of n,L st f is_reducible_wrt p,T holds
HT (p,T) <= HT (f,T),T
proof end;

theorem Th10: :: GROEB_1:10
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds PolyRedRel ({p},T) is locally-confluent
proof end;

theorem :: GROEB_1:11
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for 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
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ;
let 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) ) } ;
coherence
{ (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } is Subset of (Bags n)
proof end;
end;

:: deftheorem defines HT GROEB_1:def 1 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty non trivial right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) holds HT (P,T) = { (HT (p,T)) where p is Polynomial of n,L : ( p in P & p <> 0_ (n,L) ) } ;

definition
let n be Ordinal;
let 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 ) } ;
coherence
{ b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } is Subset of (Bags n)
proof end;
end;

:: deftheorem defines multiples GROEB_1:def 2 :
for n being Ordinal
for S being Subset of (Bags n) holds multiples S = { b where b is Element of Bags n : ex b9 being bag of n st
( b9 in S & b9 divides b ) } ;

theorem :: GROEB_1:12
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is locally-confluent holds
PolyRedRel (P,T) is confluent ;

theorem :: GROEB_1:13
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is confluent holds
PolyRedRel (P,T) is with_UN_property ;

theorem :: GROEB_1:14
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_UN_property holds
PolyRedRel (P,T) is with_Church-Rosser_property ;

Lm4: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for g being object
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g holds
g is Polynomial of n,L
proof end;

Lm5: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for f, g being Polynomial of n,L
for P being Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) reduces f,g & g <> f holds
ex h being Polynomial of n,L st
( f reduces_to h,P,T & PolyRedRel (P,T) reduces h,g )
proof end;

theorem Th15: :: GROEB_1:15
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being non empty Subset of (Polynom-Ring (n,L)) st PolyRedRel (P,T) is with_Church-Rosser_property holds
for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L)
proof end;

theorem Th16: :: GROEB_1:16
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being Polynomial of n,L st f in P -Ideal holds
PolyRedRel (P,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T
proof end;

theorem Th17: :: GROEB_1:17
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_reducible_wrt P,T ) holds
for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T
proof end;

theorem Th18: :: GROEB_1:18
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in P -Ideal holds
f is_top_reducible_wrt P,T ) holds
for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b )
proof end;

theorem :: GROEB_1:19
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT ((P -Ideal),T) holds
ex b9 being bag of n st
( b9 in HT (P,T) & b9 divides b ) ) holds
HT ((P -Ideal),T) c= multiples (HT (P,T))
proof end;

theorem :: GROEB_1:20
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) st HT ((P -Ideal),T) c= multiples (HT (P,T)) holds
PolyRedRel (P,T) is locally-confluent
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let 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;

:: deftheorem defines is_Groebner_basis_wrt GROEB_1:def 3 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G being Subset of (Polynom-Ring (n,L)) holds
( G is_Groebner_basis_wrt T iff PolyRedRel (G,T) is locally-confluent );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let 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;

:: deftheorem defines is_Groebner_basis_of GROEB_1:def 4 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) holds
( G is_Groebner_basis_of I,T iff ( G -Ideal = I & PolyRedRel (G,T) is locally-confluent ) );

Lm6: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L))
for a, b being object st a <> b & PolyRedRel (P,T) reduces a,b holds
( a is Polynomial of n,L & b is Polynomial of n,L )
proof end;

theorem :: GROEB_1:21
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for 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)
proof end;

theorem :: GROEB_1:22
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p, q being Element of (Polynom-Ring (n,L))
for 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))) )
proof end;

theorem :: GROEB_1:23
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for f being Polynomial of n,L
for 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) ) by Th15, POLYRED:60;

Lm7: for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being LeftIdeal of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
G -Ideal = I
proof end;

theorem Th24: :: GROEB_1:24
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T holds
for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) by Th15;

theorem Th25: :: GROEB_1:25
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for f being Polynomial of n,L st f in I holds
PolyRedRel (G,T) reduces f, 0_ (n,L) ) holds
for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T
proof end;

theorem Th26: :: GROEB_1:26
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G being Subset of (Polynom-Ring (n,L)) st G c= I & ( for f being non-zero Polynomial of n,L st f in I holds
f is_reducible_wrt G,T ) holds
for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T
proof end;

theorem Th27: :: GROEB_1:27
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for f being non-zero Polynomial of n,L st f in I holds
f is_top_reducible_wrt G,T ) holds
for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b )
proof end;

theorem Th28: :: GROEB_1:28
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for G, I being Subset of (Polynom-Ring (n,L)) st ( for b being bag of n st b in HT (I,T) holds
ex b9 being bag of n st
( b9 in HT (G,T) & b9 divides b ) ) holds
HT (I,T) c= multiples (HT (G,T))
proof end;

theorem Th29: :: GROEB_1:29
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G being non empty Subset of (Polynom-Ring (n,L)) st G c= I & HT (I,T) c= multiples (HT (G,T)) holds
G is_Groebner_basis_of I,T
proof end;

theorem Th30: :: GROEB_1:30
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr holds {(0_ (n,L))} is_Groebner_basis_of {(0_ (n,L))},T
proof end;

theorem :: GROEB_1:31
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L holds {p} is_Groebner_basis_of {p} -Ideal ,T
proof end;

theorem :: GROEB_1:32
for T being connected admissible TermOrder of {}
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring ({},L))
for P being non empty Subset of (Polynom-Ring ({},L)) st P c= I & P <> {(0_ ({},L))} holds
P is_Groebner_basis_of I,T
proof end;

theorem :: GROEB_1:33
for n being non empty Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr holds
not for P being Subset of (Polynom-Ring (n,L)) holds P is_Groebner_basis_wrt T
proof end;

Lm8: for n being Ordinal
for b1, b2, b3 being bag of n st b1 divides b2 & b2 divides b3 holds
b1 divides b3
proof end;

definition
let n be Ordinal;
func DivOrder n -> Order of (Bags n) means :Def5: :: GROEB_1:def 5
 for b1, b2 being bag of n holds
( [b1,b2] in it iff b1 divides b2 );
existence
ex b1 being Order of (Bags n) st
for b1, b2 being bag of n holds
( [b1,b2] in b1 iff b1 divides b2 )
proof end;
uniqueness
for b1, b2 being Order of (Bags n) st ( for b1, b2 being bag of n holds
( [b1,b2] in b1 iff b1 divides b2 ) ) & ( for b1, b2 being bag of n holds
( [b1,b2] in b2 iff b1 divides b2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines DivOrder GROEB_1:def 5 :
for n being Ordinal
for b2 being Order of (Bags n) holds
( b2 = DivOrder n iff for b1, b2 being bag of n holds
( [b1,b2] in b2 iff b1 divides b2 ) );

registration
let n be Element of NAT ;
cluster RelStr(# (Bags n),(DivOrder n) #) -> Dickson ;
coherence
RelStr(# (Bags n),(DivOrder n) #) is Dickson
proof end;
end;

theorem Th34: :: GROEB_1:34
for n being Element of NAT
for 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) #)
proof end;

theorem Th35: :: GROEB_1:35
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) ex G being finite Subset of (Polynom-Ring (n,L)) st G is_Groebner_basis_of I,T
proof end;

Lm9: for L being non empty right_complementable well-unital distributive add-associative right_zeroed associative left_zeroed doubleLoopStr
for A, B being non empty Subset of L st B = A \ {(0. L)} holds
for f being LinearCombination of A
for u being set st u = Sum f holds
ex g being LinearCombination of B st u = Sum g
proof end;

theorem :: GROEB_1:36
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & not 0_ (n,L) in G )
proof end;

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non empty multLoopStr_0 ;
let p be Polynomial of n,L;
pred p is_monic_wrt T means :Def6: :: GROEB_1:def 6
 HC (p,T) = 1. L;
end;

:: deftheorem Def6 defines is_monic_wrt GROEB_1:def 6 :
for n being Ordinal
for T being connected TermOrder of n
for L being non empty multLoopStr_0
for p being Polynomial of n,L holds
( p is_monic_wrt T iff HC (p,T) = 1. L );

definition
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let 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;

:: deftheorem defines is_reduced_wrt GROEB_1:def 7 :
for n being Ordinal
for T being connected TermOrder of n
for L being non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr
for P being Subset of (Polynom-Ring (n,L)) holds
( P is_reduced_wrt T iff for p being Polynomial of n,L st p in P holds
( p is_monic_wrt T & p is_irreducible_wrt P \ {p},T ) );

notation
let n be Ordinal;
let T be connected TermOrder of n;
let L be non trivial right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative doubleLoopStr ;
let P be Subset of (Polynom-Ring (n,L));
synonym P is_autoreduced_wrt T for P is_reduced_wrt T;
end;

theorem Th37: :: GROEB_1:37
for n being Ordinal
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being add-closed left-ideal Subset of (Polynom-Ring (n,L))
for m being Monomial of n,L
for f, g being Polynomial of n,L st f in I & g in I & HM (f,T) = m & HM (g,T) = m & ( for p being Polynomial of n,L holds
( not p in I or not p < f,T or not HM (p,T) = m ) ) & ( for p being Polynomial of n,L holds
( not p in I or not p < g,T or not HM (p,T) = m ) ) holds
f = g
proof end;

Lm10: for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for p being Polynomial of n,L
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st p in I & p <> 0_ (n,L) holds
ex q being Polynomial of n,L st
( q in I & HM (q,T) = Monom ((1. L),(HT (p,T))) & q <> 0_ (n,L) )
proof end;

theorem :: GROEB_1:38
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))
for G being Subset of (Polynom-Ring (n,L))
for p being Polynomial of n,L
for q being non-zero Polynomial of n,L st p in G & q in G & p <> q & HT (q,T) divides HT (p,T) & G is_Groebner_basis_of I,T holds
G \ {p} is_Groebner_basis_of I,T
proof end;

theorem :: GROEB_1:39
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L)) st I <> {(0_ (n,L))} holds
ex G being finite Subset of (Polynom-Ring (n,L)) st
( G is_Groebner_basis_of I,T & G is_reduced_wrt T )
proof end;

theorem :: GROEB_1:40
for n being Element of NAT
for T being connected admissible TermOrder of n
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr
for I being non empty add-closed left-ideal Subset of (Polynom-Ring (n,L))
for 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
proof end;